[STATEMENT]
lemma wlog_perpendicular_foot:
  assumes in_disc: "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc" "z \<in> unit_disc"
  assumes perpendicular: "u \<noteq> v" "is_poincare_line H" "perpendicular (poincare_line u v) H"
  assumes "z \<in> circline_set (poincare_line u v) \<inter> circline_set H" "w \<in> circline_set H"
  assumes axes: "\<And> u v w. \<lbrakk>is_real u; 0 < Re u; Re u < 1; is_real v; -1 < Re v; Re v < 1; Re u \<noteq> Re v; is_imag w; 0 \<le> Im w; Im w < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex u) (of_complex v) (of_complex w)"
  assumes moebius: "\<And> M z u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; z \<in> unit_disc; P (moebius_pt M z) (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) \<rbrakk> \<Longrightarrow> P z u v w"
  assumes conjugate: "\<And> z u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; P (conjugate z) (conjugate u) (conjugate v) (conjugate w) \<rbrakk> \<Longrightarrow> P z u v w"
  assumes perm: "P z v u w \<Longrightarrow> P z u v w"
  shows "P z u v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P z u v w
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P z u v w
[PROOF STEP]
obtain m n where mn: "m = u \<or> m = v" "n = u \<or> n = v" "m \<noteq> n" "m \<noteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>m = u \<or> m = v; n = u \<or> n = v; m \<noteq> n; m \<noteq> z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>m = u \<or> m = v; n = u \<or> n = v; m \<noteq> n; m \<noteq> z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = u \<or> m = v
n = u \<or> n = v
m \<noteq> n
m \<noteq> z

goal (1 subgoal):
 1. P z u v w
[PROOF STEP]
have "n \<in> circline_set (poincare_line z m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> circline_set (poincare_line z m)
[PROOF STEP]
using \<open>z \<in> circline_set (poincare_line u v) \<inter> circline_set H\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set (poincare_line u v) \<inter> circline_set H

goal (1 subgoal):
 1. n \<in> circline_set (poincare_line z m)
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set (poincare_line u v) \<inter> circline_set H
m = u \<or> m = v
n = u \<or> n = v
m \<noteq> n
m \<noteq> z

goal (1 subgoal):
 1. n \<in> circline_set (poincare_line z m)
[PROOF STEP]
using unique_poincare_line[of z m "poincare_line u v", symmetric] in_disc
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set (poincare_line u v) \<inter> circline_set H
m = u \<or> m = v
n = u \<or> n = v
m \<noteq> n
m \<noteq> z
\<lbrakk>z \<noteq> m; z \<in> unit_disc; m \<in> unit_disc; z \<in> circline_set (poincare_line u v); m \<in> circline_set (poincare_line u v); is_poincare_line (poincare_line u v)\<rbrakk> \<Longrightarrow> poincare_line z m = poincare_line u v
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
z \<in> unit_disc

goal (1 subgoal):
 1. n \<in> circline_set (poincare_line z m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> circline_set (poincare_line z m)

goal (1 subgoal):
 1. P z u v w
[PROOF STEP]
have "\<forall> n. n \<in> unit_disc \<and> m \<noteq> n \<and> n \<in> circline_set (poincare_line z m) \<and> m \<noteq> z \<longrightarrow> P z m n w" (is "?Q z m w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> unit_disc \<and> m \<noteq> n \<and> n \<in> circline_set (poincare_line z m) \<and> m \<noteq> z \<longrightarrow> P z m n w
[PROOF STEP]
proof (rule wlog_perpendicular_axes[where P="?Q"])
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. m \<in> unit_disc
 2. w \<in> unit_disc
 3. z \<in> unit_disc
 4. is_poincare_line ?H1.0
 5. is_poincare_line ?H2.0
 6. perpendicular ?H1.0 ?H2.0
 7. z \<in> circline_set ?H1.0 \<inter> circline_set ?H2.0
 8. m \<in> circline_set ?H1.0
 9. w \<in> circline_set ?H2.0
 10. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
A total of 12 subgoals...
[PROOF STEP]
show "is_poincare_line (poincare_line u v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_poincare_line (poincare_line u v)
[PROOF STEP]
using \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v

goal (1 subgoal):
 1. is_poincare_line (poincare_line u v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_poincare_line (poincare_line u v)

goal (11 subgoals):
 1. m \<in> unit_disc
 2. w \<in> unit_disc
 3. z \<in> unit_disc
 4. is_poincare_line ?H2.0
 5. perpendicular (poincare_line u v) ?H2.0
 6. z \<in> circline_set (poincare_line u v) \<inter> circline_set ?H2.0
 7. m \<in> circline_set (poincare_line u v)
 8. w \<in> circline_set ?H2.0
 9. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 10. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. m \<in> unit_disc
 2. w \<in> unit_disc
 3. z \<in> unit_disc
 4. is_poincare_line ?H2.0
 5. perpendicular (poincare_line u v) ?H2.0
 6. z \<in> circline_set (poincare_line u v) \<inter> circline_set ?H2.0
 7. m \<in> circline_set (poincare_line u v)
 8. w \<in> circline_set ?H2.0
 9. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 10. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
A total of 11 subgoals...
[PROOF STEP]
show "is_poincare_line H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_poincare_line H
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
is_poincare_line H

goal (10 subgoals):
 1. m \<in> unit_disc
 2. w \<in> unit_disc
 3. z \<in> unit_disc
 4. perpendicular (poincare_line u v) H
 5. z \<in> circline_set (poincare_line u v) \<inter> circline_set H
 6. m \<in> circline_set (poincare_line u v)
 7. w \<in> circline_set H
 8. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 9. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 10. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. m \<in> unit_disc
 2. w \<in> unit_disc
 3. z \<in> unit_disc
 4. perpendicular (poincare_line u v) H
 5. z \<in> circline_set (poincare_line u v) \<inter> circline_set H
 6. m \<in> circline_set (poincare_line u v)
 7. w \<in> circline_set H
 8. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 9. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 10. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "m \<in> unit_disc" "m \<in> circline_set (poincare_line u v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> unit_disc &&& m \<in> circline_set (poincare_line u v)
[PROOF STEP]
using mn in_disc
[PROOF STATE]
proof (prove)
using this:
m = u \<or> m = v
n = u \<or> n = v
m \<noteq> n
m \<noteq> z
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
z \<in> unit_disc

goal (1 subgoal):
 1. m \<in> unit_disc &&& m \<in> circline_set (poincare_line u v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<in> unit_disc
m \<in> circline_set (poincare_line u v)

goal (8 subgoals):
 1. w \<in> unit_disc
 2. z \<in> unit_disc
 3. perpendicular (poincare_line u v) H
 4. z \<in> circline_set (poincare_line u v) \<inter> circline_set H
 5. w \<in> circline_set H
 6. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 7. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 8. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. w \<in> unit_disc
 2. z \<in> unit_disc
 3. perpendicular (poincare_line u v) H
 4. z \<in> circline_set (poincare_line u v) \<inter> circline_set H
 5. w \<in> circline_set H
 6. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 7. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 8. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "w \<in> unit_disc" "z \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> unit_disc &&& z \<in> unit_disc
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
w \<in> unit_disc
z \<in> unit_disc

goal (6 subgoals):
 1. perpendicular (poincare_line u v) H
 2. z \<in> circline_set (poincare_line u v) \<inter> circline_set H
 3. w \<in> circline_set H
 4. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 5. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 6. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. perpendicular (poincare_line u v) H
 2. z \<in> circline_set (poincare_line u v) \<inter> circline_set H
 3. w \<in> circline_set H
 4. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 5. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 6. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "z \<in> circline_set (poincare_line u v) \<inter> circline_set H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> circline_set (poincare_line u v) \<inter> circline_set H
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
z \<in> circline_set (poincare_line u v) \<inter> circline_set H

goal (5 subgoals):
 1. perpendicular (poincare_line u v) H
 2. w \<in> circline_set H
 3. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 4. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 5. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. perpendicular (poincare_line u v) H
 2. w \<in> circline_set H
 3. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 4. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 5. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "perpendicular (poincare_line u v) H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perpendicular (poincare_line u v) H
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
perpendicular (poincare_line u v) H

goal (4 subgoals):
 1. w \<in> circline_set H
 2. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 3. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 4. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. w \<in> circline_set H
 2. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 3. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 4. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "w \<in> circline_set H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> circline_set H
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
w \<in> circline_set H

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
assume xy: "is_real x" "0 \<le> Re x" "Re x < 1" "is_imag y" "0 \<le> Im y" "Im y < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 \<le> Re x
Re x < 1
is_imag y
0 \<le> Im y
Im y < 1

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "?Q 0\<^sub>h (of_complex x) (of_complex y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
assume "n \<in> unit_disc" "of_complex x \<noteq> n"
[PROOF STATE]
proof (state)
this:
n \<in> unit_disc
of_complex x \<noteq> n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
assume "n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x))" "of_complex x \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (state)
this:
n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x))
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
hence "n \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x))
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. n \<in> circline_set x_axis
[PROOF STEP]
using poincare_line_0_real_is_x_axis[of "of_complex x"] xy
[PROOF STATE]
proof (prove)
using this:
n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x))
of_complex x \<noteq> 0\<^sub>h
\<lbrakk>of_complex x \<in> circline_set x_axis; of_complex x \<noteq> 0\<^sub>h; of_complex x \<noteq> \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> poincare_line 0\<^sub>h (of_complex x) = x_axis
is_real x
0 \<le> Re x
Re x < 1
is_imag y
0 \<le> Im y
Im y < 1

goal (1 subgoal):
 1. n \<in> circline_set x_axis
[PROOF STEP]
by (auto simp add: circline_set_x_axis)
[PROOF STATE]
proof (state)
this:
n \<in> circline_set x_axis

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> circline_set x_axis
[PROOF STEP]
obtain n' where n': "n = of_complex n'"
[PROOF STATE]
proof (prove)
using this:
n \<in> circline_set x_axis

goal (1 subgoal):
 1. (\<And>n'. n = of_complex n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of n] \<open>n \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
n \<in> circline_set x_axis
n = \<infinity>\<^sub>h \<or> (\<exists>x. n = of_complex x)
n \<in> unit_disc

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

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
hence "is_real n'"
[PROOF STATE]
proof (prove)
using this:
n = of_complex n'

goal (1 subgoal):
 1. is_real n'
[PROOF STEP]
using \<open>n \<in> circline_set x_axis\<close>
[PROOF STATE]
proof (prove)
using this:
n = of_complex n'
n \<in> circline_set x_axis

goal (1 subgoal):
 1. is_real n'
[PROOF STEP]
using of_complex_inj
[PROOF STATE]
proof (prove)
using this:
n = of_complex n'
n \<in> circline_set x_axis
of_complex ?x = of_complex ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. is_real n'
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
n = of_complex n'
n \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
of_complex ?x = of_complex ?y \<Longrightarrow> ?x = ?y

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

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
hence "-1 < Re n'" "Re n' < 1"
[PROOF STATE]
proof (prove)
using this:
is_real n'

goal (1 subgoal):
 1. - 1 < Re n' &&& Re n' < 1
[PROOF STEP]
using \<open>n \<in> unit_disc\<close> n'
[PROOF STATE]
proof (prove)
using this:
is_real n'
n \<in> unit_disc
n = of_complex n'

goal (1 subgoal):
 1. - 1 < Re n' &&& Re n' < 1
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
- 1 < Re n'
Re n' < 1

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
have "Re n' \<noteq> Re x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re n' \<noteq> Re x
[PROOF STEP]
using complex.expand[of n' x] \<open>is_real n'\<close> \<open>is_real x\<close> \<open>of_complex x \<noteq> n\<close> n'
[PROOF STATE]
proof (prove)
using this:
Re n' = Re x \<and> Im n' = Im x \<Longrightarrow> n' = x
is_real n'
is_real x
of_complex x \<noteq> n
n = of_complex n'

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

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
have "Re x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Re x
[PROOF STEP]
using xy \<open>of_complex x \<noteq> 0\<^sub>h\<close>
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1
is_imag y
0 \<le> Im y
Im y < 1
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. 0 < Re x
[PROOF STEP]
by (cases "Re x = 0", auto simp add: complex.expand)
[PROOF STATE]
proof (state)
this:
0 < Re x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; of_complex x \<noteq> n; n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)); of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
show "P 0\<^sub>h (of_complex x) n (of_complex y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
using axes[of x n' y] xy n' \<open>Re x > 0\<close> \<open>is_real n'\<close> \<open>-1 < Re n'\<close> \<open>Re n' < 1\<close> \<open>Re n' \<noteq> Re x\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_real x; 0 < Re x; Re x < 1; is_real n'; - 1 < Re n'; Re n' < 1; Re x \<noteq> Re n'; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex n') (of_complex y)
is_real x
0 \<le> Re x
Re x < 1
is_imag y
0 \<le> Im y
Im y < 1
n = of_complex n'
0 < Re x
is_real n'
- 1 < Re n'
Re n' < 1
Re n' \<noteq> Re x

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) n (of_complex y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P 0\<^sub>h (of_complex x) n (of_complex y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> unit_disc \<and> of_complex x \<noteq> n \<and> n \<in> circline_set (poincare_line 0\<^sub>h (of_complex x)) \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> P 0\<^sub>h (of_complex x) n (of_complex y)

goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
fix M u v w
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
assume 1: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc

goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
assume 2: "?Q (moebius_pt M u) (moebius_pt M v) (moebius_pt M w)"
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)

goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> moebius_pt M v \<noteq> n \<and> n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) n (moebius_pt M w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "?Q u v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; v \<noteq> n; n \<in> circline_set (poincare_line u v); v \<noteq> u\<rbrakk> \<Longrightarrow> P u v n w
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; v \<noteq> n; n \<in> circline_set (poincare_line u v); v \<noteq> u\<rbrakk> \<Longrightarrow> P u v n w
[PROOF STEP]
assume "n \<in> unit_disc" "v \<noteq> n" "n \<in> circline_set (poincare_line u v)" "v \<noteq> u"
[PROOF STATE]
proof (state)
this:
n \<in> unit_disc
v \<noteq> n
n \<in> circline_set (poincare_line u v)
v \<noteq> u

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; v \<noteq> n; n \<in> circline_set (poincare_line u v); v \<noteq> u\<rbrakk> \<Longrightarrow> P u v n w
[PROOF STEP]
thus "P u v n w"
[PROOF STATE]
proof (prove)
using this:
n \<in> unit_disc
v \<noteq> n
n \<in> circline_set (poincare_line u v)
v \<noteq> u

goal (1 subgoal):
 1. P u v n w
[PROOF STEP]
using moebius[of M v n w u] 1 2[rule_format, of "moebius_pt M n"]
[PROOF STATE]
proof (prove)
using this:
n \<in> unit_disc
v \<noteq> n
n \<in> circline_set (poincare_line u v)
v \<noteq> u
\<lbrakk>unit_disc_fix M; v \<in> unit_disc; n \<in> unit_disc; w \<in> unit_disc; u \<in> unit_disc; P (moebius_pt M u) (moebius_pt M v) (moebius_pt M n) (moebius_pt M w)\<rbrakk> \<Longrightarrow> P u v n w
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
moebius_pt M n \<in> unit_disc \<and> moebius_pt M v \<noteq> moebius_pt M n \<and> moebius_pt M n \<in> circline_set (poincare_line (moebius_pt M u) (moebius_pt M v)) \<and> moebius_pt M v \<noteq> moebius_pt M u \<Longrightarrow> P (moebius_pt M u) (moebius_pt M v) (moebius_pt M n) (moebius_pt M w)

goal (1 subgoal):
 1. P u v n w
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
P u v n w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w

goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
fix u v w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
assume 1: "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc

goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
assume 2: "?Q (conjugate u) (conjugate v) (conjugate w)"
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)

goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; \<forall>n. n \<in> unit_disc \<and> conjugate v \<noteq> n \<and> n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<longrightarrow> P (conjugate u) (conjugate v) n (conjugate w)\<rbrakk> \<Longrightarrow> \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
show "?Q u v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; v \<noteq> n; n \<in> circline_set (poincare_line u v); v \<noteq> u\<rbrakk> \<Longrightarrow> P u v n w
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; v \<noteq> n; n \<in> circline_set (poincare_line u v); v \<noteq> u\<rbrakk> \<Longrightarrow> P u v n w
[PROOF STEP]
assume "n \<in> unit_disc" "v \<noteq> n" "n \<in> circline_set (poincare_line u v)" "v \<noteq> u"
[PROOF STATE]
proof (state)
this:
n \<in> unit_disc
v \<noteq> n
n \<in> circline_set (poincare_line u v)
v \<noteq> u

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<in> unit_disc; v \<noteq> n; n \<in> circline_set (poincare_line u v); v \<noteq> u\<rbrakk> \<Longrightarrow> P u v n w
[PROOF STEP]
thus "P u v n w"
[PROOF STATE]
proof (prove)
using this:
n \<in> unit_disc
v \<noteq> n
n \<in> circline_set (poincare_line u v)
v \<noteq> u

goal (1 subgoal):
 1. P u v n w
[PROOF STEP]
using conjugate[of v n w u] 1 2[rule_format, of "conjugate n"]
[PROOF STATE]
proof (prove)
using this:
n \<in> unit_disc
v \<noteq> n
n \<in> circline_set (poincare_line u v)
v \<noteq> u
\<lbrakk>v \<in> unit_disc; n \<in> unit_disc; w \<in> unit_disc; P (conjugate u) (conjugate v) (conjugate n) (conjugate w)\<rbrakk> \<Longrightarrow> P u v n w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
conjugate n \<in> unit_disc \<and> conjugate v \<noteq> conjugate n \<and> conjugate n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<Longrightarrow> P (conjugate u) (conjugate v) (conjugate n) (conjugate w)

goal (1 subgoal):
 1. P u v n w
[PROOF STEP]
using conjugate_inj
[PROOF STATE]
proof (prove)
using this:
n \<in> unit_disc
v \<noteq> n
n \<in> circline_set (poincare_line u v)
v \<noteq> u
\<lbrakk>v \<in> unit_disc; n \<in> unit_disc; w \<in> unit_disc; P (conjugate u) (conjugate v) (conjugate n) (conjugate w)\<rbrakk> \<Longrightarrow> P u v n w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
conjugate n \<in> unit_disc \<and> conjugate v \<noteq> conjugate n \<and> conjugate n \<in> circline_set (poincare_line (conjugate u) (conjugate v)) \<and> conjugate v \<noteq> conjugate u \<Longrightarrow> P (conjugate u) (conjugate v) (conjugate n) (conjugate w)
conjugate ?x = conjugate ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. P u v n w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P u v n w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> unit_disc \<and> v \<noteq> n \<and> n \<in> circline_set (poincare_line u v) \<and> v \<noteq> u \<longrightarrow> P u v n w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<in> unit_disc \<and> m \<noteq> n \<and> n \<in> circline_set (poincare_line z m) \<and> m \<noteq> z \<longrightarrow> P z m n w

goal (1 subgoal):
 1. P z u v w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. n \<in> unit_disc \<and> m \<noteq> n \<and> n \<in> circline_set (poincare_line z m) \<and> m \<noteq> z \<longrightarrow> P z m n w

goal (1 subgoal):
 1. P z u v w
[PROOF STEP]
using mn in_disc \<open>n \<in> circline_set (poincare_line z m)\<close> perm
[PROOF STATE]
proof (prove)
using this:
\<forall>n. n \<in> unit_disc \<and> m \<noteq> n \<and> n \<in> circline_set (poincare_line z m) \<and> m \<noteq> z \<longrightarrow> P z m n w
m = u \<or> m = v
n = u \<or> n = v
m \<noteq> n
m \<noteq> z
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
z \<in> unit_disc
n \<in> circline_set (poincare_line z m)
P z v u w \<Longrightarrow> P z u v w

goal (1 subgoal):
 1. P z u v w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P z u v w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma perpendicular_to_x_axis_intersects_x_axis:
  assumes "is_poincare_line H" "perpendicular_to_x_axis H"
  shows "intersects_x_axis H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersects_x_axis H
[PROOF STEP]
using assms hermitean_elems
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H
perpendicular_to_x_axis H
hermitean (?A, ?B, ?C, ?D) \<Longrightarrow> is_real ?A
hermitean (?A, ?B, ?C, ?D) \<Longrightarrow> is_real ?D
hermitean (?A, ?B, ?C, ?D) \<Longrightarrow> ?B = cnj ?C
hermitean (?A, ?B, ?C, ?D) \<Longrightarrow> cnj ?B = ?C

goal (1 subgoal):
 1. intersects_x_axis H
[PROOF STEP]
by (transfer, transfer, auto simp add: cmod_eq_Re)


[STATEMENT]
lemma perpendicular_intersects:
  assumes "is_poincare_line H1" "is_poincare_line H2"
  assumes "perpendicular H1 H2"
  shows "\<exists> z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2" (is "?P' H1 H2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
have "\<forall> H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> ?P' H1 H2" (is "?P H1")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
proof (rule wlog_line_x_axis)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. is_poincare_line H1
 2. \<forall>H2. is_poincare_line H2 \<and> perpendicular x_axis H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2)
 3. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>H2. is_poincare_line H2 \<and> perpendicular (moebius_circline M H1) H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set H2)\<rbrakk> \<Longrightarrow> \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
show "?P x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>H2. is_poincare_line H2 \<and> perpendicular x_axis H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H2. \<lbrakk>is_poincare_line H2; perpendicular x_axis H2\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2
[PROOF STEP]
fix H2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H2. \<lbrakk>is_poincare_line H2; perpendicular x_axis H2\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2
[PROOF STEP]
assume "is_poincare_line H2" "perpendicular x_axis H2"
[PROOF STATE]
proof (state)
this:
is_poincare_line H2
perpendicular x_axis H2

goal (1 subgoal):
 1. \<And>H2. \<lbrakk>is_poincare_line H2; perpendicular x_axis H2\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2
[PROOF STEP]
thus "\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2"
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H2
perpendicular x_axis H2

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2
[PROOF STEP]
using perpendicular_to_x_axis[of H2]
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H2
perpendicular x_axis H2
is_poincare_line H2 \<Longrightarrow> perpendicular_to_x_axis H2 = perpendicular x_axis H2

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2
[PROOF STEP]
using perpendicular_to_x_axis_intersects_x_axis[of H2]
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H2
perpendicular x_axis H2
is_poincare_line H2 \<Longrightarrow> perpendicular_to_x_axis H2 = perpendicular x_axis H2
\<lbrakk>is_poincare_line H2; perpendicular_to_x_axis H2\<rbrakk> \<Longrightarrow> intersects_x_axis H2

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2
[PROOF STEP]
using intersects_x_axis_iff[of H2]
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H2
perpendicular x_axis H2
is_poincare_line H2 \<Longrightarrow> perpendicular_to_x_axis H2 = perpendicular x_axis H2
\<lbrakk>is_poincare_line H2; perpendicular_to_x_axis H2\<rbrakk> \<Longrightarrow> intersects_x_axis H2
is_poincare_line H2 \<Longrightarrow> (\<exists>x\<in>unit_disc. x \<in> circline_set H2 \<inter> circline_set x_axis) = intersects_x_axis H2

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>H2. is_poincare_line H2 \<and> perpendicular x_axis H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<inter> circline_set H2)

goal (2 subgoals):
 1. is_poincare_line H1
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>H2. is_poincare_line H2 \<and> perpendicular (moebius_circline M H1) H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set H2)\<rbrakk> \<Longrightarrow> \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_poincare_line H1
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>H2. is_poincare_line H2 \<and> perpendicular (moebius_circline M H1) H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set H2)\<rbrakk> \<Longrightarrow> \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
fix M
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_poincare_line H1
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>H2. is_poincare_line H2 \<and> perpendicular (moebius_circline M H1) H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set H2)\<rbrakk> \<Longrightarrow> \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
assume "unit_disc_fix M"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M

goal (2 subgoals):
 1. is_poincare_line H1
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>H2. is_poincare_line H2 \<and> perpendicular (moebius_circline M H1) H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set H2)\<rbrakk> \<Longrightarrow> \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
assume *: "?P (moebius_circline M H1)"
[PROOF STATE]
proof (state)
this:
\<forall>H2. is_poincare_line H2 \<and> perpendicular (moebius_circline M H1) H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set H2)

goal (2 subgoals):
 1. is_poincare_line H1
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>H2. is_poincare_line H2 \<and> perpendicular (moebius_circline M H1) H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set H2)\<rbrakk> \<Longrightarrow> \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
show "?P H1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H2. \<lbrakk>is_poincare_line H2; perpendicular H1 H2\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
fix H2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H2. \<lbrakk>is_poincare_line H2; perpendicular H1 H2\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
assume "is_poincare_line H2" "perpendicular H1 H2"
[PROOF STATE]
proof (state)
this:
is_poincare_line H2
perpendicular H1 H2

goal (1 subgoal):
 1. \<And>H2. \<lbrakk>is_poincare_line H2; perpendicular H1 H2\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_poincare_line H2
perpendicular H1 H2
[PROOF STEP]
obtain z where "z \<in> unit_disc" "z \<in> circline_set (moebius_circline M H1) \<and> z \<in> circline_set (moebius_circline M H2)"
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H2
perpendicular H1 H2

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> unit_disc; z \<in> circline_set (moebius_circline M H1) \<and> z \<in> circline_set (moebius_circline M H2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *[rule_format, of "moebius_circline M H2"] \<open>unit_disc_fix M\<close>
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H2
perpendicular H1 H2
is_poincare_line (moebius_circline M H2) \<and> perpendicular (moebius_circline M H1) (moebius_circline M H2) \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set (moebius_circline M H1) \<inter> circline_set (moebius_circline M H2)
unit_disc_fix M

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> unit_disc; z \<in> circline_set (moebius_circline M H1) \<and> z \<in> circline_set (moebius_circline M H2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> unit_disc
z \<in> circline_set (moebius_circline M H1) \<and> z \<in> circline_set (moebius_circline M H2)

goal (1 subgoal):
 1. \<And>H2. \<lbrakk>is_poincare_line H2; perpendicular H1 H2\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
thus "\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2"
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
z \<in> circline_set (moebius_circline M H1) \<and> z \<in> circline_set (moebius_circline M H2)

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
using \<open>unit_disc_fix M\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
z \<in> circline_set (moebius_circline M H1) \<and> z \<in> circline_set (moebius_circline M H2)
unit_disc_fix M

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
by (rule_tac x="moebius_pt (-M) z" in exI)
           (metis IntI add.inverse_inverse circline_set_moebius_circline_iff moebius_pt_comp_inv_left uminus_moebius_def unit_disc_fix_discI unit_disc_fix_moebius_uminus)
[PROOF STATE]
proof (state)
this:
\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)

goal (1 subgoal):
 1. is_poincare_line H1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_poincare_line H1
[PROOF STEP]
show "is_poincare_line H1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_poincare_line H1
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
is_poincare_line H1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>H2. is_poincare_line H2 \<and> perpendicular H1 H2 \<longrightarrow> (\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2)
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2

goal (1 subgoal):
 1. \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H1 \<inter> circline_set H2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma calc_perpendicular_to_x_axis:
  assumes "z \<noteq> of_complex 1" "z \<noteq> of_complex (-1)"
  shows "z \<in> circline_set (calc_perpendicular_to_x_axis z) \<and>
         is_poincare_line (calc_perpendicular_to_x_axis z) \<and>
         perpendicular_to_x_axis (calc_perpendicular_to_x_axis z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> circline_set (calc_perpendicular_to_x_axis z) \<and> is_poincare_line (calc_perpendicular_to_x_axis z) \<and> perpendicular_to_x_axis (calc_perpendicular_to_x_axis z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> of_complex 1
z \<noteq> of_complex (- 1)

goal (1 subgoal):
 1. z \<in> circline_set (calc_perpendicular_to_x_axis z) \<and> is_poincare_line (calc_perpendicular_to_x_axis z) \<and> perpendicular_to_x_axis (calc_perpendicular_to_x_axis z)
[PROOF STEP]
unfolding circline_set_def perpendicular_def
[PROOF STATE]
proof (prove)
using this:
z \<noteq> of_complex 1
z \<noteq> of_complex (- 1)

goal (1 subgoal):
 1. z \<in> Collect (on_circline (calc_perpendicular_to_x_axis z)) \<and> is_poincare_line (calc_perpendicular_to_x_axis z) \<and> perpendicular_to_x_axis (calc_perpendicular_to_x_axis z)
[PROOF STEP]
proof (simp, transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z za. \<lbrakk>z \<noteq> vec_zero; \<not> z \<approx>\<^sub>v 1\<^sub>v; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> z \<approx>\<^sub>v of_complex_cvec 1; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> za \<approx> of_complex_hcoords 1; \<not> za \<approx> of_complex_hcoords (- 1)\<rbrakk> \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
fix z :: complex_vec
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z za. \<lbrakk>z \<noteq> vec_zero; \<not> z \<approx>\<^sub>v 1\<^sub>v; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> z \<approx>\<^sub>v of_complex_cvec 1; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> za \<approx> of_complex_hcoords 1; \<not> za \<approx> of_complex_hcoords (- 1)\<rbrakk> \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
obtain z1 z2 where z: "z = (z1, z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z1 z2. z = (z1, z2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z, auto)
[PROOF STATE]
proof (state)
this:
z = (z1, z2)

goal (1 subgoal):
 1. \<And>z za. \<lbrakk>z \<noteq> vec_zero; \<not> z \<approx>\<^sub>v 1\<^sub>v; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> z \<approx>\<^sub>v of_complex_cvec 1; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> za \<approx> of_complex_hcoords 1; \<not> za \<approx> of_complex_hcoords (- 1)\<rbrakk> \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
assume **: "\<not> z \<approx>\<^sub>v of_complex_cvec 1" "\<not> z \<approx>\<^sub>v of_complex_cvec (- 1)"
[PROOF STATE]
proof (state)
this:
\<not> z \<approx>\<^sub>v of_complex_cvec 1
\<not> z \<approx>\<^sub>v of_complex_cvec (- 1)

goal (1 subgoal):
 1. \<And>z za. \<lbrakk>z \<noteq> vec_zero; \<not> z \<approx>\<^sub>v 1\<^sub>v; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> z \<approx>\<^sub>v of_complex_cvec 1; \<not> z \<approx>\<^sub>v of_complex_cvec (- 1); \<not> za \<approx> of_complex_hcoords 1; \<not> za \<approx> of_complex_hcoords (- 1)\<rbrakk> \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
show "on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and>
        is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and>
        perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
proof (cases "z1*cnj z2 + z2*cnj z1 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z1 * cnj z2 + z2 * cnj z1 = 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
 2. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z1 * cnj z2 + z2 * cnj z1 = 0

goal (2 subgoals):
 1. z1 * cnj z2 + z2 * cnj z1 = 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
 2. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z1 * cnj z2 + z2 * cnj z1 = 0

goal (1 subgoal):
 1. on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
z1 * cnj z2 + z2 * cnj z1 = 0
z = (z1, z2)

goal (1 subgoal):
 1. on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
by (simp add: vec_cnj_def hermitean_def mat_adj_def mat_cnj_def mult.commute)
[PROOF STATE]
proof (state)
this:
on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z1 * cnj z2 + z2 * cnj z1 \<noteq> 0

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
hence "z2 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z1 * cnj z2 + z2 * cnj z1 \<noteq> 0

goal (1 subgoal):
 1. z2 \<noteq> 0
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
z1 * cnj z2 + z2 * cnj z1 \<noteq> 0
z = (z1, z2)

goal (1 subgoal):
 1. z2 \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z2 \<noteq> 0

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
hence "Re (z2 * cnj z2) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z2 \<noteq> 0

goal (1 subgoal):
 1. Re (z2 * cnj z2) \<noteq> 0
[PROOF STEP]
using \<open>z2 \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
z2 \<noteq> 0
z2 \<noteq> 0

goal (1 subgoal):
 1. Re (z2 * cnj z2) \<noteq> 0
[PROOF STEP]
by (auto simp add: complex.expand)
[PROOF STATE]
proof (state)
this:
Re (z2 * cnj z2) \<noteq> 0

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
have "z1 \<noteq> -z2 \<and> z1 \<noteq> z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z1 \<noteq> - z2 \<and> z1 \<noteq> z2
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (z1 \<noteq> - z2 \<and> z1 \<noteq> z2) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (z1 \<noteq> - z2 \<and> z1 \<noteq> z2)

goal (1 subgoal):
 1. \<not> (z1 \<noteq> - z2 \<and> z1 \<noteq> z2) \<Longrightarrow> False
[PROOF STEP]
hence "z \<approx>\<^sub>v of_complex_cvec 1 \<or> z \<approx>\<^sub>v of_complex_cvec (-1)"
[PROOF STATE]
proof (prove)
using this:
\<not> (z1 \<noteq> - z2 \<and> z1 \<noteq> z2)

goal (1 subgoal):
 1. z \<approx>\<^sub>v of_complex_cvec 1 \<or> z \<approx>\<^sub>v of_complex_cvec (- 1)
[PROOF STEP]
using z \<open>z2 \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (z1 \<noteq> - z2 \<and> z1 \<noteq> z2)
z = (z1, z2)
z2 \<noteq> 0

goal (1 subgoal):
 1. z \<approx>\<^sub>v of_complex_cvec 1 \<or> z \<approx>\<^sub>v of_complex_cvec (- 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<approx>\<^sub>v of_complex_cvec 1 \<or> z \<approx>\<^sub>v of_complex_cvec (- 1)

goal (1 subgoal):
 1. \<not> (z1 \<noteq> - z2 \<and> z1 \<noteq> z2) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
z \<approx>\<^sub>v of_complex_cvec 1 \<or> z \<approx>\<^sub>v of_complex_cvec (- 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
z \<approx>\<^sub>v of_complex_cvec 1 \<or> z \<approx>\<^sub>v of_complex_cvec (- 1)
\<not> z \<approx>\<^sub>v of_complex_cvec 1
\<not> z \<approx>\<^sub>v of_complex_cvec (- 1)

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:
z1 \<noteq> - z2 \<and> z1 \<noteq> z2

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
let ?A = "z1*cnj z2 + z2*cnj z1" and ?B = "-(z1*cnj z1 + z2*cnj z2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
have "Re(z1*cnj z1 + z2*cnj z2) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re (z1 * cnj z1 + z2 * cnj z2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> Re (z1 * cnj z1 + z2 * cnj z2)

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
hence "Re ?B \<le> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re (z1 * cnj z1 + z2 * cnj z2)

goal (1 subgoal):
 1. Re (- (z1 * cnj z1 + z2 * cnj z2)) \<le> 0
[PROOF STEP]
by (smt uminus_complex.simps(1))
[PROOF STATE]
proof (state)
this:
Re (- (z1 * cnj z1 + z2 * cnj z2)) \<le> 0

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
hence "abs (Re ?B) = - Re ?B"
[PROOF STATE]
proof (prove)
using this:
Re (- (z1 * cnj z1 + z2 * cnj z2)) \<le> 0

goal (1 subgoal):
 1. \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar> = - Re (- (z1 * cnj z1 + z2 * cnj z2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar> = - Re (- (z1 * cnj z1 + z2 * cnj z2))

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar> = - Re (- (z1 * cnj z1 + z2 * cnj z2))

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
have "... = (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Re (- (z1 * cnj z1 + z2 * cnj z2)) = (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square[symmetric])
[PROOF STATE]
proof (state)
this:
- Re (- (z1 * cnj z1 + z2 * cnj z2)) = (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Re (- (z1 * cnj z1 + z2 * cnj z2)) = (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
have "... > abs (Re ?A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
proof (cases "Re ?A \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
 2. \<not> 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1)

goal (2 subgoals):
 1. 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
 2. \<not> 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
have "(Re z1 + Re z2)\<^sup>2 + (Im z1 + Im z2)\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (Re z1 + Re z2)\<^sup>2 + (Im z1 + Im z2)\<^sup>2
[PROOF STEP]
using \<open>z1 \<noteq> -z2 \<and> z1 \<noteq> z2\<close>
[PROOF STATE]
proof (prove)
using this:
z1 \<noteq> - z2 \<and> z1 \<noteq> z2

goal (1 subgoal):
 1. 0 < (Re z1 + Re z2)\<^sup>2 + (Im z1 + Im z2)\<^sup>2
[PROOF STEP]
by (metis add.commute add.inverse_unique complex_neq_0 plus_complex.code plus_complex.simps)
[PROOF STATE]
proof (state)
this:
0 < (Re z1 + Re z2)\<^sup>2 + (Im z1 + Im z2)\<^sup>2

goal (2 subgoals):
 1. 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
 2. \<not> 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < (Re z1 + Re z2)\<^sup>2 + (Im z1 + Im z2)\<^sup>2

goal (1 subgoal):
 1. \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
0 < (Re z1 + Re z2)\<^sup>2 + (Im z1 + Im z2)\<^sup>2
\<not> 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1)

goal (1 subgoal):
 1. \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
by (simp add: power2_sum power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2

goal (1 subgoal):
 1. 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> Re (z1 * cnj z2 + z2 * cnj z1)

goal (1 subgoal):
 1. 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
have "(Re z1 - Re z2)\<^sup>2 + (Im z1 - Im z2)\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (Re z1 - Re z2)\<^sup>2 + (Im z1 - Im z2)\<^sup>2
[PROOF STEP]
using \<open>z1 \<noteq> -z2 \<and> z1 \<noteq> z2\<close>
[PROOF STATE]
proof (prove)
using this:
z1 \<noteq> - z2 \<and> z1 \<noteq> z2

goal (1 subgoal):
 1. 0 < (Re z1 - Re z2)\<^sup>2 + (Im z1 - Im z2)\<^sup>2
[PROOF STEP]
by (meson complex_eq_iff right_minus_eq sum_power2_gt_zero_iff)
[PROOF STATE]
proof (state)
this:
0 < (Re z1 - Re z2)\<^sup>2 + (Im z1 - Im z2)\<^sup>2

goal (1 subgoal):
 1. 0 \<le> Re (z1 * cnj z2 + z2 * cnj z1) \<Longrightarrow> \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < (Re z1 - Re z2)\<^sup>2 + (Im z1 - Im z2)\<^sup>2

goal (1 subgoal):
 1. \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
0 < (Re z1 - Re z2)\<^sup>2 + (Im z1 - Im z2)\<^sup>2
0 \<le> Re (z1 * cnj z2 + z2 * cnj z1)

goal (1 subgoal):
 1. \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2
[PROOF STEP]
by (simp add: power2_sum power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < (Re z1)\<^sup>2 + (Im z1)\<^sup>2 + (Re z2)\<^sup>2 + (Im z2)\<^sup>2

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>
[PROOF STEP]
have "abs (Re ?B) > abs (Re ?A)"
[PROOF STATE]
proof (prove)
using this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>

goal (1 subgoal):
 1. \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
have "cmod ?B = abs (Re ?B)" "cmod ?A = abs (Re ?A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (- (z1 * cnj z1 + z2 * cnj z2)) = \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar> &&& cmod (z1 * cnj z2 + z2 * cnj z1) = \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar>
[PROOF STEP]
by (simp_all add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
cmod (- (z1 * cnj z1 + z2 * cnj z2)) = \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>
cmod (z1 * cnj z2 + z2 * cnj z1) = \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar>

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>
cmod (- (z1 * cnj z1 + z2 * cnj z2)) = \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>
cmod (z1 * cnj z2 + z2 * cnj z1) = \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar>
[PROOF STEP]
have "(cmod ?B)\<^sup>2 > (cmod ?A)\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
\<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar> < \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>
cmod (- (z1 * cnj z1 + z2 * cnj z2)) = \<bar>Re (- (z1 * cnj z1 + z2 * cnj z2))\<bar>
cmod (z1 * cnj z2 + z2 * cnj z1) = \<bar>Re (z1 * cnj z2 + z2 * cnj z1)\<bar>

goal (1 subgoal):
 1. (cmod (z1 * cnj z2 + z2 * cnj z1))\<^sup>2 < (cmod (- (z1 * cnj z1 + z2 * cnj z2)))\<^sup>2
[PROOF STEP]
by (smt power2_le_imp_le)
[PROOF STATE]
proof (state)
this:
(cmod (z1 * cnj z2 + z2 * cnj z1))\<^sup>2 < (cmod (- (z1 * cnj z1 + z2 * cnj z2)))\<^sup>2

goal (1 subgoal):
 1. z1 * cnj z2 + z2 * cnj z1 \<noteq> 0 \<Longrightarrow> on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(cmod (z1 * cnj z2 + z2 * cnj z1))\<^sup>2 < (cmod (- (z1 * cnj z1 + z2 * cnj z2)))\<^sup>2

goal (1 subgoal):
 1. on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
using z False
[PROOF STATE]
proof (prove)
using this:
(cmod (z1 * cnj z2 + z2 * cnj z1))\<^sup>2 < (cmod (- (z1 * cnj z1 + z2 * cnj z2)))\<^sup>2
z = (z1, z2)
z1 * cnj z2 + z2 * cnj z1 \<noteq> 0

goal (1 subgoal):
 1. on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)
[PROOF STEP]
by (simp_all add: Let_def hermitean_def mat_adj_def mat_cnj_def cmod_eq_Re vec_cnj_def field_simps)
[PROOF STATE]
proof (state)
this:
on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z \<and> is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) \<and> perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)

goal:
No subgoals!
[PROOF STEP]
qed