[STATEMENT]
lemma poincare_distance_x_axis_x_axis:
  assumes "x \<in> unit_disc" and "y \<in> unit_disc" and "x \<in> circline_set x_axis" and "y \<in> circline_set x_axis"
  shows "poincare_distance x y =
            (let x' = to_complex x; y' = to_complex y
              in abs (ln (Re (((1 + x') * (1 - y')) / ((1 - x') * (1 + y'))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
obtain x' y' where *: "x = of_complex x'" "y = of_complex y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x' y'. \<lbrakk>x = of_complex x'; y = of_complex y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of x] inf_or_of_complex[of y] \<open>x \<in> unit_disc\<close> \<open>y \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
x = \<infinity>\<^sub>h \<or> (\<exists>xa. x = of_complex xa)
y = \<infinity>\<^sub>h \<or> (\<exists>x. y = of_complex x)
x \<in> unit_disc
y \<in> unit_disc

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

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
have "cmod x' < 1" "cmod y' < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod x' < 1 &&& cmod y' < 1
[PROOF STEP]
using \<open>x \<in> unit_disc\<close> \<open>y \<in> unit_disc\<close> *
[PROOF STATE]
proof (prove)
using this:
x \<in> unit_disc
y \<in> unit_disc
x = of_complex x'
y = of_complex y'

goal (1 subgoal):
 1. cmod x' < 1 &&& cmod y' < 1
[PROOF STEP]
by (metis unit_disc_iff_cmod_lt_1)+
[PROOF STATE]
proof (state)
this:
cmod x' < 1
cmod y' < 1

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
hence **: "x' \<noteq> 1" "x' \<noteq> 1" "y' \<noteq> -1" "y' \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
cmod x' < 1
cmod y' < 1

goal (1 subgoal):
 1. (x' \<noteq> 1 &&& x' \<noteq> 1) &&& y' \<noteq> - 1 &&& y' \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<noteq> 1
x' \<noteq> 1
y' \<noteq> - 1
y' \<noteq> 1

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
have "1 + y' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + y' \<noteq> 0
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
x' \<noteq> 1
x' \<noteq> 1
y' \<noteq> - 1
y' \<noteq> 1

goal (1 subgoal):
 1. 1 + y' \<noteq> 0
[PROOF STEP]
by (metis add.left_cancel add_neg_numeral_special(7))
[PROOF STATE]
proof (state)
this:
1 + y' \<noteq> 0

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
 2. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
 2. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
using assms(1-2)
[PROOF STATE]
proof (prove)
using this:
x = y
x \<in> unit_disc
y \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
using unit_disc_iff_cmod_lt_1[of "to_complex x"] * ** \<open>1 + y' \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
x = y
x \<in> unit_disc
y \<in> unit_disc
(of_complex (to_complex x) \<in> unit_disc) = (cmod (to_complex x) < 1)
x = of_complex x'
y = of_complex y'
x' \<noteq> 1
x' \<noteq> 1
y' \<noteq> - 1
y' \<noteq> 1
1 + y' \<noteq> 0

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
hence "poincare_line x y = x_axis"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. poincare_line x y = x_axis
[PROOF STEP]
using poincare_line_x_axis[OF assms]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
x \<noteq> y \<Longrightarrow> poincare_line x y = x_axis

goal (1 subgoal):
 1. poincare_line x y = x_axis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_line x y = x_axis

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
hence "ideal_points (poincare_line x y) = {of_complex (-1), of_complex 1}"
[PROOF STATE]
proof (prove)
using this:
poincare_line x y = x_axis

goal (1 subgoal):
 1. ideal_points (poincare_line x y) = {of_complex (- 1), of_complex 1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ideal_points (poincare_line x y) = {of_complex (- 1), of_complex 1}

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
hence "poincare_distance x y = calc_poincare_distance x (of_complex (-1)) y (of_complex 1)"
[PROOF STATE]
proof (prove)
using this:
ideal_points (poincare_line x y) = {of_complex (- 1), of_complex 1}

goal (1 subgoal):
 1. poincare_distance x y = calc_poincare_distance x (of_complex (- 1)) y (of_complex 1)
[PROOF STEP]
using poincare_distance_I assms \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (prove)
using this:
ideal_points (poincare_line x y) = {of_complex (- 1), of_complex 1}
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc; ?u \<noteq> ?v; ideal_points (poincare_line ?u ?v) = {?i1.0, ?i2.0}\<rbrakk> \<Longrightarrow> poincare_distance ?u ?v = calc_poincare_distance ?u ?i1.0 ?v ?i2.0
x \<in> unit_disc
y \<in> unit_disc
x \<in> circline_set x_axis
y \<in> circline_set x_axis
x \<noteq> y

goal (1 subgoal):
 1. poincare_distance x y = calc_poincare_distance x (of_complex (- 1)) y (of_complex 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_distance x y = calc_poincare_distance x (of_complex (- 1)) y (of_complex 1)

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poincare_distance x y = calc_poincare_distance x (of_complex (- 1)) y (of_complex 1)

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
have "... = abs (ln (Re (((x' + 1) * (y' - 1)) / ((x' - 1) * (y' + 1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. calc_poincare_distance x (of_complex (- 1)) y (of_complex 1) = \<bar>ln (Re ((x' + 1) * (y' - 1) / ((x' - 1) * (y' + 1))))\<bar>
[PROOF STEP]
using * \<open>cmod x' < 1\<close> \<open>cmod y' < 1\<close>
[PROOF STATE]
proof (prove)
using this:
x = of_complex x'
y = of_complex y'
cmod x' < 1
cmod y' < 1

goal (1 subgoal):
 1. calc_poincare_distance x (of_complex (- 1)) y (of_complex 1) = \<bar>ln (Re ((x' + 1) * (y' - 1) / ((x' - 1) * (y' + 1))))\<bar>
[PROOF STEP]
by (simp, transfer, transfer, auto)
[PROOF STATE]
proof (state)
this:
calc_poincare_distance x (of_complex (- 1)) y (of_complex 1) = \<bar>ln (Re ((x' + 1) * (y' - 1) / ((x' - 1) * (y' + 1))))\<bar>

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poincare_distance x y = \<bar>ln (Re ((x' + 1) * (y' - 1) / ((x' - 1) * (y' + 1))))\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poincare_distance x y = \<bar>ln (Re ((x' + 1) * (y' - 1) / ((x' - 1) * (y' + 1))))\<bar>

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
poincare_distance x y = \<bar>ln (Re ((x' + 1) * (y' - 1) / ((x' - 1) * (y' + 1))))\<bar>
x = of_complex x'
y = of_complex y'

goal (1 subgoal):
 1. poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)
[PROOF STEP]
by (metis (no_types, lifting) add.commute minus_diff_eq minus_divide_divide mult_minus_left mult_minus_right to_complex_of_complex)
[PROOF STATE]
proof (state)
this:
poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poincare_distance x y = (let x' = to_complex x; y' = to_complex y in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poincare_distance_zero_x_axis:
  assumes "x \<in> unit_disc" and "x \<in> circline_set x_axis"
  shows "poincare_distance 0\<^sub>h x = (let x' = to_complex x in abs (ln (Re ((1 - x') / (1 + x')))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> unit_disc
x \<in> circline_set x_axis

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)
[PROOF STEP]
using poincare_distance_x_axis_x_axis[of "0\<^sub>h" x]
[PROOF STATE]
proof (prove)
using this:
x \<in> unit_disc
x \<in> circline_set x_axis
\<lbrakk>0\<^sub>h \<in> unit_disc; x \<in> unit_disc; 0\<^sub>h \<in> circline_set x_axis; x \<in> circline_set x_axis\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex 0\<^sub>h; y' = to_complex x in \<bar>ln (Re ((1 + x') * (1 - y') / ((1 - x') * (1 + y'))))\<bar>)

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma poincare_distance_zero:
  assumes "x \<in> unit_disc"
  shows "poincare_distance 0\<^sub>h x = (let x' = to_complex x in abs (ln (Re ((1 - cmod x') / (1 + cmod x')))))" (is "?P x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
proof (cases "x = 0\<^sub>h")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0\<^sub>h \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
 2. x \<noteq> 0\<^sub>h \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0\<^sub>h

goal (2 subgoals):
 1. x = 0\<^sub>h \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
 2. x \<noteq> 0\<^sub>h \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0\<^sub>h

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal (1 subgoal):
 1. x \<noteq> 0\<^sub>h \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0\<^sub>h \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. x \<noteq> 0\<^sub>h \<Longrightarrow> poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
proof (rule wlog_rotation_to_positive_x_axis)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. x \<in> unit_disc
 2. x \<noteq> 0\<^sub>h
 3. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
 4. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
show "x \<in> unit_disc" "x \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> unit_disc &&& x \<noteq> 0\<^sub>h
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
x \<in> unit_disc
x \<noteq> 0\<^sub>h

goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
fix \<phi> u
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
assume "u \<in> unit_disc" "u \<noteq> 0\<^sub>h" "?P (moebius_pt (moebius_rotation \<phi>) u)"
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
u \<noteq> 0\<^sub>h
poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
thus "?P u"
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
u \<noteq> 0\<^sub>h
poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
using unit_disc_fix_preserve_poincare_distance[of "moebius_rotation \<phi>" "0\<^sub>h" u]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
u \<noteq> 0\<^sub>h
poincare_distance 0\<^sub>h (moebius_pt (moebius_rotation \<phi>) u) = (let x' = to_complex (moebius_pt (moebius_rotation \<phi>) u) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
\<lbrakk>unit_disc_fix (moebius_rotation \<phi>); 0\<^sub>h \<in> unit_disc; u \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance (moebius_pt (moebius_rotation \<phi>) 0\<^sub>h) (moebius_pt (moebius_rotation \<phi>) u) = poincare_distance 0\<^sub>h u

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
by (cases "u = \<infinity>\<^sub>h") (simp_all add: Let_def)
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h u = (let x' = to_complex u in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
assume "is_real x" "0 < Re x" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
thus "?P (of_complex x)"
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
using poincare_distance_zero_x_axis[of "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1
\<lbrakk>of_complex x \<in> unit_disc; of_complex x \<in> circline_set x_axis\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
[PROOF STEP]
by simp (auto simp add: circline_set_x_axis cmod_eq_Re complex_is_Real_iff)
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h x = (let x' = to_complex x in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poincare_distance_zero_opposite [simp]:
  assumes "of_complex z \<in> unit_disc"
  shows "poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)
[PROOF STEP]
have *: "of_complex (-z) \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (- z) \<in> unit_disc
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
of_complex z \<in> unit_disc

goal (1 subgoal):
 1. of_complex (- z) \<in> unit_disc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_complex (- z) \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)
[PROOF STEP]
using poincare_distance_zero[OF assms]
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (of_complex z) = (let x' = to_complex (of_complex z) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)
[PROOF STEP]
using poincare_distance_zero[OF *]
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (of_complex z) = (let x' = to_complex (of_complex z) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)
poincare_distance 0\<^sub>h (of_complex (- z)) = (let x' = to_complex (of_complex (- z)) in \<bar>ln (Re (cor ((1 - cmod x') / (1 + cmod x'))))\<bar>)

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (of_complex (- z)) = poincare_distance 0\<^sub>h (of_complex z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cosh_poincare_distance_cross_ratio_average:
  assumes "u \<in> unit_disc" "v \<in> unit_disc" "u \<noteq> v" "ideal_points (poincare_line u v) = {i1, i2}"
  shows "cosh_dist u v =
           ((Re_cross_ratio u i1 v i2) + (Re_cross_ratio v i1 u i2)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
let ?cr = "cross_ratio u i1 v i2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
let ?crRe = "Re (to_complex ?cr)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
have "?cr \<noteq> \<infinity>\<^sub>h" "is_real (to_complex ?cr)" "?crRe > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h &&& is_real (to_complex (cross_ratio u i1 v i2)) &&& 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
using distance_cross_ratio_real_positive[OF assms(1-3)] assms(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
ideal_points (poincare_line u v) = {i1, i2}

goal (1 subgoal):
 1. cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h &&& is_real (to_complex (cross_ratio u i1 v i2)) &&& 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1 v i2

goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
obtain cr where *: "cross_ratio u i1 v i2 = of_complex cr" "cr \<noteq> 0" "is_real cr" "Re cr > 0"
[PROOF STATE]
proof (prove)
using this:
cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1 v i2

goal (1 subgoal):
 1. (\<And>cr. \<lbrakk>cross_ratio u i1 v i2 = of_complex cr; cr \<noteq> 0; is_real cr; 0 < Re cr\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of "cross_ratio u i1 v i2"]
[PROOF STATE]
proof (prove)
using this:
cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1 v i2
cross_ratio u i1 v i2 = \<infinity>\<^sub>h \<or> (\<exists>x. cross_ratio u i1 v i2 = of_complex x)

goal (1 subgoal):
 1. (\<And>cr. \<lbrakk>cross_ratio u i1 v i2 = of_complex cr; cr \<noteq> 0; is_real cr; 0 < Re cr\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt to_complex_of_complex zero_complex.simps(1))
[PROOF STATE]
proof (state)
this:
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr

goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr

goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr

goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
using assms cross_ratio_commute_13[of v i1 u i2]
[PROOF STATE]
proof (prove)
using this:
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
ideal_points (poincare_line u v) = {i1, i2}
cross_ratio v i1 u i2 = reciprocal (cross_ratio u i1 v i2)

goal (1 subgoal):
 1. cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
unfolding poincare_distance_I[OF assms] calc_poincare_distance_def cosh_def
[PROOF STATE]
proof (prove)
using this:
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr
cross_ratio u i1 v i2 = of_complex cr
cr \<noteq> 0
is_real cr
0 < Re cr
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
ideal_points (poincare_line u v) = {i1, i2}
cross_ratio v i1 u i2 = reciprocal (cross_ratio u i1 v i2)

goal (1 subgoal):
 1. (exp \<bar>ln (Re_cross_ratio u i1 v i2)\<bar> + exp (- \<bar>ln (Re_cross_ratio u i1 v i2)\<bar>)) /\<^sub>R 2 = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2
[PROOF STEP]
by (cases "Re cr \<ge> 1")
       (auto simp add: ln_div[of 0] exp_minus field_simps Re_divide power2_eq_square complex.expand)
[PROOF STATE]
proof (state)
this:
cosh_dist u v = (Re_cross_ratio u i1 v i2 + Re_cross_ratio v i1 u i2) / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma blaschke_preserve_distance_formula [simp]:
  assumes "of_complex k \<in> unit_disc" "u \<in> unit_disc" "v \<in> unit_disc"
  shows "poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) =
         poincare_distance_formula (to_complex u) (to_complex v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
proof (cases "k = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = 0

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
obtain u' v' where *: "u' = to_complex u" "v' = to_complex v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u' v'. \<lbrakk>u' = to_complex u; v' = to_complex v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' = to_complex u
v' = to_complex v

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "cmod u' < 1" "cmod v' < 1" "cmod k < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod u' < 1 &&& cmod v' < 1 &&& cmod k < 1
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
of_complex k \<in> unit_disc
u \<in> unit_disc
v \<in> unit_disc
u' = to_complex u
v' = to_complex v

goal (1 subgoal):
 1. cmod u' < 1 &&& cmod v' < 1 &&& cmod k < 1
[PROOF STEP]
using inf_or_of_complex[of u] inf_or_of_complex[of v]
[PROOF STATE]
proof (prove)
using this:
of_complex k \<in> unit_disc
u \<in> unit_disc
v \<in> unit_disc
u' = to_complex u
v' = to_complex v
u = \<infinity>\<^sub>h \<or> (\<exists>x. u = of_complex x)
v = \<infinity>\<^sub>h \<or> (\<exists>x. v = of_complex x)

goal (1 subgoal):
 1. cmod u' < 1 &&& cmod v' < 1 &&& cmod k < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod u' < 1
cmod v' < 1
cmod k < 1

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
obtain nu du nv dv d kk ddu ddv where
    **: "nu = u' - k" "du = 1 - cnj k *u'" "nv = v' - k" "dv = 1 - cnj k * v'"
        "d = u' - v'" "ddu = 1 - u'*cnj u'" "ddv = 1 - v'*cnj v'" "kk = 1 - k*cnj k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>nu du nv dv d ddu ddv kk. \<lbrakk>nu = u' - k; du = 1 - cnj k * u'; nv = v' - k; dv = 1 - cnj k * v'; d = u' - v'; ddu = 1 - u' * cnj u'; ddv = 1 - v' * cnj v'; kk = 1 - k * cnj k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
d = u' - v'
ddu = 1 - u' * cnj u'
ddv = 1 - v' * cnj v'
kk = 1 - k * cnj k

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have d: "nu*dv - nv*du = d*kk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nu * dv - nv * du = d * kk
[PROOF STEP]
by (subst **)+ (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
nu * dv - nv * du = d * kk

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have ddu: "du*cnj du - nu*cnj nu = ddu*kk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. du * cnj du - nu * cnj nu = ddu * kk
[PROOF STEP]
by (subst **)+ (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
du * cnj du - nu * cnj nu = ddu * kk

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have ddv: "dv*cnj dv - nv*cnj nv = ddv*kk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dv * cnj dv - nv * cnj nv = ddv * kk
[PROOF STEP]
by (subst **)+ (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
dv * cnj dv - nv * cnj nv = ddv * kk

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "du \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. du \<noteq> 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> du \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> du \<noteq> 0

goal (1 subgoal):
 1. \<not> du \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "cmod (1 - cnj k * u') = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> du \<noteq> 0

goal (1 subgoal):
 1. cmod (1 - cnj k * u') = 0
[PROOF STEP]
using \<open>du = 1 - cnj k * u'\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> du \<noteq> 0
du = 1 - cnj k * u'

goal (1 subgoal):
 1. cmod (1 - cnj k * u') = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (1 - cnj k * u') = 0

goal (1 subgoal):
 1. \<not> du \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "cmod (cnj k * u') = 1"
[PROOF STATE]
proof (prove)
using this:
cmod (1 - cnj k * u') = 0

goal (1 subgoal):
 1. cmod (cnj k * u') = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (cnj k * u') = 1

goal (1 subgoal):
 1. \<not> du \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
cmod (cnj k * u') = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>cmod k < 1\<close> \<open>cmod u' < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod (cnj k * u') = 1
cmod k < 1
cmod u' < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using mult_strict_mono[of "cmod k" 1 "cmod u'" 1]
[PROOF STATE]
proof (prove)
using this:
cmod (cnj k * u') = 1
cmod k < 1
cmod u' < 1
\<lbrakk>cmod k < 1; cmod u' < 1; 0 < 1; 0 \<le> cmod u'\<rbrakk> \<Longrightarrow> cmod k * cmod u' < 1 * 1

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

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

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "dv \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dv \<noteq> 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dv \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> dv \<noteq> 0

goal (1 subgoal):
 1. \<not> dv \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "cmod (1 - cnj k * v') = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> dv \<noteq> 0

goal (1 subgoal):
 1. cmod (1 - cnj k * v') = 0
[PROOF STEP]
using \<open>dv = 1 - cnj k * v'\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> dv \<noteq> 0
dv = 1 - cnj k * v'

goal (1 subgoal):
 1. cmod (1 - cnj k * v') = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (1 - cnj k * v') = 0

goal (1 subgoal):
 1. \<not> dv \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "cmod (cnj k * v') = 1"
[PROOF STATE]
proof (prove)
using this:
cmod (1 - cnj k * v') = 0

goal (1 subgoal):
 1. cmod (cnj k * v') = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (cnj k * v') = 1

goal (1 subgoal):
 1. \<not> dv \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
cmod (cnj k * v') = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>cmod k < 1\<close> \<open>cmod v' < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod (cnj k * v') = 1
cmod k < 1
cmod v' < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using mult_strict_mono[of "cmod k" 1 "cmod v'" 1]
[PROOF STATE]
proof (prove)
using this:
cmod (cnj k * v') = 1
cmod k < 1
cmod v' < 1
\<lbrakk>cmod k < 1; cmod v' < 1; 0 < 1; 0 \<le> cmod v'\<rbrakk> \<Longrightarrow> cmod k * cmod v' < 1 * 1

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

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

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "kk \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kk \<noteq> 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> kk \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> kk \<noteq> 0

goal (1 subgoal):
 1. \<not> kk \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "cmod (1 - k * cnj k) = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> kk \<noteq> 0

goal (1 subgoal):
 1. cmod (1 - k * cnj k) = 0
[PROOF STEP]
using \<open>kk = 1 - k * cnj k\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> kk \<noteq> 0
kk = 1 - k * cnj k

goal (1 subgoal):
 1. cmod (1 - k * cnj k) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (1 - k * cnj k) = 0

goal (1 subgoal):
 1. \<not> kk \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "cmod (k * cnj k) = 1"
[PROOF STATE]
proof (prove)
using this:
cmod (1 - k * cnj k) = 0

goal (1 subgoal):
 1. cmod (k * cnj k) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (k * cnj k) = 1

goal (1 subgoal):
 1. \<not> kk \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
cmod (k * cnj k) = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>cmod k < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod (k * cnj k) = 1
cmod k < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using mult_strict_mono[of "cmod k" 1 "cmod k" 1]
[PROOF STATE]
proof (prove)
using this:
cmod (k * cnj k) = 1
cmod k < 1
\<lbrakk>cmod k < 1; cmod k < 1; 0 < 1; 0 \<le> cmod k\<rbrakk> \<Longrightarrow> cmod k * cmod k < 1 * 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using complex_mod_sqrt_Re_mult_cnj
[PROOF STATE]
proof (prove)
using this:
cmod (k * cnj k) = 1
cmod k < 1
\<lbrakk>cmod k < 1; cmod k < 1; 0 < 1; 0 \<le> cmod k\<rbrakk> \<Longrightarrow> cmod k * cmod k < 1 * 1
cmod ?z = sqrt (Re (?z * cnj ?z))

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

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

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
note nz = \<open>du \<noteq> 0\<close> \<open>dv \<noteq> 0\<close> \<open>kk \<noteq> 0\<close>
[PROOF STATE]
proof (state)
this:
du \<noteq> 0
dv \<noteq> 0
kk \<noteq> 0

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "nu / du - nv / dv = (nu*dv - nv*du) / (du * dv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nu / du - nv / dv = (nu * dv - nv * du) / (du * dv)
[PROOF STEP]
using nz
[PROOF STATE]
proof (prove)
using this:
du \<noteq> 0
dv \<noteq> 0
kk \<noteq> 0

goal (1 subgoal):
 1. nu / du - nv / dv = (nu * dv - nv * du) / (du * dv)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
nu / du - nv / dv = (nu * dv - nv * du) / (du * dv)

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
hence "(cmod (nu/du - nv/dv))\<^sup>2 = cmod ((d*kk) / (du*dv) * (cnj ((d*kk) / (du*dv))))" (is "?lhs = _")
[PROOF STATE]
proof (prove)
using this:
nu / du - nv / dv = (nu * dv - nv * du) / (du * dv)

goal (1 subgoal):
 1. (cmod (nu / du - nv / dv))\<^sup>2 = cmod (d * kk / (du * dv) * cnj (d * kk / (du * dv)))
[PROOF STEP]
unfolding complex_mod_mult_cnj[symmetric]
[PROOF STATE]
proof (prove)
using this:
nu / du - nv / dv = (nu * dv - nv * du) / (du * dv)

goal (1 subgoal):
 1. cmod ((nu / du - nv / dv) * cnj (nu / du - nv / dv)) = cmod (d * kk / (du * dv) * cnj (d * kk / (du * dv)))
[PROOF STEP]
by (subst (asm) d) simp
[PROOF STATE]
proof (state)
this:
(cmod (nu / du - nv / dv))\<^sup>2 = cmod (d * kk / (du * dv) * cnj (d * kk / (du * dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod (nu / du - nv / dv))\<^sup>2 = cmod (d * kk / (du * dv) * cnj (d * kk / (du * dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "... = cmod ((d*cnj d*kk*kk) / (du*cnj du*dv*cnj dv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (d * kk / (du * dv) * cnj (d * kk / (du * dv))) = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv))
[PROOF STEP]
by (simp add: field_simps norm_mult norm_divide)
[PROOF STATE]
proof (state)
this:
cmod (d * kk / (du * dv) * cnj (d * kk / (du * dv))) = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(cmod (nu / du - nv / dv))\<^sup>2 = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv))
[PROOF STEP]
have 1: "?lhs = cmod ((d*cnj d*kk*kk) / (du*cnj du*dv*cnj dv))"
[PROOF STATE]
proof (prove)
using this:
(cmod (nu / du - nv / dv))\<^sup>2 = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. (cmod (nu / du - nv / dv))\<^sup>2 = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(cmod (nu / du - nv / dv))\<^sup>2 = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "(1 - ((cmod nu) / (cmod du))\<^sup>2)*(1 - ((cmod nv) / (cmod dv))\<^sup>2) =
        (1 - cmod((nu * cnj nu) / (du * cnj du)))*(1 - cmod((nv * cnj nv) / (dv * cnj dv)))" (is "?rhs = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2) = (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv)))
[PROOF STEP]
by (metis norm_divide complex_mod_mult_cnj power_divide)
[PROOF STATE]
proof (state)
this:
(1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2) = (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2) = (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "... = cmod(((du*cnj du - nu*cnj nu) / (du * cnj du)) * ((dv*cnj dv - nv*cnj nv) / (dv * cnj dv)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
have "u' \<noteq> 1 / cnj k" "v' \<noteq> 1 / cnj k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' \<noteq> 1 / cnj k &&& v' \<noteq> 1 / cnj k
[PROOF STEP]
using \<open>cmod u' < 1\<close> \<open>cmod v' < 1\<close> \<open>cmod k < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod u' < 1
cmod v' < 1
cmod k < 1

goal (1 subgoal):
 1. u' \<noteq> 1 / cnj k &&& v' \<noteq> 1 / cnj k
[PROOF STEP]
by (auto simp add: False norm_divide)
[PROOF STATE]
proof (state)
this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
have "cmod k \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod k \<noteq> 1
[PROOF STEP]
using \<open>cmod k < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod k < 1

goal (1 subgoal):
 1. cmod k \<noteq> 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
cmod k \<noteq> 1

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1
[PROOF STEP]
have "cmod (nu/du) < 1" "cmod (nv/dv) < 1"
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1

goal (1 subgoal):
 1. cmod (nu / du) < 1 &&& cmod (nv / dv) < 1
[PROOF STEP]
using **(1-4)
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'

goal (1 subgoal):
 1. cmod (nu / du) < 1 &&& cmod (nv / dv) < 1
[PROOF STEP]
using unit_disc_fix_discI[OF blaschke_unit_disc_fix[OF \<open>cmod k < 1\<close>] \<open>u \<in> unit_disc\<close>] \<open>u' = to_complex u\<close>
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
moebius_pt (blaschke k) u \<in> unit_disc
u' = to_complex u

goal (1 subgoal):
 1. cmod (nu / du) < 1 &&& cmod (nv / dv) < 1
[PROOF STEP]
using unit_disc_fix_discI[OF blaschke_unit_disc_fix[OF \<open>cmod k < 1\<close>] \<open>v \<in> unit_disc\<close>] \<open>v' = to_complex v\<close>
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
moebius_pt (blaschke k) u \<in> unit_disc
u' = to_complex u
moebius_pt (blaschke k) v \<in> unit_disc
v' = to_complex v

goal (1 subgoal):
 1. cmod (nu / du) < 1 &&& cmod (nv / dv) < 1
[PROOF STEP]
using inf_or_of_complex[of u] \<open>u \<in> unit_disc\<close> inf_or_of_complex[of v] \<open>v \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
moebius_pt (blaschke k) u \<in> unit_disc
u' = to_complex u
moebius_pt (blaschke k) v \<in> unit_disc
v' = to_complex v
u = \<infinity>\<^sub>h \<or> (\<exists>x. u = of_complex x)
u \<in> unit_disc
v = \<infinity>\<^sub>h \<or> (\<exists>x. v = of_complex x)
v \<in> unit_disc

goal (1 subgoal):
 1. cmod (nu / du) < 1 &&& cmod (nv / dv) < 1
[PROOF STEP]
using moebius_pt_blaschke[of k u']
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
moebius_pt (blaschke k) u \<in> unit_disc
u' = to_complex u
moebius_pt (blaschke k) v \<in> unit_disc
v' = to_complex v
u = \<infinity>\<^sub>h \<or> (\<exists>x. u = of_complex x)
u \<in> unit_disc
v = \<infinity>\<^sub>h \<or> (\<exists>x. v = of_complex x)
v \<in> unit_disc
\<lbrakk>cmod k \<noteq> 1; u' \<noteq> 1 / cnj k\<rbrakk> \<Longrightarrow> moebius_pt (blaschke k) (of_complex u') = of_complex ((u' - k) / (1 - cnj k * u'))

goal (1 subgoal):
 1. cmod (nu / du) < 1 &&& cmod (nv / dv) < 1
[PROOF STEP]
using moebius_pt_blaschke[of k v']
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
cmod k \<noteq> 1
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
moebius_pt (blaschke k) u \<in> unit_disc
u' = to_complex u
moebius_pt (blaschke k) v \<in> unit_disc
v' = to_complex v
u = \<infinity>\<^sub>h \<or> (\<exists>x. u = of_complex x)
u \<in> unit_disc
v = \<infinity>\<^sub>h \<or> (\<exists>x. v = of_complex x)
v \<in> unit_disc
\<lbrakk>cmod k \<noteq> 1; u' \<noteq> 1 / cnj k\<rbrakk> \<Longrightarrow> moebius_pt (blaschke k) (of_complex u') = of_complex ((u' - k) / (1 - cnj k * u'))
\<lbrakk>cmod k \<noteq> 1; v' \<noteq> 1 / cnj k\<rbrakk> \<Longrightarrow> moebius_pt (blaschke k) (of_complex v') = of_complex ((v' - k) / (1 - cnj k * v'))

goal (1 subgoal):
 1. cmod (nu / du) < 1 &&& cmod (nv / dv) < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (nu / du) < 1
cmod (nv / dv) < 1

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
hence "(cmod (nu/du))\<^sup>2 < 1" "(cmod (nv/dv))\<^sup>2 < 1"
[PROOF STATE]
proof (prove)
using this:
cmod (nu / du) < 1
cmod (nv / dv) < 1

goal (1 subgoal):
 1. (cmod (nu / du))\<^sup>2 < 1 &&& (cmod (nv / dv))\<^sup>2 < 1
[PROOF STEP]
by (simp_all add: cmod_def)
[PROOF STATE]
proof (state)
this:
(cmod (nu / du))\<^sup>2 < 1
(cmod (nv / dv))\<^sup>2 < 1

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
hence "cmod (nu * cnj nu / (du * cnj du)) < 1"  "cmod (nv * cnj nv / (dv * cnj dv)) < 1"
[PROOF STATE]
proof (prove)
using this:
(cmod (nu / du))\<^sup>2 < 1
(cmod (nv / dv))\<^sup>2 < 1

goal (1 subgoal):
 1. cmod (nu * cnj nu / (du * cnj du)) < 1 &&& cmod (nv * cnj nv / (dv * cnj dv)) < 1
[PROOF STEP]
by (metis complex_mod_mult_cnj norm_divide power_divide)+
[PROOF STATE]
proof (state)
this:
cmod (nu * cnj nu / (du * cnj du)) < 1
cmod (nv * cnj nv / (dv * cnj dv)) < 1

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cmod (nu * cnj nu / (du * cnj du)) < 1
cmod (nv * cnj nv / (dv * cnj dv)) < 1

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
have "is_real (nu * cnj nu / (du * cnj du))" "is_real (nv * cnj nv / (dv * cnj dv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (nu * cnj nu / (du * cnj du)) &&& is_real (nv * cnj nv / (dv * cnj dv))
[PROOF STEP]
using eq_cnj_iff_real[of "nu * cnj nu / (du * cnj du)"]
[PROOF STATE]
proof (prove)
using this:
(cnj (nu * cnj nu / (du * cnj du)) = nu * cnj nu / (du * cnj du)) = is_real (nu * cnj nu / (du * cnj du))

goal (1 subgoal):
 1. is_real (nu * cnj nu / (du * cnj du)) &&& is_real (nv * cnj nv / (dv * cnj dv))
[PROOF STEP]
using eq_cnj_iff_real[of "nv * cnj nv / (dv * cnj dv)"]
[PROOF STATE]
proof (prove)
using this:
(cnj (nu * cnj nu / (du * cnj du)) = nu * cnj nu / (du * cnj du)) = is_real (nu * cnj nu / (du * cnj du))
(cnj (nv * cnj nv / (dv * cnj dv)) = nv * cnj nv / (dv * cnj dv)) = is_real (nv * cnj nv / (dv * cnj dv))

goal (1 subgoal):
 1. is_real (nu * cnj nu / (du * cnj du)) &&& is_real (nv * cnj nv / (dv * cnj dv))
[PROOF STEP]
by (auto simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
is_real (nu * cnj nu / (du * cnj du))
is_real (nv * cnj nv / (dv * cnj dv))

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_real (nu * cnj nu / (du * cnj du))
is_real (nv * cnj nv / (dv * cnj dv))

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
have "Re (nu * cnj nu / (du * cnj du)) \<ge> 0"  "Re (nv * cnj nv / (dv * cnj dv)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re (nu * cnj nu / (du * cnj du)) &&& 0 \<le> Re (nv * cnj nv / (dv * cnj dv))
[PROOF STEP]
using \<open>du \<noteq> 0\<close> \<open>dv \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
du \<noteq> 0
dv \<noteq> 0

goal (1 subgoal):
 1. 0 \<le> Re (nu * cnj nu / (du * cnj du)) &&& 0 \<le> Re (nv * cnj nv / (dv * cnj dv))
[PROOF STEP]
unfolding complex_mult_cnj_cmod
[PROOF STATE]
proof (prove)
using this:
du \<noteq> 0
dv \<noteq> 0

goal (1 subgoal):
 1. 0 \<le> Re (cor ((cmod nu)\<^sup>2) / cor ((cmod du)\<^sup>2)) &&& 0 \<le> Re (cor ((cmod nv)\<^sup>2) / cor ((cmod dv)\<^sup>2))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> Re (nu * cnj nu / (du * cnj du))
0 \<le> Re (nv * cnj nv / (dv * cnj dv))

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cmod (nu * cnj nu / (du * cnj du)) < 1
cmod (nv * cnj nv / (dv * cnj dv)) < 1
is_real (nu * cnj nu / (du * cnj du))
is_real (nv * cnj nv / (dv * cnj dv))
0 \<le> Re (nu * cnj nu / (du * cnj du))
0 \<le> Re (nv * cnj nv / (dv * cnj dv))
[PROOF STEP]
have "1 - cmod (nu * cnj nu / (du * cnj du)) = cmod (1 - nu * cnj nu / (du * cnj du))"
         "1 - cmod (nv * cnj nv / (dv * cnj dv)) = cmod (1 - nv * cnj nv / (dv * cnj dv))"
[PROOF STATE]
proof (prove)
using this:
cmod (nu * cnj nu / (du * cnj du)) < 1
cmod (nv * cnj nv / (dv * cnj dv)) < 1
is_real (nu * cnj nu / (du * cnj du))
is_real (nv * cnj nv / (dv * cnj dv))
0 \<le> Re (nu * cnj nu / (du * cnj du))
0 \<le> Re (nv * cnj nv / (dv * cnj dv))

goal (1 subgoal):
 1. 1 - cmod (nu * cnj nu / (du * cnj du)) = cmod (1 - nu * cnj nu / (du * cnj du)) &&& 1 - cmod (nv * cnj nv / (dv * cnj dv)) = cmod (1 - nv * cnj nv / (dv * cnj dv))
[PROOF STEP]
by (simp_all add: cmod_def)
[PROOF STATE]
proof (state)
this:
1 - cmod (nu * cnj nu / (du * cnj du)) = cmod (1 - nu * cnj nu / (du * cnj du))
1 - cmod (nv * cnj nv / (dv * cnj dv)) = cmod (1 - nv * cnj nv / (dv * cnj dv))

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 - cmod (nu * cnj nu / (du * cnj du)) = cmod (1 - nu * cnj nu / (du * cnj du))
1 - cmod (nv * cnj nv / (dv * cnj dv)) = cmod (1 - nv * cnj nv / (dv * cnj dv))

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
using nz
[PROOF STATE]
proof (prove)
using this:
1 - cmod (nu * cnj nu / (du * cnj du)) = cmod (1 - nu * cnj nu / (du * cnj du))
1 - cmod (nv * cnj nv / (dv * cnj dv)) = cmod (1 - nv * cnj nv / (dv * cnj dv))
du \<noteq> 0
dv \<noteq> 0
kk \<noteq> 0

goal (1 subgoal):
 1. (1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))
[PROOF STEP]
by (simp add: diff_divide_distrib norm_mult)
[PROOF STATE]
proof (state)
this:
(1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - cmod (nu * cnj nu / (du * cnj du))) * (1 - cmod (nv * cnj nv / (dv * cnj dv))) = cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "... = cmod(((ddu * kk) / (du * cnj du)) * ((ddv * kk) / (dv * cnj dv)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv))) = cmod (ddu * kk / (du * cnj du) * (ddv * kk / (dv * cnj dv)))
[PROOF STEP]
by (subst ddu, subst ddv, simp)
[PROOF STATE]
proof (state)
this:
cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv))) = cmod (ddu * kk / (du * cnj du) * (ddv * kk / (dv * cnj dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod ((du * cnj du - nu * cnj nu) / (du * cnj du) * ((dv * cnj dv - nv * cnj nv) / (dv * cnj dv))) = cmod (ddu * kk / (du * cnj du) * (ddv * kk / (dv * cnj dv)))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "... = cmod((ddu*ddv*kk*kk) / (du*cnj du*dv*cnj dv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (ddu * kk / (du * cnj du) * (ddv * kk / (dv * cnj dv))) = cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
cmod (ddu * kk / (du * cnj du) * (ddv * kk / (dv * cnj dv))) = cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2) = cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))
[PROOF STEP]
have 2: "?rhs = cmod((ddu*ddv*kk*kk) / (du*cnj du*dv*cnj dv))"
[PROOF STATE]
proof (prove)
using this:
(1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2) = cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. (1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2) = cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2) = cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "?lhs / ?rhs =
       cmod ((d*cnj d*kk*kk) / (du*cnj du*dv*cnj dv)) / cmod((ddu*ddv*kk*kk) / (du*cnj du*dv*cnj dv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv)) / cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))
[PROOF STEP]
by (subst 1, subst 2, simp)
[PROOF STATE]
proof (state)
this:
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv)) / cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv)) / cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "... = cmod ((d*cnj d)/(ddu*ddv))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv)) / cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv)) = cmod (d * cnj d / (ddu * ddv))
[PROOF STEP]
using nz
[PROOF STATE]
proof (prove)
using this:
du \<noteq> 0
dv \<noteq> 0
kk \<noteq> 0

goal (1 subgoal):
 1. cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv)) / cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv)) = cmod (d * cnj d / (ddu * ddv))
[PROOF STEP]
by (simp add: norm_mult norm_divide)
[PROOF STATE]
proof (state)
this:
cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv)) / cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv)) = cmod (d * cnj d / (ddu * ddv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (d * cnj d * kk * kk / (du * cnj du * dv * cnj dv)) / cmod (ddu * ddv * kk * kk / (du * cnj du * dv * cnj dv)) = cmod (d * cnj d / (ddu * ddv))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "... = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2)*(1 - (cmod v')\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
have "(cmod u')\<^sup>2 < 1" "(cmod v')\<^sup>2 < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod u')\<^sup>2 < 1 &&& (cmod v')\<^sup>2 < 1
[PROOF STEP]
using \<open>cmod u' < 1\<close> \<open>cmod v' < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod u' < 1
cmod v' < 1

goal (1 subgoal):
 1. (cmod u')\<^sup>2 < 1 &&& (cmod v')\<^sup>2 < 1
[PROOF STEP]
by (simp_all add: cmod_def)
[PROOF STATE]
proof (state)
this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
hence "cmod (1 - u' * cnj u') = 1 - (cmod u')\<^sup>2" "cmod (1 - v' * cnj v') = 1 - (cmod v')\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. cmod (1 - u' * cnj u') = 1 - (cmod u')\<^sup>2 &&& cmod (1 - v' * cnj v') = 1 - (cmod v')\<^sup>2
[PROOF STEP]
by (auto simp add: cmod_eq_Re cmod_power2 power2_eq_square[symmetric])
[PROOF STATE]
proof (state)
this:
cmod (1 - u' * cnj u') = 1 - (cmod u')\<^sup>2
cmod (1 - v' * cnj v') = 1 - (cmod v')\<^sup>2

goal (1 subgoal):
 1. cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod (1 - u' * cnj u') = 1 - (cmod u')\<^sup>2
cmod (1 - v' * cnj v') = 1 - (cmod v')\<^sup>2

goal (1 subgoal):
 1. cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
using nz
[PROOF STATE]
proof (prove)
using this:
cmod (1 - u' * cnj u') = 1 - (cmod u')\<^sup>2
cmod (1 - v' * cnj v') = 1 - (cmod v')\<^sup>2
du \<noteq> 0
dv \<noteq> 0
kk \<noteq> 0

goal (1 subgoal):
 1. cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
by (simp add: "**"(6) "**"(7) norm_divide norm_mult power2_eq_square)
[PROOF STATE]
proof (state)
this:
cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cmod (d * cnj d / (ddu * ddv)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
have 3: "?lhs / ?rhs = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2)*(1 - (cmod v')\<^sup>2))"
[PROOF STATE]
proof (prove)
using this:
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal (1 subgoal):
 1. (cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "cmod k \<noteq> 1" "u' \<noteq> 1 / cnj k" "v' \<noteq> 1 / cnj k" "u \<noteq> \<infinity>\<^sub>h" "v \<noteq> \<infinity>\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod k \<noteq> 1 &&& u' \<noteq> 1 / cnj k) &&& v' \<noteq> 1 / cnj k &&& u \<noteq> \<infinity>\<^sub>h &&& v \<noteq> \<infinity>\<^sub>h
[PROOF STEP]
using \<open>cmod k < 1\<close> \<open>u \<in> unit_disc\<close> \<open>v \<in> unit_disc\<close> * \<open>k \<noteq> 0\<close> ** \<open>kk \<noteq> 0\<close> nz
[PROOF STATE]
proof (prove)
using this:
cmod k < 1
u \<in> unit_disc
v \<in> unit_disc
u' = to_complex u
v' = to_complex v
k \<noteq> 0
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
d = u' - v'
ddu = 1 - u' * cnj u'
ddv = 1 - v' * cnj v'
kk = 1 - k * cnj k
kk \<noteq> 0
du \<noteq> 0
dv \<noteq> 0
kk \<noteq> 0

goal (1 subgoal):
 1. (cmod k \<noteq> 1 &&& u' \<noteq> 1 / cnj k) &&& v' \<noteq> 1 / cnj k &&& u \<noteq> \<infinity>\<^sub>h &&& v \<noteq> \<infinity>\<^sub>h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod k \<noteq> 1
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
u \<noteq> \<infinity>\<^sub>h
v \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod k \<noteq> 1
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
u \<noteq> \<infinity>\<^sub>h
v \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cmod k \<noteq> 1
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
u \<noteq> \<infinity>\<^sub>h
v \<noteq> \<infinity>\<^sub>h
of_complex k \<in> unit_disc
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using * ** 3
[PROOF STATE]
proof (prove)
using this:
cmod k \<noteq> 1
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
u \<noteq> \<infinity>\<^sub>h
v \<noteq> \<infinity>\<^sub>h
of_complex k \<in> unit_disc
u \<in> unit_disc
v \<in> unit_disc
u' = to_complex u
v' = to_complex v
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
d = u' - v'
ddu = 1 - u' * cnj u'
ddv = 1 - v' * cnj v'
kk = 1 - k * cnj k
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using moebius_pt_blaschke[of k u']
[PROOF STATE]
proof (prove)
using this:
cmod k \<noteq> 1
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
u \<noteq> \<infinity>\<^sub>h
v \<noteq> \<infinity>\<^sub>h
of_complex k \<in> unit_disc
u \<in> unit_disc
v \<in> unit_disc
u' = to_complex u
v' = to_complex v
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
d = u' - v'
ddu = 1 - u' * cnj u'
ddv = 1 - v' * cnj v'
kk = 1 - k * cnj k
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
\<lbrakk>cmod k \<noteq> 1; u' \<noteq> 1 / cnj k\<rbrakk> \<Longrightarrow> moebius_pt (blaschke k) (of_complex u') = of_complex ((u' - k) / (1 - cnj k * u'))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using moebius_pt_blaschke[of k v']
[PROOF STATE]
proof (prove)
using this:
cmod k \<noteq> 1
u' \<noteq> 1 / cnj k
v' \<noteq> 1 / cnj k
u \<noteq> \<infinity>\<^sub>h
v \<noteq> \<infinity>\<^sub>h
of_complex k \<in> unit_disc
u \<in> unit_disc
v \<in> unit_disc
u' = to_complex u
v' = to_complex v
nu = u' - k
du = 1 - cnj k * u'
nv = v' - k
dv = 1 - cnj k * v'
d = u' - v'
ddu = 1 - u' * cnj u'
ddv = 1 - v' * cnj v'
kk = 1 - k * cnj k
(cmod (nu / du - nv / dv))\<^sup>2 / ((1 - (cmod nu / cmod du)\<^sup>2) * (1 - (cmod nv / cmod dv)\<^sup>2)) = (cmod d)\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
\<lbrakk>cmod k \<noteq> 1; u' \<noteq> 1 / cnj k\<rbrakk> \<Longrightarrow> moebius_pt (blaschke k) (of_complex u') = of_complex ((u' - k) / (1 - cnj k * u'))
\<lbrakk>cmod k \<noteq> 1; v' \<noteq> 1 / cnj k\<rbrakk> \<Longrightarrow> moebius_pt (blaschke k) (of_complex v') = of_complex ((v' - k) / (1 - cnj k * v'))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by (simp add: norm_divide)
[PROOF STATE]
proof (state)
this:
poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rotation_preserve_distance_formula [simp]:
  assumes "u \<in> unit_disc" "v \<in> unit_disc"
  shows "poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) =
         poincare_distance_formula (to_complex u) (to_complex v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using inf_or_of_complex[of u] inf_or_of_complex[of v]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc
u = \<infinity>\<^sub>h \<or> (\<exists>x. u = of_complex x)
v = \<infinity>\<^sub>h \<or> (\<exists>x. v = of_complex x)

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by (auto simp: norm_mult)


[STATEMENT]
lemma unit_disc_fix_preserve_distance_formula [simp]:
  assumes "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc"
  shows "poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) =
         poincare_distance_formula (to_complex u) (to_complex v)" (is "?P' u v M")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
have "\<forall> u \<in> unit_disc. \<forall> v \<in> unit_disc. ?P' u v M" (is "?P M")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
proof (rule wlog_unit_disc_fix[OF assms(1)])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. cmod k < 1 \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. \<And>\<phi>. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 3. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. cmod k < 1 \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. \<And>\<phi>. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 3. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
assume "cmod k < 1"
[PROOF STATE]
proof (state)
this:
cmod k < 1

goal (3 subgoals):
 1. \<And>k. cmod k < 1 \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. \<And>\<phi>. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 3. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
hence "of_complex k \<in> unit_disc"
[PROOF STATE]
proof (prove)
using this:
cmod k < 1

goal (1 subgoal):
 1. of_complex k \<in> unit_disc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_complex k \<in> unit_disc

goal (3 subgoals):
 1. \<And>k. cmod k < 1 \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. \<And>\<phi>. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 3. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
thus  "?P (blaschke k)"
[PROOF STATE]
proof (prove)
using this:
of_complex k \<in> unit_disc

goal (1 subgoal):
 1. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using blaschke_preserve_distance_formula
[PROOF STATE]
proof (prove)
using this:
of_complex k \<in> unit_disc
\<lbrakk>of_complex ?k \<in> unit_disc; ?u \<in> unit_disc; ?v \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (blaschke ?k) ?u)) (to_complex (moebius_pt (blaschke ?k) ?v)) = poincare_distance_formula (to_complex ?u) (to_complex ?v)

goal (1 subgoal):
 1. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (blaschke k) u)) (to_complex (moebius_pt (blaschke k) v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal (2 subgoals):
 1. \<And>\<phi>. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
fix \<phi>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
 2. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
show "?P (moebius_rotation \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using rotation_preserve_distance_formula
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance_formula (to_complex (moebius_pt (moebius_rotation ?\<phi>) ?u)) (to_complex (moebius_pt (moebius_rotation ?\<phi>) ?v)) = poincare_distance_formula (to_complex ?u) (to_complex ?v)

goal (1 subgoal):
 1. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (moebius_rotation \<phi>) u)) (to_complex (moebius_pt (moebius_rotation \<phi>) v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal (1 subgoal):
 1. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
fix M1 M2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
assume *: "?P M1" and **: "?P M2"  and u11: "unit_disc_fix M1" "unit_disc_fix M2"
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v)
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)
unit_disc_fix M1
unit_disc_fix M2

goal (1 subgoal):
 1. \<And>M1 M2. \<lbrakk>unit_disc_fix M1; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v); unit_disc_fix M2; \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)\<rbrakk> \<Longrightarrow> \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
thus "?P (M1 + M2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M1 u)) (to_complex (moebius_pt M1 v)) = poincare_distance_formula (to_complex u) (to_complex v)
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M2 u)) (to_complex (moebius_pt M2 v)) = poincare_distance_formula (to_complex u) (to_complex v)
unit_disc_fix M1
unit_disc_fix M2

goal (1 subgoal):
 1. \<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by (auto simp del: poincare_distance_formula_def)
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt (M1 + M2) u)) (to_complex (moebius_pt (M1 + M2) v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>unit_disc. \<forall>v\<in>unit_disc. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v)) = poincare_distance_formula (to_complex u) (to_complex v)

goal:
No subgoals!
[PROOF STEP]
qed