[STATEMENT]
lemma poincare_circle_is_euclidean_circle:
  assumes "z \<in> unit_disc" and "r > 0"
  shows  "let (Ze, Re) = poincare_circle_euclidean z r
           in of_complex ` (circle Ze Re) = poincare_circle z r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
let ?z = "to_complex z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
z \<in> unit_disc
0 < r
[PROOF STEP]
obtain z' where z': "z = of_complex z'" "cmod z' < 1"
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
0 < r

goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>z = of_complex z'; cmod z' < 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of z]
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
0 < r
z = \<infinity>\<^sub>h \<or> (\<exists>x. z = of_complex x)

goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>z = of_complex z'; cmod z' < 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = of_complex z'
cmod z' < 1

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have *: "\<And> x. cmod x < 1 \<Longrightarrow> 1 - (cmod x)\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. cmod x < 1 \<Longrightarrow> 0 < 1 - (cmod x)\<^sup>2
[PROOF STEP]
by (metis less_iff_diff_less_0 minus_diff_eq mult.left_neutral neg_less_0_iff_less norm_mult_less norm_power power2_eq_square)
[PROOF STATE]
proof (state)
this:
cmod ?x < 1 \<Longrightarrow> 0 < 1 - (cmod ?x)\<^sup>2

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
let ?R = "(cosh r - 1) / 2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
obtain R where R: "R = ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>R. R = (cosh r - 1) / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R = (cosh r - 1) / 2

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
let ?cx = "1 - (cmod x)\<^sup>2" and ?cz = "1 - (cmod z')\<^sup>2"  and ?czx = "(cmod (z' - x))\<^sup>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
let ?k = "1 + R * ?cz"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
obtain k where k: "k = ?k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k = 1 + R * (1 - (cmod z')\<^sup>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k = 1 + R * (1 - (cmod z')\<^sup>2)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "R > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < R
[PROOF STEP]
using R cosh_gt_1[OF \<open>r > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
R = (cosh r - 1) / 2
1 < cosh r

goal (1 subgoal):
 1. 0 < R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < R

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
hence "k > 1"
[PROOF STATE]
proof (prove)
using this:
0 < R

goal (1 subgoal):
 1. 1 < k
[PROOF STEP]
using assms z' k *[of z']
[PROOF STATE]
proof (prove)
using this:
0 < R
z \<in> unit_disc
0 < r
z = of_complex z'
cmod z' < 1
k = 1 + R * (1 - (cmod z')\<^sup>2)
cmod z' < 1 \<Longrightarrow> 0 < 1 - (cmod z')\<^sup>2

goal (1 subgoal):
 1. 1 < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < k

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
hence **: "cor k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
1 < k

goal (1 subgoal):
 1. cor k \<noteq> 0
[PROOF STEP]
by (smt of_real_eq_0_iff)
[PROOF STATE]
proof (state)
this:
cor k \<noteq> 0

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "of_complex x \<in> poincare_circle z r \<longleftrightarrow> cmod x < 1 \<and> poincare_distance z (of_complex x) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> poincare_distance z (of_complex x) = r)
[PROOF STEP]
unfolding poincare_circle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_complex x \<in> {z' \<in> unit_disc. poincare_distance z z' = r}) = (cmod x < 1 \<and> poincare_distance z (of_complex x) = r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> poincare_distance z (of_complex x) = r)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> poincare_distance z (of_complex x) = r)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> poincare_distance_formula' ?z x = cosh r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> poincare_distance z (of_complex x) = r) = (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r)
[PROOF STEP]
using poincare_distance_formula[of z "of_complex x"] cosh_dist[of z "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance z (of_complex x) = poincare_distance_formula (to_complex z) (to_complex (of_complex x))
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> cosh_dist z (of_complex x) = poincare_distance_formula' (to_complex z) (to_complex (of_complex x))

goal (1 subgoal):
 1. (cmod x < 1 \<and> poincare_distance z (of_complex x) = r) = (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r)
[PROOF STEP]
unfolding poincare_distance_formula_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance z (of_complex x) = arcosh (poincare_distance_formula' (to_complex z) (to_complex (of_complex x)))
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> cosh_dist z (of_complex x) = poincare_distance_formula' (to_complex z) (to_complex (of_complex x))

goal (1 subgoal):
 1. (cmod x < 1 \<and> poincare_distance z (of_complex x) = r) = (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance z (of_complex x) = arcosh (poincare_distance_formula' (to_complex z) (to_complex (of_complex x)))
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> cosh_dist z (of_complex x) = poincare_distance_formula' (to_complex z) (to_complex (of_complex x))
z \<in> unit_disc
0 < r

goal (1 subgoal):
 1. (cmod x < 1 \<and> poincare_distance z (of_complex x) = r) = (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r)
[PROOF STEP]
using arcosh_cosh_real
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance z (of_complex x) = arcosh (poincare_distance_formula' (to_complex z) (to_complex (of_complex x)))
\<lbrakk>z \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> cosh_dist z (of_complex x) = poincare_distance_formula' (to_complex z) (to_complex (of_complex x))
z \<in> unit_disc
0 < r
0 \<le> ?x \<Longrightarrow> arcosh (cosh ?x) = ?x

goal (1 subgoal):
 1. (cmod x < 1 \<and> poincare_distance z (of_complex x) = r) = (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> poincare_distance z (of_complex x) = r) = (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> poincare_distance z (of_complex x) = r) = (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> ?czx / (?cz * ?cx) = ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2)
[PROOF STEP]
using z'
[PROOF STATE]
proof (prove)
using this:
z = of_complex z'
cmod z' < 1

goal (1 subgoal):
 1. (cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> poincare_distance_formula' (to_complex z) x = cosh r) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> ?czx = ?R * ?cx * ?cz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2))
[PROOF STEP]
using assms z' *[of z'] *[of x]
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
0 < r
z = of_complex z'
cmod z' < 1
cmod z' < 1 \<Longrightarrow> 0 < 1 - (cmod z')\<^sup>2
cmod x < 1 \<Longrightarrow> 0 < 1 - (cmod x)\<^sup>2

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2))
[PROOF STEP]
using nonzero_divide_eq_eq[of "(1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)" "(cmod (z' - x))\<^sup>2" ?R]
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
0 < r
z = of_complex z'
cmod z' < 1
cmod z' < 1 \<Longrightarrow> 0 < 1 - (cmod z')\<^sup>2
cmod x < 1 \<Longrightarrow> 0 < 1 - (cmod x)\<^sup>2
(1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2) \<noteq> 0 \<Longrightarrow> ((cmod (z' - x))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cosh r - 1) / 2) = ((cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * ((1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)))

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2))
[PROOF STEP]
by (auto, simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 / ((1 - (cmod z')\<^sup>2) * (1 - (cmod x)\<^sup>2)) = (cosh r - 1) / 2) = (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = R * ?cz * (1 - x * cnj x)" (is "_ \<longleftrightarrow> _ \<and> ?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
let ?l = "(z' - x) * (cnj z' - cnj x)" and ?r = "R * (1 - Re (z' * cnj z')) * (1 - x * cnj x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
have "is_real ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real ((z' - x) * (cnj z' - cnj x))
[PROOF STEP]
using eq_cnj_iff_real[of "?l"]
[PROOF STATE]
proof (prove)
using this:
(cnj ((z' - x) * (cnj z' - cnj x)) = (z' - x) * (cnj z' - cnj x)) = is_real ((z' - x) * (cnj z' - cnj x))

goal (1 subgoal):
 1. is_real ((z' - x) * (cnj z' - cnj x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_real ((z' - x) * (cnj z' - cnj x))

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_real ((z' - x) * (cnj z' - cnj x))

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
have "is_real ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))
[PROOF STEP]
using eq_cnj_iff_real[of "1 - x * cnj x"]
[PROOF STATE]
proof (prove)
using this:
(cnj (1 - x * cnj x) = 1 - x * cnj x) = is_real (1 - x * cnj x)

goal (1 subgoal):
 1. is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))
[PROOF STEP]
using Im_complex_of_real[of "R * (1 - Re (z' * cnj z'))"]
[PROOF STATE]
proof (prove)
using this:
(cnj (1 - x * cnj x) = 1 - x * cnj x) = is_real (1 - x * cnj x)
is_real (cor (R * (1 - Re (z' * cnj z'))))

goal (1 subgoal):
 1. is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_real ((z' - x) * (cnj z' - cnj x))
is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_real ((z' - x) * (cnj z' - cnj x))
is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
apply (subst R[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_real ((z' - x) * (cnj z' - cnj x)); is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))\<rbrakk> \<Longrightarrow> (cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = R * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))
[PROOF STEP]
apply (subst cmod_square)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_real ((z' - x) * (cnj z' - cnj x)); is_real (cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))\<rbrakk> \<Longrightarrow> (cmod x < 1 \<and> Re ((z' - x) * cnj (z' - x)) = R * (1 - Re (x * cnj x)) * (1 - Re (z' * cnj z'))) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - Re (z' * cnj z'))) * (1 - x * cnj x))
[PROOF STEP]
apply (subst complex_eq_if_Re_eq, simp_all add: field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (z' - x))\<^sup>2 = (cosh r - 1) / 2 * (1 - (cmod x)\<^sup>2) * (1 - (cmod z')\<^sup>2)) = (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = R * ?cz - R * ?cz * x * cnj x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x)) = (cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = cor (R * (1 - (cmod z')\<^sup>2)) - cor (R * (1 - (cmod z')\<^sup>2)) * x * cnj x)
[PROOF STEP]
unfolding right_diff_distrib left_diff_distrib
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> z' * cnj z' - x * cnj z' - (z' * cnj x - x * cnj x) = cor (R * 1 - R * (cmod z')\<^sup>2) * 1 - cor (R * 1 - R * (cmod z')\<^sup>2) * (x * cnj x)) = (cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = cor (R * 1 - R * (cmod z')\<^sup>2) - cor (R * 1 - R * (cmod z')\<^sup>2) * x * cnj x)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x)) = (cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = cor (R * (1 - (cmod z')\<^sup>2)) - cor (R * (1 - (cmod z')\<^sup>2)) * x * cnj x)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (z' - x) * (cnj z' - cnj x) = cor (R * (1 - (cmod z')\<^sup>2)) * (1 - x * cnj x)) = (cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = cor (R * (1 - (cmod z')\<^sup>2)) - cor (R * (1 - (cmod z')\<^sup>2)) * x * cnj x)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = R * ?cz" (is "_ \<longleftrightarrow> _ \<and> ?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = cor (R * (1 - (cmod z')\<^sup>2)) - cor (R * (1 - (cmod z')\<^sup>2)) * x * cnj x) = (cmod x < 1 \<and> cor k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = cor (R * (1 - (cmod z')\<^sup>2)))
[PROOF STEP]
by (subst k) (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = cor (R * (1 - (cmod z')\<^sup>2)) - cor (R * (1 - (cmod z')\<^sup>2)) * x * cnj x) = (cmod x < 1 \<and> cor k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = cor (R * (1 - (cmod z')\<^sup>2)))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> z' * cnj z' - x * cnj z' - cnj x * z' + x * cnj x = cor (R * (1 - (cmod z')\<^sup>2)) - cor (R * (1 - (cmod z')\<^sup>2)) * x * cnj x) = (cmod x < 1 \<and> cor k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = cor (R * (1 - (cmod z')\<^sup>2)))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> (k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / k = (R * ?cz) / k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> cor k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = cor (R * (1 - (cmod z')\<^sup>2))) = (cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
cor k \<noteq> 0

goal (1 subgoal):
 1. (cmod x < 1 \<and> cor k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = cor (R * (1 - (cmod z')\<^sup>2))) = (cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))
[PROOF STEP]
by (auto simp add: Groups.mult_ac(1))
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> cor k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = cor (R * (1 - (cmod z')\<^sup>2))) = (cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> cor k * (x * cnj x) - x * cnj z' - cnj x * z' + z' * cnj z' = cor (R * (1 - (cmod z')\<^sup>2))) = (cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> x * cnj x - x * cnj z' / k - cnj x * z' / k + z' * cnj z' / k = (R * ?cz) / k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
cor k \<noteq> 0

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))
[PROOF STEP]
unfolding add_divide_distrib diff_divide_distrib
[PROOF STATE]
proof (prove)
using this:
cor k \<noteq> 0

goal (1 subgoal):
 1. (cmod x < 1 \<and> cor k * x * cnj x / cor k - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cor k * x * cnj x - x * cnj z' - cnj x * z' + z' * cnj z') / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> (x - z'/k) * cnj(x - z'/k) = (R * ?cz) / k + (z' / k) * cnj(z' / k) - z' * cnj z' / k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> (x - z' / cor k) * cnj (x - z' / cor k) = cor (R * (1 - (cmod z')\<^sup>2) / k) + z' / cor k * cnj (z' / cor k) - z' * cnj z' / cor k)
[PROOF STEP]
by (auto simp add: field_simps diff_divide_distrib)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> (x - z' / cor k) * cnj (x - z' / cor k) = cor (R * (1 - (cmod z')\<^sup>2) / k) + z' / cor k * cnj (z' / cor k) - z' * cnj z' / cor k)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> x * cnj x - x * cnj z' / cor k - cnj x * z' / cor k + z' * cnj z' / cor k = cor (R * (1 - (cmod z')\<^sup>2) / k)) = (cmod x < 1 \<and> (x - z' / cor k) * cnj (x - z' / cor k) = cor (R * (1 - (cmod z')\<^sup>2) / k) + z' / cor k * cnj (z' / cor k) - z' * cnj z' / cor k)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> (cmod (x - z'/k))\<^sup>2 = (R * ?cz) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (x - z' / cor k) * cnj (x - z' / cor k) = cor (R * (1 - (cmod z')\<^sup>2) / k) + z' / cor k * cnj (z' / cor k) - z' * cnj z' / cor k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k)
[PROOF STEP]
apply (subst complex_mult_cnj_cmod)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> cor ((cmod (x - z' / cor k))\<^sup>2) = cor (R * (1 - (cmod z')\<^sup>2) / k) + cor ((cmod (z' / cor k))\<^sup>2) - cor ((cmod z')\<^sup>2) / cor k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k)
[PROOF STEP]
apply (subst complex_eq_if_Re_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. is_real (cor ((cmod (x - z' / cor k))\<^sup>2))
 2. is_real (cor (R * (1 - (cmod z')\<^sup>2) / k) + cor ((cmod (z' / cor k))\<^sup>2) - cor ((cmod z')\<^sup>2) / cor k)
 3. (cmod x < 1 \<and> Re (cor ((cmod (x - z' / cor k))\<^sup>2)) = Re (cor (R * (1 - (cmod z')\<^sup>2) / k) + cor ((cmod (z' / cor k))\<^sup>2) - cor ((cmod z')\<^sup>2) / cor k)) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k)
[PROOF STEP]
apply (simp_all add: power_divide)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (x - z' / cor k) * cnj (x - z' / cor k) = cor (R * (1 - (cmod z')\<^sup>2) / k) + z' / cor k * cnj (z' / cor k) - z' * cnj z' / cor k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (x - z' / cor k) * cnj (x - z' / cor k) = cor (R * (1 - (cmod z')\<^sup>2) / k) + z' / cor k * cnj (z' / cor k) - z' * cnj z' / cor k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> (cmod (x - z'/k))\<^sup>2 = (R * ?cz * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2)
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
cor k \<noteq> 0

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2)
[PROOF STEP]
unfolding add_divide_distrib diff_divide_distrib
[PROOF STATE]
proof (prove)
using this:
cor k \<noteq> 0

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) * k / k\<^sup>2 + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 * k / k\<^sup>2)
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = R * (1 - (cmod z')\<^sup>2) / k + (cmod z')\<^sup>2 / k\<^sup>2 - (cmod z')\<^sup>2 / k) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> (cmod (x - z'/k))\<^sup>2 = ?cz\<^sup>2 * R * (R + 1) / k\<^sup>2" (is "_ \<longleftrightarrow> _ \<and> ?a\<^sup>2 = ?b")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)
[PROOF STEP]
have *: "R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1)
[PROOF STEP]
by (subst k)+ (simp add: field_simps power2_diff)
[PROOF STATE]
proof (state)
this:
R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1)

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1)

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)
[PROOF STEP]
by (subst *, simp)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (R * (1 - (cmod z')\<^sup>2) * k + (cmod z')\<^sup>2 - (cmod z')\<^sup>2 * k) / k\<^sup>2) = (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
have "... \<longleftrightarrow> cmod x < 1 \<and> cmod (x - z'/k) = ?cz * sqrt (R * (R + 1)) / k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2) = (cmod x < 1 \<and> cmod (x - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k)
[PROOF STEP]
using \<open>R > 0\<close> *[of z'] ** \<open>k > 1\<close> \<open>z \<in> unit_disc\<close> z'
[PROOF STATE]
proof (prove)
using this:
0 < R
cmod z' < 1 \<Longrightarrow> 0 < 1 - (cmod z')\<^sup>2
cor k \<noteq> 0
1 < k
z \<in> unit_disc
z = of_complex z'
cmod z' < 1

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2) = (cmod x < 1 \<and> cmod (x - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k)
[PROOF STEP]
using real_sqrt_unique[of ?a ?b, symmetric]
[PROOF STATE]
proof (prove)
using this:
0 < R
cmod z' < 1 \<Longrightarrow> 0 < 1 - (cmod z')\<^sup>2
cor k \<noteq> 0
1 < k
z \<in> unit_disc
z = of_complex z'
cmod z' < 1
\<lbrakk>(cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2; 0 \<le> cmod (x - z' / cor k)\<rbrakk> \<Longrightarrow> cmod (x - z' / cor k) = sqrt ((1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2)

goal (1 subgoal):
 1. (cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2) = (cmod x < 1 \<and> cmod (x - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k)
[PROOF STEP]
by (auto simp add: real_sqrt_divide real_sqrt_mult power_divide power_mult_distrib)
[PROOF STATE]
proof (state)
this:
(cmod x < 1 \<and> (cmod (x - z' / cor k))\<^sup>2 = (1 - (cmod z')\<^sup>2)\<^sup>2 * R * (R + 1) / k\<^sup>2) = (cmod x < 1 \<and> cmod (x - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> cmod (x - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k)
[PROOF STEP]
have "of_complex x \<in> poincare_circle z r \<longleftrightarrow> cmod x < 1 \<and> x \<in> circle (z'/k) (?cz * sqrt(R * (R+1)) / k)"
[PROOF STATE]
proof (prove)
using this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> cmod (x - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k)

goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> x \<in> circle (z' / cor k) ((1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k))
[PROOF STEP]
unfolding circle_def z' k R
[PROOF STATE]
proof (prove)
using this:
(of_complex x \<in> poincare_circle (of_complex z') r) = (cmod x < 1 \<and> cmod (x - z' / cor (1 + (cosh r - 1) / 2 * (1 - (cmod z')\<^sup>2))) = (1 - (cmod z')\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / (1 + (cosh r - 1) / 2 * (1 - (cmod z')\<^sup>2)))

goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle (of_complex z') r) = (cmod x < 1 \<and> x \<in> {z. cmod (z - z' / cor (1 + (cosh r - 1) / 2 * (1 - (cmod z')\<^sup>2))) = (1 - (cmod z')\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / (1 + (cosh r - 1) / 2 * (1 - (cmod z')\<^sup>2))})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> x \<in> circle (z' / cor k) ((1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k))

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
hence "of_complex x \<in> poincare_circle z r \<longleftrightarrow> (let (Ze, Re) = poincare_circle_euclidean z r in cmod x < 1 \<and> x \<in> circle Ze Re)"
[PROOF STATE]
proof (prove)
using this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> x \<in> circle (z' / cor k) ((1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k))

goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in cmod x < 1 \<and> x \<in> circle Ze Re)
[PROOF STEP]
unfolding poincare_circle_euclidean_def Let_def circle_def
[PROOF STATE]
proof (prove)
using this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> x \<in> {z. cmod (z - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k})

goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle z r) = (case (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1), (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) of (Ze, Re) \<Rightarrow> cmod x < 1 \<and> x \<in> {z. cmod (z - Ze) = Re})
[PROOF STEP]
using z' R k
[PROOF STATE]
proof (prove)
using this:
(of_complex x \<in> poincare_circle z r) = (cmod x < 1 \<and> x \<in> {z. cmod (z - z' / cor k) = (1 - (cmod z')\<^sup>2) * sqrt (R * (R + 1)) / k})
z = of_complex z'
cmod z' < 1
R = (cosh r - 1) / 2
k = 1 + R * (1 - (cmod z')\<^sup>2)

goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle z r) = (case (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1), (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) of (Ze, Re) \<Rightarrow> cmod x < 1 \<and> x \<in> {z. cmod (z - Ze) = Re})
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in cmod x < 1 \<and> x \<in> circle Ze Re)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
hence "of_complex x \<in> poincare_circle z r \<longleftrightarrow> (let (Ze, Re) = poincare_circle_euclidean z r in x \<in> circle Ze Re)"
[PROOF STATE]
proof (prove)
using this:
(of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in cmod x < 1 \<and> x \<in> circle Ze Re)

goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in x \<in> circle Ze Re)
[PROOF STEP]
using poincare_circle_in_disc[OF \<open>r > 0\<close> \<open>z \<in> unit_disc\<close>]
[PROOF STATE]
proof (prove)
using this:
(of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in cmod x < 1 \<and> x \<in> circle Ze Re)
(?ze, ?re) = poincare_circle_euclidean z r \<Longrightarrow> cmod ?ze < 1
(?ze, ?re) = poincare_circle_euclidean z r \<Longrightarrow> 0 < ?re
(?ze, ?re) = poincare_circle_euclidean z r \<Longrightarrow> \<forall>x\<in>circle ?ze ?re. cmod x < 1

goal (1 subgoal):
 1. (of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in x \<in> circle Ze Re)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in x \<in> circle Ze Re)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(of_complex ?x2 \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in ?x2 \<in> circle Ze Re)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
(of_complex ?x2 \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in ?x2 \<in> circle Ze Re)

goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case poincare_circle_euclidean z r of (Ze, Re) \<Rightarrow> of_complex ` circle Ze Re = poincare_circle z r
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ze Re x xa. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); xa \<in> circle Ze Re\<rbrakk> \<Longrightarrow> of_complex xa \<in> poincare_circle z r
 2. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
fix Ze Re x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ze Re x xa. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); xa \<in> circle Ze Re\<rbrakk> \<Longrightarrow> of_complex xa \<in> poincare_circle z r
 2. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
assume "poincare_circle_euclidean z r = (Ze, Re)" "x \<in> circle Ze Re"
[PROOF STATE]
proof (state)
this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> circle Ze Re

goal (2 subgoals):
 1. \<And>Ze Re x xa. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); xa \<in> circle Ze Re\<rbrakk> \<Longrightarrow> of_complex xa \<in> poincare_circle z r
 2. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
thus "of_complex x \<in> poincare_circle z r"
[PROOF STATE]
proof (prove)
using this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> circle Ze Re

goal (1 subgoal):
 1. of_complex x \<in> poincare_circle z r
[PROOF STEP]
using *[of x]
[PROOF STATE]
proof (prove)
using this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> circle Ze Re
(of_complex x \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in x \<in> circle Ze Re)

goal (1 subgoal):
 1. of_complex x \<in> poincare_circle z r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_complex x \<in> poincare_circle z r

goal (1 subgoal):
 1. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
fix Ze Re x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
assume **: "poincare_circle_euclidean z r = (Ze, Re)" "x \<in> poincare_circle z r"
[PROOF STATE]
proof (state)
this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> poincare_circle z r

goal (1 subgoal):
 1. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> poincare_circle z r
[PROOF STEP]
obtain x' where x': "x = of_complex x'"
[PROOF STATE]
proof (prove)
using this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> poincare_circle z r

goal (1 subgoal):
 1. (\<And>x'. x = of_complex x' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding poincare_circle_def
[PROOF STATE]
proof (prove)
using this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> {z' \<in> unit_disc. poincare_distance z z' = r}

goal (1 subgoal):
 1. (\<And>x'. x = of_complex x' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of x]
[PROOF STATE]
proof (prove)
using this:
poincare_circle_euclidean z r = (Ze, Re)
x \<in> {z' \<in> unit_disc. poincare_distance z z' = r}
x = \<infinity>\<^sub>h \<or> (\<exists>xa. x = of_complex xa)

goal (1 subgoal):
 1. (\<And>x'. x = of_complex x' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = of_complex x'

goal (1 subgoal):
 1. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
hence "x' \<in> circle Ze Re"
[PROOF STATE]
proof (prove)
using this:
x = of_complex x'

goal (1 subgoal):
 1. x' \<in> circle Ze Re
[PROOF STEP]
using *[of x'] **
[PROOF STATE]
proof (prove)
using this:
x = of_complex x'
(of_complex x' \<in> poincare_circle z r) = (let (Ze, Re) = poincare_circle_euclidean z r in x' \<in> circle Ze Re)
poincare_circle_euclidean z r = (Ze, Re)
x \<in> poincare_circle z r

goal (1 subgoal):
 1. x' \<in> circle Ze Re
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' \<in> circle Ze Re

goal (1 subgoal):
 1. \<And>Ze Re x. \<lbrakk>poincare_circle_euclidean z r = (Ze, Re); x \<in> poincare_circle z r\<rbrakk> \<Longrightarrow> x \<in> of_complex ` circle Ze Re
[PROOF STEP]
thus "x \<in> of_complex ` circle Ze Re"
[PROOF STATE]
proof (prove)
using this:
x' \<in> circle Ze Re

goal (1 subgoal):
 1. x \<in> of_complex ` circle Ze Re
[PROOF STEP]
using x'
[PROOF STATE]
proof (prove)
using this:
x' \<in> circle Ze Re
x = of_complex x'

goal (1 subgoal):
 1. x \<in> of_complex ` circle Ze Re
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> of_complex ` circle Ze Re

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
let (Ze, Re) = poincare_circle_euclidean z r in of_complex ` circle Ze Re = poincare_circle z r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma intersect_poincare_circles_x_axis:
  assumes z: "is_real z1" and "is_real z2" and "r1 > 0" and "r2 > 0" and
             "-1 < Re z1" and "Re z1 < 1" and "-1 < Re z2" and "Re z2 < 1" and
             "z1 \<noteq> z2"
  assumes x1: "x1 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2" and
          x2: "x2 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2" and
              "x1 \<noteq> x2"
  shows "x1 = conjugate x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
have in_disc: "of_complex z1 \<in> unit_disc" "of_complex z2 \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex z1 \<in> unit_disc &&& of_complex z2 \<in> unit_disc
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real z1
is_real z2
0 < r1
0 < r2
- 1 < Re z1
Re z1 < 1
- 1 < Re z2
Re z2 < 1
z1 \<noteq> z2
x1 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2
x2 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2
x1 \<noteq> x2

goal (1 subgoal):
 1. of_complex z1 \<in> unit_disc &&& of_complex z2 \<in> unit_disc
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
of_complex z1 \<in> unit_disc
of_complex z2 \<in> unit_disc

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
obtain x1' x2' where x': "x1 = of_complex x1'" "x2 = of_complex x2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1' x2'. \<lbrakk>x1 = of_complex x1'; x2 = of_complex x2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x1 x2
[PROOF STATE]
proof (prove)
using this:
x1 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2
x2 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2

goal (1 subgoal):
 1. (\<And>x1' x2'. \<lbrakk>x1 = of_complex x1'; x2 = of_complex x2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of x1] inf_or_of_complex[of x2]
[PROOF STATE]
proof (prove)
using this:
x1 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2
x2 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2
x1 = \<infinity>\<^sub>h \<or> (\<exists>x. x1 = of_complex x)
x2 = \<infinity>\<^sub>h \<or> (\<exists>x. x2 = of_complex x)

goal (1 subgoal):
 1. (\<And>x1' x2'. \<lbrakk>x1 = of_complex x1'; x2 = of_complex x2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding poincare_circle_def
[PROOF STATE]
proof (prove)
using this:
x1 \<in> {z' \<in> unit_disc. poincare_distance (of_complex z1) z' = r1} \<inter> {z' \<in> unit_disc. poincare_distance (of_complex z2) z' = r2}
x2 \<in> {z' \<in> unit_disc. poincare_distance (of_complex z1) z' = r1} \<inter> {z' \<in> unit_disc. poincare_distance (of_complex z2) z' = r2}
x1 = \<infinity>\<^sub>h \<or> (\<exists>x. x1 = of_complex x)
x2 = \<infinity>\<^sub>h \<or> (\<exists>x. x2 = of_complex x)

goal (1 subgoal):
 1. (\<And>x1' x2'. \<lbrakk>x1 = of_complex x1'; x2 = of_complex x2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 = of_complex x1'
x2 = of_complex x2'

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
obtain Ze1 Re1 where 1: "(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ze1 Re1. (Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis poincare_circle_euclidean_def)
[PROOF STATE]
proof (state)
this:
(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
obtain Ze2 Re2 where 2: "(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ze2 Re2. (Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis poincare_circle_euclidean_def)
[PROOF STATE]
proof (state)
this:
(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
have circle: "x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2"  "x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2 &&& x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
[PROOF STEP]
using poincare_circle_is_euclidean_circle[of "of_complex z1" r1]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>of_complex z1 \<in> unit_disc; 0 < r1\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean (of_complex z1) r1 in of_complex ` circle Ze Re = poincare_circle (of_complex z1) r1

goal (1 subgoal):
 1. x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2 &&& x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
[PROOF STEP]
using poincare_circle_is_euclidean_circle[of "of_complex z2" r2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>of_complex z1 \<in> unit_disc; 0 < r1\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean (of_complex z1) r1 in of_complex ` circle Ze Re = poincare_circle (of_complex z1) r1
\<lbrakk>of_complex z2 \<in> unit_disc; 0 < r2\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean (of_complex z2) r2 in of_complex ` circle Ze Re = poincare_circle (of_complex z2) r2

goal (1 subgoal):
 1. x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2 &&& x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
[PROOF STEP]
using assms 1 2 \<open>of_complex z1 \<in> unit_disc\<close> \<open>of_complex z2 \<in> unit_disc\<close> x'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>of_complex z1 \<in> unit_disc; 0 < r1\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean (of_complex z1) r1 in of_complex ` circle Ze Re = poincare_circle (of_complex z1) r1
\<lbrakk>of_complex z2 \<in> unit_disc; 0 < r2\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean (of_complex z2) r2 in of_complex ` circle Ze Re = poincare_circle (of_complex z2) r2
is_real z1
is_real z2
0 < r1
0 < r2
- 1 < Re z1
Re z1 < 1
- 1 < Re z2
Re z2 < 1
z1 \<noteq> z2
x1 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2
x2 \<in> poincare_circle (of_complex z1) r1 \<inter> poincare_circle (of_complex z2) r2
x1 \<noteq> x2
(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1
(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2
of_complex z1 \<in> unit_disc
of_complex z2 \<in> unit_disc
x1 = of_complex x1'
x2 = of_complex x2'

goal (1 subgoal):
 1. x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2 &&& x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
[PROOF STEP]
by auto (metis image_iff of_complex_inj)+
[PROOF STATE]
proof (state)
this:
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
have "is_real Ze1" "is_real Ze2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real Ze1 &&& is_real Ze2
[PROOF STEP]
using 1 2 \<open>is_real z1\<close> \<open>is_real z2\<close>
[PROOF STATE]
proof (prove)
using this:
(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1
(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2
is_real z1
is_real z2

goal (1 subgoal):
 1. is_real Ze1 &&& is_real Ze2
[PROOF STEP]
by (simp_all add: poincare_circle_euclidean_def Let_def)
[PROOF STATE]
proof (state)
this:
is_real Ze1
is_real Ze2

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
have "Re1 > 0" "Re2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Re1 &&& 0 < Re2
[PROOF STEP]
using 1 2 in_disc \<open>r1 > 0\<close> \<open>r2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1
(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2
of_complex z1 \<in> unit_disc
of_complex z2 \<in> unit_disc
0 < r1
0 < r2

goal (1 subgoal):
 1. 0 < Re1 &&& 0 < Re2
[PROOF STEP]
using poincare_circle_in_disc(2)[of r1 "of_complex z1" Ze1 Re1]
[PROOF STATE]
proof (prove)
using this:
(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1
(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2
of_complex z1 \<in> unit_disc
of_complex z2 \<in> unit_disc
0 < r1
0 < r2
\<lbrakk>0 < r1; of_complex z1 \<in> unit_disc; (Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1\<rbrakk> \<Longrightarrow> 0 < Re1

goal (1 subgoal):
 1. 0 < Re1 &&& 0 < Re2
[PROOF STEP]
using poincare_circle_in_disc(2)[of r2 "of_complex z2" Ze2 Re2]
[PROOF STATE]
proof (prove)
using this:
(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1
(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2
of_complex z1 \<in> unit_disc
of_complex z2 \<in> unit_disc
0 < r1
0 < r2
\<lbrakk>0 < r1; of_complex z1 \<in> unit_disc; (Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1\<rbrakk> \<Longrightarrow> 0 < Re1
\<lbrakk>0 < r2; of_complex z2 \<in> unit_disc; (Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2\<rbrakk> \<Longrightarrow> 0 < Re2

goal (1 subgoal):
 1. 0 < Re1 &&& 0 < Re2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < Re1
0 < Re2

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
have "Ze1 \<noteq> Ze2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ze1 \<noteq> Ze2
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> Ze1 \<noteq> Ze2

goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
hence eq: "Ze1 = Ze2" "Re1 = Re2"
[PROOF STATE]
proof (prove)
using this:
\<not> Ze1 \<noteq> Ze2

goal (1 subgoal):
 1. Ze1 = Ze2 &&& Re1 = Re2
[PROOF STEP]
using circle(1)
[PROOF STATE]
proof (prove)
using this:
\<not> Ze1 \<noteq> Ze2
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2

goal (1 subgoal):
 1. Ze1 = Ze2 &&& Re1 = Re2
[PROOF STEP]
unfolding circle_def
[PROOF STATE]
proof (prove)
using this:
\<not> Ze1 \<noteq> Ze2
x1' \<in> {z. cmod (z - Ze1) = Re1} \<inter> {z. cmod (z - Ze2) = Re2}

goal (1 subgoal):
 1. Ze1 = Ze2 &&& Re1 = Re2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ze1 = Ze2
Re1 = Re2

goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
let ?A = "Ze1 - Re1" and ?B = "Ze1 + Re1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
have "?A \<in> circle Ze1 Re1" "?B \<in> circle Ze1 Re1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ze1 - cor Re1 \<in> circle Ze1 Re1 &&& Ze1 + cor Re1 \<in> circle Ze1 Re1
[PROOF STEP]
using \<open>Re1 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Re1

goal (1 subgoal):
 1. Ze1 - cor Re1 \<in> circle Ze1 Re1 &&& Ze1 + cor Re1 \<in> circle Ze1 Re1
[PROOF STEP]
unfolding circle_def
[PROOF STATE]
proof (prove)
using this:
0 < Re1

goal (1 subgoal):
 1. Ze1 - cor Re1 \<in> {z. cmod (z - Ze1) = Re1} &&& Ze1 + cor Re1 \<in> {z. cmod (z - Ze1) = Re1}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Ze1 - cor Re1 \<in> circle Ze1 Re1
Ze1 + cor Re1 \<in> circle Ze1 Re1

goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
hence "of_complex ?A \<in> poincare_circle (of_complex z1) r1" "of_complex ?B \<in> poincare_circle (of_complex z1) r1"
          "of_complex ?A \<in> poincare_circle (of_complex z2) r2" "of_complex ?B \<in> poincare_circle (of_complex z2) r2"
[PROOF STATE]
proof (prove)
using this:
Ze1 - cor Re1 \<in> circle Ze1 Re1
Ze1 + cor Re1 \<in> circle Ze1 Re1

goal (1 subgoal):
 1. (of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1) &&& of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
Ze1 - cor Re1 \<in> circle Ze1 Re1
Ze1 + cor Re1 \<in> circle Ze1 Re1
Ze1 = Ze2
Re1 = Re2

goal (1 subgoal):
 1. (of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1) &&& of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2
[PROOF STEP]
using poincare_circle_is_euclidean_circle[OF \<open>of_complex z1 \<in> unit_disc\<close> \<open>r1 > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
Ze1 - cor Re1 \<in> circle Ze1 Re1
Ze1 + cor Re1 \<in> circle Ze1 Re1
Ze1 = Ze2
Re1 = Re2
let (Ze, Re) = poincare_circle_euclidean (of_complex z1) r1 in of_complex ` circle Ze Re = poincare_circle (of_complex z1) r1

goal (1 subgoal):
 1. (of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1) &&& of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2
[PROOF STEP]
using poincare_circle_is_euclidean_circle[OF \<open>of_complex z2 \<in> unit_disc\<close> \<open>r2 > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
Ze1 - cor Re1 \<in> circle Ze1 Re1
Ze1 + cor Re1 \<in> circle Ze1 Re1
Ze1 = Ze2
Re1 = Re2
let (Ze, Re) = poincare_circle_euclidean (of_complex z1) r1 in of_complex ` circle Ze Re = poincare_circle (of_complex z1) r1
let (Ze, Re) = poincare_circle_euclidean (of_complex z2) r2 in of_complex ` circle Ze Re = poincare_circle (of_complex z2) r2

goal (1 subgoal):
 1. (of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1) &&& of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
Ze1 - cor Re1 \<in> circle Ze1 Re1
Ze1 + cor Re1 \<in> circle Ze1 Re1
Ze1 = Ze2
Re1 = Re2
let (Ze, Re) = poincare_circle_euclidean (of_complex z1) r1 in of_complex ` circle Ze Re = poincare_circle (of_complex z1) r1
let (Ze, Re) = poincare_circle_euclidean (of_complex z2) r2 in of_complex ` circle Ze Re = poincare_circle (of_complex z2) r2
(Ze1, Re1) = poincare_circle_euclidean (of_complex z1) r1
(Ze2, Re2) = poincare_circle_euclidean (of_complex z2) r2

goal (1 subgoal):
 1. (of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1) &&& of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2 &&& of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2
[PROOF STEP]
by auto blast+
[PROOF STATE]
proof (state)
this:
of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1
of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1
of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2
of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2

goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
hence "poincare_distance (of_complex z1) (of_complex ?A) = poincare_distance (of_complex z1) (of_complex ?B)"
          "poincare_distance (of_complex z2) (of_complex ?A) = poincare_distance (of_complex z2) (of_complex ?B)"
          "-1 < Re (Ze1 - Re1)" "Re (Ze1 - Re1) < 1" "-1 < Re (Ze1 + Re1)" "Re (Ze1 + Re1) < 1"
[PROOF STATE]
proof (prove)
using this:
of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1
of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1
of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2
of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2

goal (1 subgoal):
 1. (poincare_distance (of_complex z1) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z1) (of_complex (Ze1 + cor Re1)) &&& poincare_distance (of_complex z2) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z2) (of_complex (Ze1 + cor Re1)) &&& - 1 < Re (Ze1 - cor Re1)) &&& Re (Ze1 - cor Re1) < 1 &&& - 1 < Re (Ze1 + cor Re1) &&& Re (Ze1 + cor Re1) < 1
[PROOF STEP]
using \<open>is_real Ze1\<close> \<open>is_real Ze2\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z1) r1
of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z1) r1
of_complex (Ze1 - cor Re1) \<in> poincare_circle (of_complex z2) r2
of_complex (Ze1 + cor Re1) \<in> poincare_circle (of_complex z2) r2
is_real Ze1
is_real Ze2

goal (1 subgoal):
 1. (poincare_distance (of_complex z1) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z1) (of_complex (Ze1 + cor Re1)) &&& poincare_distance (of_complex z2) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z2) (of_complex (Ze1 + cor Re1)) &&& - 1 < Re (Ze1 - cor Re1)) &&& Re (Ze1 - cor Re1) < 1 &&& - 1 < Re (Ze1 + cor Re1) &&& Re (Ze1 + cor Re1) < 1
[PROOF STEP]
unfolding poincare_circle_def
[PROOF STATE]
proof (prove)
using this:
of_complex (Ze1 - cor Re1) \<in> {z' \<in> unit_disc. poincare_distance (of_complex z1) z' = r1}
of_complex (Ze1 + cor Re1) \<in> {z' \<in> unit_disc. poincare_distance (of_complex z1) z' = r1}
of_complex (Ze1 - cor Re1) \<in> {z' \<in> unit_disc. poincare_distance (of_complex z2) z' = r2}
of_complex (Ze1 + cor Re1) \<in> {z' \<in> unit_disc. poincare_distance (of_complex z2) z' = r2}
is_real Ze1
is_real Ze2

goal (1 subgoal):
 1. (poincare_distance (of_complex z1) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z1) (of_complex (Ze1 + cor Re1)) &&& poincare_distance (of_complex z2) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z2) (of_complex (Ze1 + cor Re1)) &&& - 1 < Re (Ze1 - cor Re1)) &&& Re (Ze1 - cor Re1) < 1 &&& - 1 < Re (Ze1 + cor Re1) &&& Re (Ze1 + cor Re1) < 1
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
poincare_distance (of_complex z1) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z1) (of_complex (Ze1 + cor Re1))
poincare_distance (of_complex z2) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z2) (of_complex (Ze1 + cor Re1))
- 1 < Re (Ze1 - cor Re1)
Re (Ze1 - cor Re1) < 1
- 1 < Re (Ze1 + cor Re1)
Re (Ze1 + cor Re1) < 1

goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
hence "z1 = z2"
[PROOF STATE]
proof (prove)
using this:
poincare_distance (of_complex z1) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z1) (of_complex (Ze1 + cor Re1))
poincare_distance (of_complex z2) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z2) (of_complex (Ze1 + cor Re1))
- 1 < Re (Ze1 - cor Re1)
Re (Ze1 - cor Re1) < 1
- 1 < Re (Ze1 + cor Re1)
Re (Ze1 + cor Re1) < 1

goal (1 subgoal):
 1. z1 = z2
[PROOF STEP]
using unique_midpoint_x_axis[of "Ze1 - Re1" "Ze1 + Re1"]
[PROOF STATE]
proof (prove)
using this:
poincare_distance (of_complex z1) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z1) (of_complex (Ze1 + cor Re1))
poincare_distance (of_complex z2) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z2) (of_complex (Ze1 + cor Re1))
- 1 < Re (Ze1 - cor Re1)
Re (Ze1 - cor Re1) < 1
- 1 < Re (Ze1 + cor Re1)
Re (Ze1 + cor Re1) < 1
\<lbrakk>is_real (Ze1 - cor Re1); - 1 < Re (Ze1 - cor Re1); Re (Ze1 - cor Re1) < 1; is_real (Ze1 + cor Re1); - 1 < Re (Ze1 + cor Re1); Re (Ze1 + cor Re1) < 1; Ze1 - cor Re1 \<noteq> Ze1 + cor Re1\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z) (of_complex (Ze1 + cor Re1))

goal (1 subgoal):
 1. z1 = z2
[PROOF STEP]
using \<open>is_real Ze1\<close> \<open>is_real z1\<close> \<open>is_real z2\<close> \<open>Re1 > 0\<close> \<open>-1 < Re z1\<close> \<open>Re z1 < 1\<close> \<open>-1 < Re z2\<close> \<open>Re z2 < 1\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_distance (of_complex z1) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z1) (of_complex (Ze1 + cor Re1))
poincare_distance (of_complex z2) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z2) (of_complex (Ze1 + cor Re1))
- 1 < Re (Ze1 - cor Re1)
Re (Ze1 - cor Re1) < 1
- 1 < Re (Ze1 + cor Re1)
Re (Ze1 + cor Re1) < 1
\<lbrakk>is_real (Ze1 - cor Re1); - 1 < Re (Ze1 - cor Re1); Re (Ze1 - cor Re1) < 1; is_real (Ze1 + cor Re1); - 1 < Re (Ze1 + cor Re1); Re (Ze1 + cor Re1) < 1; Ze1 - cor Re1 \<noteq> Ze1 + cor Re1\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex (Ze1 - cor Re1)) = poincare_distance (of_complex z) (of_complex (Ze1 + cor Re1))
is_real Ze1
is_real z1
is_real z2
0 < Re1
- 1 < Re z1
Re z1 < 1
- 1 < Re z2
Re z2 < 1

goal (1 subgoal):
 1. z1 = z2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z1 = z2

goal (1 subgoal):
 1. \<not> Ze1 \<noteq> Ze2 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
z1 = z2

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>z1 \<noteq> z2\<close>
[PROOF STATE]
proof (prove)
using this:
z1 = z2
z1 \<noteq> z2

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ze1 \<noteq> Ze2

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
hence *: "(Re x1')\<^sup>2 + (Im x1')\<^sup>2 - 2 * Re x1' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0"
           "(Re x1')\<^sup>2 + (Im x1')\<^sup>2 - 2 * Re x1' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0"
           "(Re x2')\<^sup>2 + (Im x2')\<^sup>2 - 2 * Re x2' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0"
           "(Re x2')\<^sup>2 + (Im x2')\<^sup>2 - 2 * Re x2' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0"
[PROOF STATE]
proof (prove)
using this:
Ze1 \<noteq> Ze2

goal (1 subgoal):
 1. (cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0) &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
[PROOF STEP]
using circle_equation[of Re1 Ze1] circle_equation[of Re2 Ze2] circle
[PROOF STATE]
proof (prove)
using this:
Ze1 \<noteq> Ze2
0 \<le> Re1 \<Longrightarrow> circle Ze1 Re1 = {z. z * cnj z - z * cnj Ze1 - cnj z * Ze1 + Ze1 * cnj Ze1 - cor (Re1 * Re1) = 0}
0 \<le> Re2 \<Longrightarrow> circle Ze2 Re2 = {z. z * cnj z - z * cnj Ze2 - cnj z * Ze2 + Ze2 * cnj Ze2 - cor (Re2 * Re2) = 0}
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2

goal (1 subgoal):
 1. (cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0) &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
[PROOF STEP]
using eq_cnj_iff_real[of Ze1] \<open>is_real Ze1\<close> \<open>Re1 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
Ze1 \<noteq> Ze2
0 \<le> Re1 \<Longrightarrow> circle Ze1 Re1 = {z. z * cnj z - z * cnj Ze1 - cnj z * Ze1 + Ze1 * cnj Ze1 - cor (Re1 * Re1) = 0}
0 \<le> Re2 \<Longrightarrow> circle Ze2 Re2 = {z. z * cnj z - z * cnj Ze2 - cnj z * Ze2 + Ze2 * cnj Ze2 - cor (Re2 * Re2) = 0}
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
(cnj Ze1 = Ze1) = is_real Ze1
is_real Ze1
0 < Re1

goal (1 subgoal):
 1. (cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0) &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
[PROOF STEP]
using eq_cnj_iff_real[of Ze2] \<open>is_real Ze2\<close> \<open>Re2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
Ze1 \<noteq> Ze2
0 \<le> Re1 \<Longrightarrow> circle Ze1 Re1 = {z. z * cnj z - z * cnj Ze1 - cnj z * Ze1 + Ze1 * cnj Ze1 - cor (Re1 * Re1) = 0}
0 \<le> Re2 \<Longrightarrow> circle Ze2 Re2 = {z. z * cnj z - z * cnj Ze2 - cnj z * Ze2 + Ze2 * cnj Ze2 - cor (Re2 * Re2) = 0}
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
(cnj Ze1 = Ze1) = is_real Ze1
is_real Ze1
0 < Re1
(cnj Ze2 = Ze2) = is_real Ze2
is_real Ze2
0 < Re2

goal (1 subgoal):
 1. (cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0) &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
[PROOF STEP]
using complex_add_cnj[of x1']  complex_add_cnj[of x2']
[PROOF STATE]
proof (prove)
using this:
Ze1 \<noteq> Ze2
0 \<le> Re1 \<Longrightarrow> circle Ze1 Re1 = {z. z * cnj z - z * cnj Ze1 - cnj z * Ze1 + Ze1 * cnj Ze1 - cor (Re1 * Re1) = 0}
0 \<le> Re2 \<Longrightarrow> circle Ze2 Re2 = {z. z * cnj z - z * cnj Ze2 - cnj z * Ze2 + Ze2 * cnj Ze2 - cor (Re2 * Re2) = 0}
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
(cnj Ze1 = Ze1) = is_real Ze1
is_real Ze1
0 < Re1
(cnj Ze2 = Ze2) = is_real Ze2
is_real Ze2
0 < Re2
x1' + cnj x1' = cor (2 * Re x1')
x2' + cnj x2' = cor (2 * Re x2')

goal (1 subgoal):
 1. (cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0) &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
[PROOF STEP]
using distrib_left[of Ze1 x1' "cnj x1'"] distrib_left[of Ze2 x1' "cnj x1'"]
[PROOF STATE]
proof (prove)
using this:
Ze1 \<noteq> Ze2
0 \<le> Re1 \<Longrightarrow> circle Ze1 Re1 = {z. z * cnj z - z * cnj Ze1 - cnj z * Ze1 + Ze1 * cnj Ze1 - cor (Re1 * Re1) = 0}
0 \<le> Re2 \<Longrightarrow> circle Ze2 Re2 = {z. z * cnj z - z * cnj Ze2 - cnj z * Ze2 + Ze2 * cnj Ze2 - cor (Re2 * Re2) = 0}
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
(cnj Ze1 = Ze1) = is_real Ze1
is_real Ze1
0 < Re1
(cnj Ze2 = Ze2) = is_real Ze2
is_real Ze2
0 < Re2
x1' + cnj x1' = cor (2 * Re x1')
x2' + cnj x2' = cor (2 * Re x2')
Ze1 * (x1' + cnj x1') = Ze1 * x1' + Ze1 * cnj x1'
Ze2 * (x1' + cnj x1') = Ze2 * x1' + Ze2 * cnj x1'

goal (1 subgoal):
 1. (cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0) &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
[PROOF STEP]
using distrib_left[of Ze1 x2' "cnj x2'"] distrib_left[of Ze2 x2' "cnj x2'"]
[PROOF STATE]
proof (prove)
using this:
Ze1 \<noteq> Ze2
0 \<le> Re1 \<Longrightarrow> circle Ze1 Re1 = {z. z * cnj z - z * cnj Ze1 - cnj z * Ze1 + Ze1 * cnj Ze1 - cor (Re1 * Re1) = 0}
0 \<le> Re2 \<Longrightarrow> circle Ze2 Re2 = {z. z * cnj z - z * cnj Ze2 - cnj z * Ze2 + Ze2 * cnj Ze2 - cor (Re2 * Re2) = 0}
x1' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
x2' \<in> circle Ze1 Re1 \<inter> circle Ze2 Re2
(cnj Ze1 = Ze1) = is_real Ze1
is_real Ze1
0 < Re1
(cnj Ze2 = Ze2) = is_real Ze2
is_real Ze2
0 < Re2
x1' + cnj x1' = cor (2 * Re x1')
x2' + cnj x2' = cor (2 * Re x2')
Ze1 * (x1' + cnj x1') = Ze1 * x1' + Ze1 * cnj x1'
Ze2 * (x1' + cnj x1') = Ze2 * x1' + Ze2 * cnj x1'
Ze1 * (x2' + cnj x2') = Ze1 * x2' + Ze1 * cnj x2'
Ze2 * (x2' + cnj x2') = Ze2 * x2' + Ze2 * cnj x2'

goal (1 subgoal):
 1. (cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0) &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0 &&& cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
[PROOF STEP]
by (auto simp add: complex_mult_cnj power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0
cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0
cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
hence "- 2 * Re x1' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = - 2 * Re x1' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)"
        "- 2 * Re x2' * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = - 2 * Re x2' * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)"
[PROOF STATE]
proof (prove)
using this:
cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0
cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0
cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0
cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) = 0

goal (1 subgoal):
 1. cor (- 2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = cor (- 2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2) &&& cor (- 2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = cor (- 2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)
[PROOF STEP]
by (smt add_diff_cancel_right' add_diff_eq eq_iff_diff_eq_0 minus_diff_eq mult_minus_left of_real_minus)+
[PROOF STATE]
proof (state)
this:
cor (- 2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = cor (- 2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)
cor (- 2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = cor (- 2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
hence "2 * Re x1' * (Ze2 - Ze1) =  (Ze2 * Ze2 - cor (Re2 * Re2)) - (Ze1 * Ze1 - cor (Re1 * Re1))"
        "2 * Re x2' * (Ze2 - Ze1) =  (Ze2 * Ze2 - cor (Re2 * Re2)) - (Ze1 * Ze1 - cor (Re1 * Re1))"
[PROOF STATE]
proof (prove)
using this:
cor (- 2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = cor (- 2 * Re x1') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)
cor (- 2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = cor (- 2 * Re x2') * Ze2 + Ze2 * Ze2 - cor (Re2 * Re2)

goal (1 subgoal):
 1. cor (2 * Re x1') * (Ze2 - Ze1) = Ze2 * Ze2 - cor (Re2 * Re2) - (Ze1 * Ze1 - cor (Re1 * Re1)) &&& cor (2 * Re x2') * (Ze2 - Ze1) = Ze2 * Ze2 - cor (Re2 * Re2) - (Ze1 * Ze1 - cor (Re1 * Re1))
[PROOF STEP]
by simp_all (simp add: field_simps)+
[PROOF STATE]
proof (state)
this:
cor (2 * Re x1') * (Ze2 - Ze1) = Ze2 * Ze2 - cor (Re2 * Re2) - (Ze1 * Ze1 - cor (Re1 * Re1))
cor (2 * Re x2') * (Ze2 - Ze1) = Ze2 * Ze2 - cor (Re2 * Re2) - (Ze1 * Ze1 - cor (Re1 * Re1))

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
hence "2 * Re x1' * (Ze2 - Ze1) = 2 * Re x2' * (Ze2 - Ze1)"
[PROOF STATE]
proof (prove)
using this:
cor (2 * Re x1') * (Ze2 - Ze1) = Ze2 * Ze2 - cor (Re2 * Re2) - (Ze1 * Ze1 - cor (Re1 * Re1))
cor (2 * Re x2') * (Ze2 - Ze1) = Ze2 * Ze2 - cor (Re2 * Re2) - (Ze1 * Ze1 - cor (Re1 * Re1))

goal (1 subgoal):
 1. cor (2 * Re x1') * (Ze2 - Ze1) = cor (2 * Re x2') * (Ze2 - Ze1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cor (2 * Re x1') * (Ze2 - Ze1) = cor (2 * Re x2') * (Ze2 - Ze1)

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
hence "Re x1' = Re x2'"
[PROOF STATE]
proof (prove)
using this:
cor (2 * Re x1') * (Ze2 - Ze1) = cor (2 * Re x2') * (Ze2 - Ze1)

goal (1 subgoal):
 1. Re x1' = Re x2'
[PROOF STEP]
using \<open>Ze1 \<noteq> Ze2\<close>
[PROOF STATE]
proof (prove)
using this:
cor (2 * Re x1') * (Ze2 - Ze1) = cor (2 * Re x2') * (Ze2 - Ze1)
Ze1 \<noteq> Ze2

goal (1 subgoal):
 1. Re x1' = Re x2'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Re x1' = Re x2'

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Re x1' = Re x2'

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
hence "(Im x1')\<^sup>2 = (Im x2')\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
Re x1' = Re x2'

goal (1 subgoal):
 1. (Im x1')\<^sup>2 = (Im x2')\<^sup>2
[PROOF STEP]
using *(1) *(3)
[PROOF STATE]
proof (prove)
using this:
Re x1' = Re x2'
cor ((Re x1')\<^sup>2 + (Im x1')\<^sup>2) - cor (2 * Re x1') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0
cor ((Re x2')\<^sup>2 + (Im x2')\<^sup>2) - cor (2 * Re x2') * Ze1 + Ze1 * Ze1 - cor (Re1 * Re1) = 0

goal (1 subgoal):
 1. (Im x1')\<^sup>2 = (Im x2')\<^sup>2
[PROOF STEP]
by (simp add: \<open>is_real Ze1\<close> complex_eq_if_Re_eq)
[PROOF STATE]
proof (state)
this:
(Im x1')\<^sup>2 = (Im x2')\<^sup>2

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
hence "Im x1' = Im x2' \<or> Im x1' = -Im x2'"
[PROOF STATE]
proof (prove)
using this:
(Im x1')\<^sup>2 = (Im x2')\<^sup>2

goal (1 subgoal):
 1. Im x1' = Im x2' \<or> Im x1' = - Im x2'
[PROOF STEP]
using power2_eq_iff
[PROOF STATE]
proof (prove)
using this:
(Im x1')\<^sup>2 = (Im x2')\<^sup>2
(?x\<^sup>2 = ?y\<^sup>2) = (?x = ?y \<or> ?x = - ?y)

goal (1 subgoal):
 1. Im x1' = Im x2' \<or> Im x1' = - Im x2'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Im x1' = Im x2' \<or> Im x1' = - Im x2'

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Re x1' = Re x2'
Im x1' = Im x2' \<or> Im x1' = - Im x2'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Re x1' = Re x2'
Im x1' = Im x2' \<or> Im x1' = - Im x2'

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
using x' \<open>x1 \<noteq> x2\<close>
[PROOF STATE]
proof (prove)
using this:
Re x1' = Re x2'
Im x1' = Im x2' \<or> Im x1' = - Im x2'
x1 = of_complex x1'
x2 = of_complex x2'
x1 \<noteq> x2

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
using complex.expand
[PROOF STATE]
proof (prove)
using this:
Re x1' = Re x2'
Im x1' = Im x2' \<or> Im x1' = - Im x2'
x1 = of_complex x1'
x2 = of_complex x2'
x1 \<noteq> x2
Re ?complex = Re ?complex' \<and> Im ?complex = Im ?complex' \<Longrightarrow> ?complex = ?complex'

goal (1 subgoal):
 1. x1 = conjugate x2
[PROOF STEP]
by (metis cnj.code complex_surj conjugate_of_complex)
[PROOF STATE]
proof (state)
this:
x1 = conjugate x2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma intersect_poincare_circles_conjugate_centers:
  assumes in_disc: "z1 \<in> unit_disc" "z2 \<in> unit_disc" and
          "z1 \<noteq> z2" and "z1 = conjugate z2" and "r > 0" and
          u: "u \<in> poincare_circle z1 r \<inter> poincare_circle z2 r"
  shows "is_real (to_complex u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
obtain z1e r1e z2e r2e where
   euclidean: "(z1e, r1e) = poincare_circle_euclidean z1 r"
              "(z2e, r2e) = poincare_circle_euclidean z2 r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z1e r1e z2e r2e. \<lbrakk>(z1e, r1e) = poincare_circle_euclidean z1 r; (z2e, r2e) = poincare_circle_euclidean z2 r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis poincare_circle_euclidean_def)
[PROOF STATE]
proof (state)
this:
(z1e, r1e) = poincare_circle_euclidean z1 r
(z2e, r2e) = poincare_circle_euclidean z2 r

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
obtain z1' z2' where z': "z1 = of_complex z1'" "z2 = of_complex z2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z1' z2'. \<lbrakk>z1 = of_complex z1'; z2 = of_complex z2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of z1] inf_or_of_complex[of z2] in_disc
[PROOF STATE]
proof (prove)
using this:
z1 = \<infinity>\<^sub>h \<or> (\<exists>x. z1 = of_complex x)
z2 = \<infinity>\<^sub>h \<or> (\<exists>x. z2 = of_complex x)
z1 \<in> unit_disc
z2 \<in> unit_disc

goal (1 subgoal):
 1. (\<And>z1' z2'. \<lbrakk>z1 = of_complex z1'; z2 = of_complex z2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z1 = of_complex z1'
z2 = of_complex z2'

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
obtain u' where u': "u = of_complex u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u'. u = of_complex u' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using u inf_or_of_complex[of u]
[PROOF STATE]
proof (prove)
using this:
u \<in> poincare_circle z1 r \<inter> poincare_circle z2 r
u = \<infinity>\<^sub>h \<or> (\<exists>x. u = of_complex x)

goal (1 subgoal):
 1. (\<And>u'. u = of_complex u' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: poincare_circle_def)
[PROOF STATE]
proof (state)
this:
u = of_complex u'

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
have "z1' = cnj z2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z1' = cnj z2'
[PROOF STEP]
using \<open>z1 = conjugate z2\<close> z'
[PROOF STATE]
proof (prove)
using this:
z1 = conjugate z2
z1 = of_complex z1'
z2 = of_complex z2'

goal (1 subgoal):
 1. z1' = cnj z2'
[PROOF STEP]
by (auto simp add: of_complex_inj)
[PROOF STATE]
proof (state)
this:
z1' = cnj z2'

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z1' = cnj z2'

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
let ?cz = "1 - (cmod z2')\<^sup>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
let ?den = "?cz * (cosh r - 1) / 2 + 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
have "?cz > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod z2')\<^sup>2
[PROOF STEP]
using in_disc z'
[PROOF STATE]
proof (prove)
using this:
z1 \<in> unit_disc
z2 \<in> unit_disc
z1 = of_complex z1'
z2 = of_complex z2'

goal (1 subgoal):
 1. 0 < 1 - (cmod z2')\<^sup>2
[PROOF STEP]
by (simp add: cmod_def)
[PROOF STATE]
proof (state)
this:
0 < 1 - (cmod z2')\<^sup>2

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
hence "?den \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod z2')\<^sup>2

goal (1 subgoal):
 1. 1 \<le> (1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1
[PROOF STEP]
using cosh_gt_1[OF \<open>r > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod z2')\<^sup>2
1 < cosh r

goal (1 subgoal):
 1. 1 \<le> (1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> (1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
hence "?den \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> (1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1

goal (1 subgoal):
 1. (1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1 \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1 \<noteq> 0

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
hence "cor ?den \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
(1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1 \<noteq> 0

goal (1 subgoal):
 1. cor ((1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1) \<noteq> 0
[PROOF STEP]
using of_real_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
(1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1 \<noteq> 0
(of_real ?x = (0::?'a)) = (?x = 0)

goal (1 subgoal):
 1. cor ((1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1) \<noteq> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cor ((1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1) \<noteq> 0

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
z1' = cnj z2'
cor ((1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1) \<noteq> 0
[PROOF STEP]
have "r1e = r2e" "z1e = cnj z2e" "z1e \<noteq> z2e"
[PROOF STATE]
proof (prove)
using this:
z1' = cnj z2'
cor ((1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1) \<noteq> 0

goal (1 subgoal):
 1. r1e = r2e &&& z1e = cnj z2e &&& z1e \<noteq> z2e
[PROOF STEP]
using z' euclidean \<open>z1 \<noteq> z2\<close>
[PROOF STATE]
proof (prove)
using this:
z1' = cnj z2'
cor ((1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1) \<noteq> 0
z1 = of_complex z1'
z2 = of_complex z2'
(z1e, r1e) = poincare_circle_euclidean z1 r
(z2e, r2e) = poincare_circle_euclidean z2 r
z1 \<noteq> z2

goal (1 subgoal):
 1. r1e = r2e &&& z1e = cnj z2e &&& z1e \<noteq> z2e
[PROOF STEP]
unfolding poincare_circle_euclidean_def Let_def
[PROOF STATE]
proof (prove)
using this:
z1' = cnj z2'
cor ((1 - (cmod z2')\<^sup>2) * (cosh r - 1) / 2 + 1) \<noteq> 0
z1 = of_complex z1'
z2 = of_complex z2'
(z1e, r1e) = (to_complex z1 / cor ((1 - (cmod (to_complex z1))\<^sup>2) * ((cosh r - 1) / 2) + 1), (1 - (cmod (to_complex z1))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z1))\<^sup>2) * ((cosh r - 1) / 2) + 1))
(z2e, r2e) = (to_complex z2 / cor ((1 - (cmod (to_complex z2))\<^sup>2) * ((cosh r - 1) / 2) + 1), (1 - (cmod (to_complex z2))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z2))\<^sup>2) * ((cosh r - 1) / 2) + 1))
z1 \<noteq> z2

goal (1 subgoal):
 1. r1e = r2e &&& z1e = cnj z2e &&& z1e \<noteq> z2e
[PROOF STEP]
by simp_all metis
[PROOF STATE]
proof (state)
this:
r1e = r2e
z1e = cnj z2e
z1e \<noteq> z2e

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
hence "u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e" "z2e \<noteq> cnj z2e"
[PROOF STATE]
proof (prove)
using this:
r1e = r2e
z1e = cnj z2e
z1e \<noteq> z2e

goal (1 subgoal):
 1. u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e &&& z2e \<noteq> cnj z2e
[PROOF STEP]
using euclidean u u'
[PROOF STATE]
proof (prove)
using this:
r1e = r2e
z1e = cnj z2e
z1e \<noteq> z2e
(z1e, r1e) = poincare_circle_euclidean z1 r
(z2e, r2e) = poincare_circle_euclidean z2 r
u \<in> poincare_circle z1 r \<inter> poincare_circle z2 r
u = of_complex u'

goal (1 subgoal):
 1. u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e &&& z2e \<noteq> cnj z2e
[PROOF STEP]
using poincare_circle_is_euclidean_circle[of z1 r]
[PROOF STATE]
proof (prove)
using this:
r1e = r2e
z1e = cnj z2e
z1e \<noteq> z2e
(z1e, r1e) = poincare_circle_euclidean z1 r
(z2e, r2e) = poincare_circle_euclidean z2 r
u \<in> poincare_circle z1 r \<inter> poincare_circle z2 r
u = of_complex u'
\<lbrakk>z1 \<in> unit_disc; 0 < r\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean z1 r in of_complex ` circle Ze Re = poincare_circle z1 r

goal (1 subgoal):
 1. u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e &&& z2e \<noteq> cnj z2e
[PROOF STEP]
using poincare_circle_is_euclidean_circle[of z2 r]
[PROOF STATE]
proof (prove)
using this:
r1e = r2e
z1e = cnj z2e
z1e \<noteq> z2e
(z1e, r1e) = poincare_circle_euclidean z1 r
(z2e, r2e) = poincare_circle_euclidean z2 r
u \<in> poincare_circle z1 r \<inter> poincare_circle z2 r
u = of_complex u'
\<lbrakk>z1 \<in> unit_disc; 0 < r\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean z1 r in of_complex ` circle Ze Re = poincare_circle z1 r
\<lbrakk>z2 \<in> unit_disc; 0 < r\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean z2 r in of_complex ` circle Ze Re = poincare_circle z2 r

goal (1 subgoal):
 1. u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e &&& z2e \<noteq> cnj z2e
[PROOF STEP]
using in_disc \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
r1e = r2e
z1e = cnj z2e
z1e \<noteq> z2e
(z1e, r1e) = poincare_circle_euclidean z1 r
(z2e, r2e) = poincare_circle_euclidean z2 r
u \<in> poincare_circle z1 r \<inter> poincare_circle z2 r
u = of_complex u'
\<lbrakk>z1 \<in> unit_disc; 0 < r\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean z1 r in of_complex ` circle Ze Re = poincare_circle z1 r
\<lbrakk>z2 \<in> unit_disc; 0 < r\<rbrakk> \<Longrightarrow> let (Ze, Re) = poincare_circle_euclidean z2 r in of_complex ` circle Ze Re = poincare_circle z2 r
z1 \<in> unit_disc
z2 \<in> unit_disc
0 < r

goal (1 subgoal):
 1. u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e &&& z2e \<noteq> cnj z2e
[PROOF STEP]
by auto (metis image_iff of_complex_inj)+
[PROOF STATE]
proof (state)
this:
u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e
z2e \<noteq> cnj z2e

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
hence "(cmod (u' - z2e))\<^sup>2 = (cmod(u' - cnj z2e))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
u' \<in> circle (cnj z2e) r2e \<inter> circle z2e r2e
z2e \<noteq> cnj z2e

goal (1 subgoal):
 1. (cmod (u' - z2e))\<^sup>2 = (cmod (u' - cnj z2e))\<^sup>2
[PROOF STEP]
by (simp add: circle_def)
[PROOF STATE]
proof (state)
this:
(cmod (u' - z2e))\<^sup>2 = (cmod (u' - cnj z2e))\<^sup>2

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
hence "(u' - z2e) * (cnj u' - cnj z2e) = (u' - cnj z2e) * (cnj u' - z2e)"
[PROOF STATE]
proof (prove)
using this:
(cmod (u' - z2e))\<^sup>2 = (cmod (u' - cnj z2e))\<^sup>2

goal (1 subgoal):
 1. (u' - z2e) * (cnj u' - cnj z2e) = (u' - cnj z2e) * (cnj u' - z2e)
[PROOF STEP]
by (metis complex_cnj_cnj complex_cnj_diff complex_norm_square)
[PROOF STATE]
proof (state)
this:
(u' - z2e) * (cnj u' - cnj z2e) = (u' - cnj z2e) * (cnj u' - z2e)

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
hence "(z2e - cnj z2e) * (u' - cnj u') = 0"
[PROOF STATE]
proof (prove)
using this:
(u' - z2e) * (cnj u' - cnj z2e) = (u' - cnj z2e) * (cnj u' - z2e)

goal (1 subgoal):
 1. (z2e - cnj z2e) * (u' - cnj u') = 0
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(z2e - cnj z2e) * (u' - cnj u') = 0

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(z2e - cnj z2e) * (u' - cnj u') = 0

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
using u' \<open>z2e \<noteq> cnj z2e\<close> eq_cnj_iff_real[of u']
[PROOF STATE]
proof (prove)
using this:
(z2e - cnj z2e) * (u' - cnj u') = 0
u = of_complex u'
z2e \<noteq> cnj z2e
(cnj u' = u') = is_real u'

goal (1 subgoal):
 1. is_real (to_complex u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_real (to_complex u)

goal:
No subgoals!
[PROOF STEP]
qed