[STATEMENT]
lemma arg_uminus_opposite_sign:
  assumes "z \<noteq> 0"
  shows "Arg z > 0 \<longleftrightarrow> \<not> Arg (-z) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
proof (cases "Arg z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Arg z = 0 \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
 2. Arg z \<noteq> 0 \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Arg z = 0

goal (2 subgoals):
 1. Arg z = 0 \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
 2. Arg z \<noteq> 0 \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg z = 0

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Arg z = 0
z \<noteq> 0

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
by (simp add: arg_uminus)
[PROOF STATE]
proof (state)
this:
(0 < Arg z) = (\<not> 0 < Arg (- z))

goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Arg z \<noteq> 0

goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
proof (cases "Arg z > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < Arg z \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
 2. \<not> 0 < Arg z \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < Arg z

goal (2 subgoals):
 1. 0 < Arg z \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
 2. \<not> 0 < Arg z \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < Arg z

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < Arg z
z \<noteq> 0

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using Arg_bounded[of z]
[PROOF STATE]
proof (prove)
using this:
0 < Arg z
z \<noteq> 0
- pi < Arg z \<and> Arg z \<le> pi

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using canon_ang_plus_pi1[of "Arg z"]
[PROOF STATE]
proof (prove)
using this:
0 < Arg z
z \<noteq> 0
- pi < Arg z \<and> Arg z \<le> pi
\<lbrakk>0 < Arg z; Arg z \<le> 2 * pi\<rbrakk> \<Longrightarrow> \<downharpoonright>Arg z + pi\<downharpoonleft> = Arg z - pi

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
by (simp add: arg_uminus)
[PROOF STATE]
proof (state)
this:
(0 < Arg z) = (\<not> 0 < Arg (- z))

goal (1 subgoal):
 1. \<not> 0 < Arg z \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < Arg z \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < Arg z

goal (1 subgoal):
 1. \<not> 0 < Arg z \<Longrightarrow> (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Arg z

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using \<open>Arg z \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Arg z
Arg z \<noteq> 0

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Arg z
Arg z \<noteq> 0
z \<noteq> 0

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using Arg_bounded[of z]
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Arg z
Arg z \<noteq> 0
z \<noteq> 0
- pi < Arg z \<and> Arg z \<le> pi

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
using canon_ang_plus_pi2[of "Arg z"]
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Arg z
Arg z \<noteq> 0
z \<noteq> 0
- pi < Arg z \<and> Arg z \<le> pi
\<lbrakk>- 2 * pi < Arg z; Arg z \<le> 0\<rbrakk> \<Longrightarrow> \<downharpoonright>Arg z + pi\<downharpoonleft> = Arg z + pi

goal (1 subgoal):
 1. (0 < Arg z) = (\<not> 0 < Arg (- z))
[PROOF STEP]
by (simp add: arg_uminus)
[PROOF STATE]
proof (state)
this:
(0 < Arg z) = (\<not> 0 < Arg (- z))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(0 < Arg z) = (\<not> 0 < Arg (- z))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_Im_sgn:
  assumes "\<not> is_real z"
  shows "sgn (Arg z) = sgn (Im z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
have "z \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Im z \<noteq> 0

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

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> 0
[PROOF STEP]
obtain r \<phi> where polar: "z = cor r * cis \<phi>" "\<phi> = Arg z" "r > 0"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. (\<And>r \<phi>. \<lbrakk>z = cor r * cis \<phi>; \<phi> = Arg z; 0 < r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt cmod_cis mult_eq_0_iff norm_ge_zero of_real_0)
[PROOF STATE]
proof (state)
this:
z = cor r * cis \<phi>
\<phi> = Arg z
0 < r

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
hence "Im z = r * sin \<phi>"
[PROOF STATE]
proof (prove)
using this:
z = cor r * cis \<phi>
\<phi> = Arg z
0 < r

goal (1 subgoal):
 1. Im z = r * sin \<phi>
[PROOF STEP]
by (metis Im_mult_real Re_complex_of_real cis.simps(2) Im_complex_of_real)
[PROOF STATE]
proof (state)
this:
Im z = r * sin \<phi>

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
hence  "Im z > 0 \<longleftrightarrow> sin \<phi> > 0" "Im z < 0 \<longleftrightarrow> sin \<phi> < 0"
[PROOF STATE]
proof (prove)
using this:
Im z = r * sin \<phi>

goal (1 subgoal):
 1. (0 < Im z) = (0 < sin \<phi>) &&& (Im z < 0) = (sin \<phi> < 0)
[PROOF STEP]
using \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
Im z = r * sin \<phi>
0 < r

goal (1 subgoal):
 1. (0 < Im z) = (0 < sin \<phi>) &&& (Im z < 0) = (sin \<phi> < 0)
[PROOF STEP]
using mult_pos_pos mult_nonneg_nonneg zero_less_mult_pos mult_less_cancel_left
[PROOF STATE]
proof (prove)
using this:
Im z = r * sin \<phi>
0 < r
\<lbrakk>(0::?'a) < ?a; (0::?'a) < ?b\<rbrakk> \<Longrightarrow> (0::?'a) < ?a * ?b
\<lbrakk>(0::?'a) \<le> ?a; (0::?'a) \<le> ?b\<rbrakk> \<Longrightarrow> (0::?'a) \<le> ?a * ?b
\<lbrakk>(0::?'a) < ?a * ?b; (0::?'a) < ?a\<rbrakk> \<Longrightarrow> (0::?'a) < ?b
(?c * ?a < ?c * ?b) = (((0::?'a) \<le> ?c \<longrightarrow> ?a < ?b) \<and> (?c \<le> (0::?'a) \<longrightarrow> ?b < ?a))

goal (1 subgoal):
 1. (0 < Im z) = (0 < sin \<phi>) &&& (Im z < 0) = (sin \<phi> < 0)
[PROOF STEP]
by smt+
[PROOF STATE]
proof (state)
this:
(0 < Im z) = (0 < sin \<phi>)
(Im z < 0) = (sin \<phi> < 0)

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(0 < Im z) = (0 < sin \<phi>)
(Im z < 0) = (sin \<phi> < 0)

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
have "\<phi> \<noteq> pi" "\<phi> \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<noteq> pi &&& \<phi> \<noteq> 0
[PROOF STEP]
using \<open>\<not> is_real z\<close> polar cis_pi
[PROOF STATE]
proof (prove)
using this:
Im z \<noteq> 0
z = cor r * cis \<phi>
\<phi> = Arg z
0 < r
cis pi = - 1

goal (1 subgoal):
 1. \<phi> \<noteq> pi &&& \<phi> \<noteq> 0
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
\<phi> \<noteq> pi
\<phi> \<noteq> 0

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
hence "sin \<phi> > 0 \<longleftrightarrow> \<phi> > 0" "\<phi> < 0 \<longleftrightarrow> sin \<phi> < 0"
[PROOF STATE]
proof (prove)
using this:
\<phi> \<noteq> pi
\<phi> \<noteq> 0

goal (1 subgoal):
 1. (0 < sin \<phi>) = (0 < \<phi>) &&& (\<phi> < 0) = (sin \<phi> < 0)
[PROOF STEP]
using \<open>\<phi> = Arg z\<close> \<open>\<phi> \<noteq> 0\<close> \<open>\<phi> \<noteq> pi\<close>
[PROOF STATE]
proof (prove)
using this:
\<phi> \<noteq> pi
\<phi> \<noteq> 0
\<phi> = Arg z
\<phi> \<noteq> 0
\<phi> \<noteq> pi

goal (1 subgoal):
 1. (0 < sin \<phi>) = (0 < \<phi>) &&& (\<phi> < 0) = (sin \<phi> < 0)
[PROOF STEP]
using Arg_bounded[of z]
[PROOF STATE]
proof (prove)
using this:
\<phi> \<noteq> pi
\<phi> \<noteq> 0
\<phi> = Arg z
\<phi> \<noteq> 0
\<phi> \<noteq> pi
- pi < Arg z \<and> Arg z \<le> pi

goal (1 subgoal):
 1. (0 < sin \<phi>) = (0 < \<phi>) &&& (\<phi> < 0) = (sin \<phi> < 0)
[PROOF STEP]
by (smt sin_gt_zero sin_le_zero sin_pi_minus sin_0_iff_canon sin_ge_zero)+
[PROOF STATE]
proof (state)
this:
(0 < sin \<phi>) = (0 < \<phi>)
(\<phi> < 0) = (sin \<phi> < 0)

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(0 < Im z) = (0 < sin \<phi>)
(Im z < 0) = (sin \<phi> < 0)
(0 < sin \<phi>) = (0 < \<phi>)
(\<phi> < 0) = (sin \<phi> < 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0 < Im z) = (0 < sin \<phi>)
(Im z < 0) = (sin \<phi> < 0)
(0 < sin \<phi>) = (0 < \<phi>)
(\<phi> < 0) = (sin \<phi> < 0)

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
using \<open>\<phi> = Arg z\<close>
[PROOF STATE]
proof (prove)
using this:
(0 < Im z) = (0 < sin \<phi>)
(Im z < 0) = (sin \<phi> < 0)
(0 < sin \<phi>) = (0 < \<phi>)
(\<phi> < 0) = (sin \<phi> < 0)
\<phi> = Arg z

goal (1 subgoal):
 1. sgn (Arg z) = sgn (Im z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sgn (Arg z) = sgn (Im z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma square_ccsqrt [simp]:
  shows "(ccsqrt x)\<^sup>2 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ccsqrt x)\<^sup>2 = x
[PROOF STEP]
unfolding ccsqrt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rcis (sqrt (cmod x)) (Arg x / 2))\<^sup>2 = x
[PROOF STEP]
by (subst DeMoivre2) (simp add: rcis_cmod_Arg)


[STATEMENT]
lemma ex_complex_sqrt:
  shows "\<exists> s::complex. s*s = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. s * s = z
[PROOF STEP]
unfolding power2_eq_square[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. s\<^sup>2 = z
[PROOF STEP]
by (rule_tac x="csqrt z" in exI) simp


[STATEMENT]
lemma ccsqrt:
  assumes "s * s = z"
  shows "s = ccsqrt z \<or> s = -ccsqrt z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
proof (cases "s = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s = 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
 2. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s = 0

goal (2 subgoals):
 1. s = 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
 2. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s = 0

goal (1 subgoal):
 1. s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s = 0
s * s = z

goal (1 subgoal):
 1. s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
unfolding ccsqrt_def
[PROOF STATE]
proof (prove)
using this:
s = 0
s * s = z

goal (1 subgoal):
 1. s = rcis (sqrt (cmod z)) (Arg z / 2) \<or> s = - rcis (sqrt (cmod z)) (Arg z / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s = ccsqrt z \<or> s = - ccsqrt z

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s \<noteq> 0

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> 0
[PROOF STEP]
obtain k::int where "cmod s * cmod s = cmod z" "2 * Arg s - Arg z = 2*k*pi"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 0

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>cmod s * cmod s = cmod z; 2 * Arg s - Arg z = real_of_int (2 * k) * pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 0
s * s = z

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>cmod s * cmod s = cmod z; 2 * Arg s - Arg z = real_of_int (2 * k) * pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rcis_cmod_Arg[of z] rcis_cmod_Arg[of s]
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 0
s * s = z
rcis (cmod z) (Arg z) = z
rcis (cmod s) (Arg s) = s

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>cmod s * cmod s = cmod z; 2 * Arg s - Arg z = real_of_int (2 * k) * pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using arg_mult[of s s]
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 0
s * s = z
rcis (cmod z) (Arg z) = z
rcis (cmod s) (Arg s) = s
s * s \<noteq> 0 \<Longrightarrow> Arg (s * s) = \<downharpoonright>Arg s + Arg s\<downharpoonleft>

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>cmod s * cmod s = cmod z; 2 * Arg s - Arg z = real_of_int (2 * k) * pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using canon_ang(3)[of "2*Arg s"]
[PROOF STATE]
proof (prove)
using this:
s \<noteq> 0
s * s = z
rcis (cmod z) (Arg z) = z
rcis (cmod s) (Arg s) = s
s * s \<noteq> 0 \<Longrightarrow> Arg (s * s) = \<downharpoonright>Arg s + Arg s\<downharpoonleft>
\<exists>x. 2 * Arg s - \<downharpoonright>2 * Arg s\<downharpoonleft> = 2 * real_of_int x * pi

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>cmod s * cmod s = cmod z; 2 * Arg s - Arg z = real_of_int (2 * k) * pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: norm_mult arg_mult)
[PROOF STATE]
proof (state)
this:
cmod s * cmod s = cmod z
2 * Arg s - Arg z = real_of_int (2 * k) * pi

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
have *: "sqrt (cmod z) = cmod s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (cmod z) = cmod s
[PROOF STEP]
using \<open>cmod s * cmod s = cmod z\<close>
[PROOF STATE]
proof (prove)
using this:
cmod s * cmod s = cmod z

goal (1 subgoal):
 1. sqrt (cmod z) = cmod s
[PROOF STEP]
by (smt norm_not_less_zero real_sqrt_abs2)
[PROOF STATE]
proof (state)
this:
sqrt (cmod z) = cmod s

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
have **: "Arg z / 2 = Arg s - k*pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg z / 2 = Arg s - real_of_int k * pi
[PROOF STEP]
using \<open>2 * Arg s - Arg z = 2*k*pi\<close>
[PROOF STATE]
proof (prove)
using this:
2 * Arg s - Arg z = real_of_int (2 * k) * pi

goal (1 subgoal):
 1. Arg z / 2 = Arg s - real_of_int k * pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Arg z / 2 = Arg s - real_of_int k * pi

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
have "cis (Arg s - k*pi) = cis (Arg s) \<or> cis (Arg s - k*pi) = -cis (Arg s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
proof (cases "even k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. even k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
 2. odd k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
even k

goal (2 subgoals):
 1. even k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
 2. odd k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
hence "cis (Arg s - k*pi) = cis (Arg s)"
[PROOF STATE]
proof (prove)
using this:
even k

goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = cis (Arg s)
[PROOF STEP]
by (simp add: cis_def complex.corec cos_diff sin_diff)
[PROOF STATE]
proof (state)
this:
cis (Arg s - real_of_int k * pi) = cis (Arg s)

goal (2 subgoals):
 1. even k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
 2. odd k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = cis (Arg s)

goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal (1 subgoal):
 1. odd k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
odd k

goal (1 subgoal):
 1. odd k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
hence "cis (Arg s - k*pi) = -cis (Arg s)"
[PROOF STATE]
proof (prove)
using this:
odd k

goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
by (simp add: cis_def complex.corec Complex_eq cos_diff sin_diff)
[PROOF STATE]
proof (state)
this:
cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal (1 subgoal):
 1. odd k \<Longrightarrow> cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal (1 subgoal):
 1. s \<noteq> 0 \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = cis (Arg s) \<or> cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal (1 subgoal):
 1. s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cis (Arg s - real_of_int k * pi) = cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
 2. cis (Arg s - real_of_int k * pi) = - cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
assume ***: "cis (Arg s - k * pi) = cis (Arg s)"
[PROOF STATE]
proof (state)
this:
cis (Arg s - real_of_int k * pi) = cis (Arg s)

goal (2 subgoals):
 1. cis (Arg s - real_of_int k * pi) = cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
 2. cis (Arg s - real_of_int k * pi) = - cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
hence "s = ccsqrt z"
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = cis (Arg s)

goal (1 subgoal):
 1. s = ccsqrt z
[PROOF STEP]
using rcis_cmod_Arg[of s]
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = cis (Arg s)
rcis (cmod s) (Arg s) = s

goal (1 subgoal):
 1. s = ccsqrt z
[PROOF STEP]
unfolding ccsqrt_def rcis_def
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = cis (Arg s)
cor (cmod s) * cis (Arg s) = s

goal (1 subgoal):
 1. s = cor (sqrt (cmod z)) * cis (Arg z / 2)
[PROOF STEP]
by (subst *, subst **, subst ***, simp)
[PROOF STATE]
proof (state)
this:
s = ccsqrt z

goal (2 subgoals):
 1. cis (Arg s - real_of_int k * pi) = cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
 2. cis (Arg s - real_of_int k * pi) = - cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s = ccsqrt z

goal (1 subgoal):
 1. s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s = ccsqrt z \<or> s = - ccsqrt z

goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = - cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = - cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
assume ***: "cis (Arg s - k * pi) = -cis (Arg s)"
[PROOF STATE]
proof (state)
this:
cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = - cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
hence "s = - ccsqrt z"
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = - cis (Arg s)

goal (1 subgoal):
 1. s = - ccsqrt z
[PROOF STEP]
using rcis_cmod_Arg[of s]
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = - cis (Arg s)
rcis (cmod s) (Arg s) = s

goal (1 subgoal):
 1. s = - ccsqrt z
[PROOF STEP]
unfolding ccsqrt_def rcis_def
[PROOF STATE]
proof (prove)
using this:
cis (Arg s - real_of_int k * pi) = - cis (Arg s)
cor (cmod s) * cis (Arg s) = s

goal (1 subgoal):
 1. s = - (cor (sqrt (cmod z)) * cis (Arg z / 2))
[PROOF STEP]
by (subst *, subst **, subst ***, simp)
[PROOF STATE]
proof (state)
this:
s = - ccsqrt z

goal (1 subgoal):
 1. cis (Arg s - real_of_int k * pi) = - cis (Arg s) \<Longrightarrow> s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s = - ccsqrt z

goal (1 subgoal):
 1. s = ccsqrt z \<or> s = - ccsqrt z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s = ccsqrt z \<or> s = - ccsqrt z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s = ccsqrt z \<or> s = - ccsqrt z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma null_ccsqrt [simp]:
  shows "ccsqrt x = 0 \<longleftrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ccsqrt x = 0) = (x = 0)
[PROOF STEP]
unfolding ccsqrt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rcis (sqrt (cmod x)) (Arg x / 2) = 0) = (x = 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma ccsqrt_mult:
  shows "ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or>
         ccsqrt (a * b) = - ccsqrt a * ccsqrt b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
proof (cases "a = 0 \<or> b = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<or> b = 0 \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
 2. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = 0 \<or> b = 0

goal (2 subgoals):
 1. a = 0 \<or> b = 0 \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
 2. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = 0 \<or> b = 0

goal (1 subgoal):
 1. ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b

goal (1 subgoal):
 1. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (a = 0 \<or> b = 0)

goal (1 subgoal):
 1. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
obtain k::int where "Arg a + Arg b - \<downharpoonright>Arg a + Arg b\<downharpoonleft> = 2 * real_of_int k * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. Arg a + Arg b - \<downharpoonright>Arg a + Arg b\<downharpoonleft> = 2 * real_of_int k * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using canon_ang(3)[of "Arg a + Arg b"]
[PROOF STATE]
proof (prove)
using this:
\<exists>x. Arg a + Arg b - \<downharpoonright>Arg a + Arg b\<downharpoonleft> = 2 * real_of_int x * pi

goal (1 subgoal):
 1. (\<And>k. Arg a + Arg b - \<downharpoonright>Arg a + Arg b\<downharpoonleft> = 2 * real_of_int k * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg a + Arg b - \<downharpoonright>Arg a + Arg b\<downharpoonleft> = 2 * real_of_int k * pi

goal (1 subgoal):
 1. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
hence *: "\<downharpoonright>Arg a + Arg b\<downharpoonleft> = Arg a + Arg b - 2 * (real_of_int k) * pi"
[PROOF STATE]
proof (prove)
using this:
Arg a + Arg b - \<downharpoonright>Arg a + Arg b\<downharpoonleft> = 2 * real_of_int k * pi

goal (1 subgoal):
 1. \<downharpoonright>Arg a + Arg b\<downharpoonleft> = Arg a + Arg b - 2 * real_of_int k * pi
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<downharpoonright>Arg a + Arg b\<downharpoonleft> = Arg a + Arg b - 2 * real_of_int k * pi

goal (1 subgoal):
 1. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
have "cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = cis (Arg a / 2 + Arg b / 2) \<or> cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = - cis (Arg a / 2 + Arg b / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = cis (Arg a / 2 + Arg b / 2) \<or> cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = - cis (Arg a / 2 + Arg b / 2)
[PROOF STEP]
using cos_even_kpi[of k] cos_odd_kpi[of k]
[PROOF STATE]
proof (prove)
using this:
even k \<Longrightarrow> cos (real_of_int k * pi) = 1
odd k \<Longrightarrow> cos (real_of_int k * pi) = - 1

goal (1 subgoal):
 1. cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = cis (Arg a / 2 + Arg b / 2) \<or> cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = - cis (Arg a / 2 + Arg b / 2)
[PROOF STEP]
by ((subst *)+, (subst diff_divide_distrib)+, (subst add_divide_distrib)+)
       (cases "even k", auto simp add: cis_def complex.corec Complex_eq cos_diff sin_diff)
[PROOF STATE]
proof (state)
this:
cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = cis (Arg a / 2 + Arg b / 2) \<or> cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = - cis (Arg a / 2 + Arg b / 2)

goal (1 subgoal):
 1. \<not> (a = 0 \<or> b = 0) \<Longrightarrow> ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = cis (Arg a / 2 + Arg b / 2) \<or> cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = - cis (Arg a / 2 + Arg b / 2)

goal (1 subgoal):
 1. ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = cis (Arg a / 2 + Arg b / 2) \<or> cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = - cis (Arg a / 2 + Arg b / 2)
\<not> (a = 0 \<or> b = 0)

goal (1 subgoal):
 1. ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b
[PROOF STEP]
unfolding ccsqrt_def
[PROOF STATE]
proof (prove)
using this:
cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = cis (Arg a / 2 + Arg b / 2) \<or> cis (\<downharpoonright>Arg a + Arg b\<downharpoonleft> / 2) = - cis (Arg a / 2 + Arg b / 2)
\<not> (a = 0 \<or> b = 0)

goal (1 subgoal):
 1. rcis (sqrt (cmod (a * b))) (Arg (a * b) / 2) = rcis (sqrt (cmod a)) (Arg a / 2) * rcis (sqrt (cmod b)) (Arg b / 2) \<or> rcis (sqrt (cmod (a * b))) (Arg (a * b) / 2) = - rcis (sqrt (cmod a)) (Arg a / 2) * rcis (sqrt (cmod b)) (Arg b / 2)
[PROOF STEP]
by (smt (verit, best) arg_mult mult_minus_left mult_minus_right no_zero_divisors norm_mult rcis_def rcis_mult real_sqrt_mult)
[PROOF STATE]
proof (state)
this:
ccsqrt (a * b) = ccsqrt a * ccsqrt b \<or> ccsqrt (a * b) = - ccsqrt a * ccsqrt b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma csqrt_real:
  assumes "is_real x"
  shows "(Re x \<ge> 0 \<and> ccsqrt x = cor (sqrt (Re x))) \<or>
         (Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- (Re x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
 2. x \<noteq> 0 \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
 2. x \<noteq> 0 \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
proof (cases "Re x > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
 2. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < Re x

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
 2. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
hence "Arg x = 0"
[PROOF STATE]
proof (prove)
using this:
0 < Re x

goal (1 subgoal):
 1. Arg x = 0
[PROOF STEP]
using \<open>is_real x\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Re x
is_real x

goal (1 subgoal):
 1. Arg x = 0
[PROOF STEP]
by (metis arg_complex_of_real_positive complex_of_real_Re)
[PROOF STATE]
proof (state)
this:
Arg x = 0

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
 2. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg x = 0

goal (1 subgoal):
 1. 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
using \<open>Re x > 0\<close> \<open>is_real x\<close>
[PROOF STATE]
proof (prove)
using this:
Arg x = 0
0 < Re x
is_real x

goal (1 subgoal):
 1. 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
unfolding ccsqrt_def
[PROOF STATE]
proof (prove)
using this:
Arg x = 0
0 < Re x
is_real x

goal (1 subgoal):
 1. 0 \<le> Re x \<and> rcis (sqrt (cmod x)) (Arg x / 2) = cor (sqrt (Re x)) \<or> Re x < 0 \<and> rcis (sqrt (cmod x)) (Arg x / 2) = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
by (simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < Re x

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
hence "Re x < 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Re x

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

goal (1 subgoal):
 1. Re x < 0
[PROOF STEP]
using complex_eq_if_Re_eq
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Re x
x \<noteq> 0
is_real x
\<lbrakk>is_real ?z1.0; is_real ?z2.0\<rbrakk> \<Longrightarrow> (?z1.0 = ?z2.0) = (Re ?z1.0 = Re ?z2.0)

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

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
hence "Arg x = pi"
[PROOF STATE]
proof (prove)
using this:
Re x < 0

goal (1 subgoal):
 1. Arg x = pi
[PROOF STEP]
using \<open>is_real x\<close>
[PROOF STATE]
proof (prove)
using this:
Re x < 0
is_real x

goal (1 subgoal):
 1. Arg x = pi
[PROOF STEP]
by (metis arg_complex_of_real_negative complex_of_real_Re)
[PROOF STATE]
proof (state)
this:
Arg x = pi

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg x = pi

goal (1 subgoal):
 1. 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
using \<open>Re x < 0\<close> \<open>is_real x\<close>
[PROOF STATE]
proof (prove)
using this:
Arg x = pi
Re x < 0
is_real x

goal (1 subgoal):
 1. 0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
unfolding ccsqrt_def rcis_def
[PROOF STATE]
proof (prove)
using this:
Arg x = pi
Re x < 0
is_real x

goal (1 subgoal):
 1. 0 \<le> Re x \<and> cor (sqrt (cmod x)) * cis (Arg x / 2) = cor (sqrt (Re x)) \<or> Re x < 0 \<and> cor (sqrt (cmod x)) * cis (Arg x / 2) = \<i> * cor (sqrt (- Re x))
[PROOF STEP]
by (simp add: cis_def complex.corec Complex_eq cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> Re x \<and> ccsqrt x = cor (sqrt (Re x)) \<or> Re x < 0 \<and> ccsqrt x = \<i> * cor (sqrt (- Re x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_real_rot_to_x_axis:
  assumes "z \<noteq> 0"
  shows "is_real (cis (-Arg z) * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (cis (- Arg z) * z)
[PROOF STEP]
proof (cases "Arg z = pi")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Arg z = pi \<Longrightarrow> is_real (cis (- Arg z) * z)
 2. Arg z \<noteq> pi \<Longrightarrow> is_real (cis (- Arg z) * z)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Arg z = pi

goal (2 subgoals):
 1. Arg z = pi \<Longrightarrow> is_real (cis (- Arg z) * z)
 2. Arg z \<noteq> pi \<Longrightarrow> is_real (cis (- Arg z) * z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg z = pi

goal (1 subgoal):
 1. is_real (cis (- Arg z) * z)
[PROOF STEP]
using is_real_arg1[of z]
[PROOF STATE]
proof (prove)
using this:
Arg z = pi
Arg z = 0 \<or> Arg z = pi \<Longrightarrow> is_real z

goal (1 subgoal):
 1. is_real (cis (- Arg z) * z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real (cis (- Arg z) * z)

goal (1 subgoal):
 1. Arg z \<noteq> pi \<Longrightarrow> is_real (cis (- Arg z) * z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg z \<noteq> pi \<Longrightarrow> is_real (cis (- Arg z) * z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Arg z \<noteq> pi

goal (1 subgoal):
 1. Arg z \<noteq> pi \<Longrightarrow> is_real (cis (- Arg z) * z)
[PROOF STEP]
hence "\<downharpoonright>- Arg z\<downharpoonleft> = - Arg z"
[PROOF STATE]
proof (prove)
using this:
Arg z \<noteq> pi

goal (1 subgoal):
 1. \<downharpoonright>- Arg z\<downharpoonleft> = - Arg z
[PROOF STEP]
using canon_ang_eqI[of "- Arg z" "-Arg z"]
[PROOF STATE]
proof (prove)
using this:
Arg z \<noteq> pi
\<lbrakk>\<exists>x. - Arg z - - Arg z = 2 * real_of_int x * pi; - pi < - Arg z \<and> - Arg z \<le> pi\<rbrakk> \<Longrightarrow> \<downharpoonright>- Arg z\<downharpoonleft> = - Arg z

goal (1 subgoal):
 1. \<downharpoonright>- Arg z\<downharpoonleft> = - Arg z
[PROOF STEP]
using Arg_bounded[of z]
[PROOF STATE]
proof (prove)
using this:
Arg z \<noteq> pi
\<lbrakk>\<exists>x. - Arg z - - Arg z = 2 * real_of_int x * pi; - pi < - Arg z \<and> - Arg z \<le> pi\<rbrakk> \<Longrightarrow> \<downharpoonright>- Arg z\<downharpoonleft> = - Arg z
- pi < Arg z \<and> Arg z \<le> pi

goal (1 subgoal):
 1. \<downharpoonright>- Arg z\<downharpoonleft> = - Arg z
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<downharpoonright>- Arg z\<downharpoonleft> = - Arg z

goal (1 subgoal):
 1. Arg z \<noteq> pi \<Longrightarrow> is_real (cis (- Arg z) * z)
[PROOF STEP]
hence "Arg (cis (- (Arg z)) * z) = 0"
[PROOF STATE]
proof (prove)
using this:
\<downharpoonright>- Arg z\<downharpoonleft> = - Arg z

goal (1 subgoal):
 1. Arg (cis (- Arg z) * z) = 0
[PROOF STEP]
using arg_mult[of "cis (- (Arg z))" z] \<open>z \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<downharpoonright>- Arg z\<downharpoonleft> = - Arg z
cis (- Arg z) * z \<noteq> 0 \<Longrightarrow> Arg (cis (- Arg z) * z) = \<downharpoonright>Arg (cis (- Arg z)) + Arg z\<downharpoonleft>
z \<noteq> 0

goal (1 subgoal):
 1. Arg (cis (- Arg z) * z) = 0
[PROOF STEP]
using arg_cis[of "- Arg z"]
[PROOF STATE]
proof (prove)
using this:
\<downharpoonright>- Arg z\<downharpoonleft> = - Arg z
cis (- Arg z) * z \<noteq> 0 \<Longrightarrow> Arg (cis (- Arg z) * z) = \<downharpoonright>Arg (cis (- Arg z)) + Arg z\<downharpoonleft>
z \<noteq> 0
Arg (cis (- Arg z)) = \<downharpoonright>- Arg z\<downharpoonleft>

goal (1 subgoal):
 1. Arg (cis (- Arg z) * z) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Arg (cis (- Arg z) * z) = 0

goal (1 subgoal):
 1. Arg z \<noteq> pi \<Longrightarrow> is_real (cis (- Arg z) * z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg (cis (- Arg z) * z) = 0

goal (1 subgoal):
 1. is_real (cis (- Arg z) * z)
[PROOF STEP]
using is_real_arg1[of "cis (- Arg z) * z"]
[PROOF STATE]
proof (prove)
using this:
Arg (cis (- Arg z) * z) = 0
Arg (cis (- Arg z) * z) = 0 \<or> Arg (cis (- Arg z) * z) = pi \<Longrightarrow> is_real (cis (- Arg z) * z)

goal (1 subgoal):
 1. is_real (cis (- Arg z) * z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real (cis (- Arg z) * z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma positive_rot_to_x_axis:
  assumes "z \<noteq> 0"
  shows "Re (cis (-Arg z) * z) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Re (cis (- Arg z) * z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. 0 < Re (cis (- Arg z) * z)
[PROOF STEP]
by (smt Re_complex_of_real cis_rcis_eq mult_cancel_right1 rcis_cmod_Arg rcis_mult rcis_zero_arg zero_less_norm_iff)


[STATEMENT]
lemma cmod_1_plus_mult_le:
  shows "cmod (1 + z*w) \<le> sqrt((1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (1 + z * w) \<le> sqrt ((1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (1 + z * w) \<le> sqrt ((1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2))
[PROOF STEP]
have "Re ((1+z*w)*(1+cnj z*cnj w)) \<le> Re (1+z*cnj z)* Re (1+w*cnj w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)
[PROOF STEP]
have "Re ((w - cnj z)*cnj(w - cnj z)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re ((w - cnj z) * cnj (w - cnj z))
[PROOF STEP]
by (subst complex_mult_cnj_cmod) (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
0 \<le> Re ((w - cnj z) * cnj (w - cnj z))

goal (1 subgoal):
 1. Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)
[PROOF STEP]
hence "Re (z*w + cnj z * cnj w) \<le> Re (w*cnj w) + Re(z*cnj z)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re ((w - cnj z) * cnj (w - cnj z))

goal (1 subgoal):
 1. Re (z * w + cnj z * cnj w) \<le> Re (w * cnj w) + Re (z * cnj z)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
Re (z * w + cnj z * cnj w) \<le> Re (w * cnj w) + Re (z * cnj z)

goal (1 subgoal):
 1. Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Re (z * w + cnj z * cnj w) \<le> Re (w * cnj w) + Re (z * cnj z)

goal (1 subgoal):
 1. Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)

goal (1 subgoal):
 1. cmod (1 + z * w) \<le> sqrt ((1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2))
[PROOF STEP]
hence "(cmod (1 + z * w))\<^sup>2 \<le> (1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
Re ((1 + z * w) * (1 + cnj z * cnj w)) \<le> Re (1 + z * cnj z) * Re (1 + w * cnj w)

goal (1 subgoal):
 1. (cmod (1 + z * w))\<^sup>2 \<le> (1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2)
[PROOF STEP]
by (subst cmod_square)+ simp
[PROOF STATE]
proof (state)
this:
(cmod (1 + z * w))\<^sup>2 \<le> (1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2)

goal (1 subgoal):
 1. cmod (1 + z * w) \<le> sqrt ((1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(cmod (1 + z * w))\<^sup>2 \<le> (1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2)

goal (1 subgoal):
 1. cmod (1 + z * w) \<le> sqrt ((1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2))
[PROOF STEP]
by (metis abs_norm_cancel real_sqrt_abs real_sqrt_le_iff)
[PROOF STATE]
proof (state)
this:
cmod (1 + z * w) \<le> sqrt ((1 + (cmod z)\<^sup>2) * (1 + (cmod w)\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmod_diff_ge:
  shows "cmod (b - c) \<ge> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
have "(cmod (b - c))\<^sup>2 + (1/2*Im(b*cnj c - c*cnj b))\<^sup>2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (cmod (b - c))\<^sup>2 + (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> (cmod (b - c))\<^sup>2 + (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
hence "(cmod (b - c))\<^sup>2 \<ge> - (1/2*Im(b*cnj c - c*cnj b))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
0 \<le> (cmod (b - c))\<^sup>2 + (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2

goal (1 subgoal):
 1. - (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2 \<le> (cmod (b - c))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2 \<le> (cmod (b - c))\<^sup>2

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
hence "(cmod (b - c))\<^sup>2 \<ge> (1/2*Re(b*cnj c + c*cnj b))\<^sup>2 - Re(b*cnj b*c*cnj c) "
[PROOF STATE]
proof (prove)
using this:
- (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2 \<le> (cmod (b - c))\<^sup>2

goal (1 subgoal):
 1. (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> (cmod (b - c))\<^sup>2
[PROOF STEP]
by (auto simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> (cmod (b - c))\<^sup>2

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
hence "Re ((b - c)*(cnj b - cnj c)) \<ge> (1/2*Re(b*cnj c + c*cnj b))\<^sup>2 - Re(b*cnj b*c*cnj c)"
[PROOF STATE]
proof (prove)
using this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> (cmod (b - c))\<^sup>2

goal (1 subgoal):
 1. (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b - c) * (cnj b - cnj c))
[PROOF STEP]
by (subst (asm) cmod_square) simp
[PROOF STATE]
proof (state)
this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b - c) * (cnj b - cnj c))

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b - c) * (cnj b - cnj c))

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
have "(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re(b*cnj b) + Re(c*cnj c) + Re(b*cnj b*c*cnj c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)
[PROOF STEP]
by (subst cmod_square)+ (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
have "(1 + Re (scalprod b c))\<^sup>2 = 1 + 2*Re(scalprod b c) + ((Re (scalprod b c))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + Re (scalprod b c))\<^sup>2 = 1 + 2 * Re (scalprod b c) + (Re (scalprod b c))\<^sup>2
[PROOF STEP]
by (subst power2_sum) simp
[PROOF STATE]
proof (state)
this:
(1 + Re (scalprod b c))\<^sup>2 = 1 + 2 * Re (scalprod b c) + (Re (scalprod b c))\<^sup>2

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
hence "(1 + Re (scalprod b c))\<^sup>2 = 1 + Re(b*cnj c + c*cnj b) + (1/2 * Re (b*cnj c + c*cnj b))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(1 + Re (scalprod b c))\<^sup>2 = 1 + 2 * Re (scalprod b c) + (Re (scalprod b c))\<^sup>2

goal (1 subgoal):
 1. (1 + Re (scalprod b c))\<^sup>2 = 1 + Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 + Re (scalprod b c))\<^sup>2 = 1 + Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b - c) * (cnj b - cnj c))
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)
(1 + Re (scalprod b c))\<^sup>2 = 1 + Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2
[PROOF STEP]
have "(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) \<ge> (1 + Re (scalprod b c))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b - c) * (cnj b - cnj c))
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)
(1 + Re (scalprod b c))\<^sup>2 = 1 + Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2

goal (1 subgoal):
 1. (1 + Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(1 + Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 + Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
have "sqrt((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))
[PROOF STEP]
by (metis one_power2 real_sqrt_sum_squares_mult_ge_zero)
[PROOF STATE]
proof (state)
this:
0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(1 + Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)
0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))
[PROOF STEP]
have "sqrt((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<ge> 1 + Re (scalprod b c)"
[PROOF STATE]
proof (prove)
using this:
(1 + Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)
0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. 1 + Re (scalprod b c) \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))
[PROOF STEP]
by (metis power2_le_imp_le real_sqrt_ge_0_iff real_sqrt_pow2_iff)
[PROOF STATE]
proof (state)
this:
1 + Re (scalprod b c) \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
hence "Re ((b - c) * (cnj b - cnj c)) \<ge> 1 + Re (c*cnj c) + 1 + Re (b*cnj b) - 2*sqrt((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))"
[PROOF STATE]
proof (prove)
using this:
1 + Re (scalprod b c) \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<le> Re ((b - c) * (cnj b - cnj c))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<le> Re ((b - c) * (cnj b - cnj c))

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
hence *: "(cmod (b - c))\<^sup>2 \<ge> (sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<le> Re ((b - c) * (cnj b - cnj c))

goal (1 subgoal):
 1. (sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2
[PROOF STEP]
apply (subst cmod_square)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<le> Re ((b - c) * (cnj b - cnj c))\<rbrakk> \<Longrightarrow> (sqrt (1 + Re (b * cnj b)) - sqrt (1 + Re (c * cnj c)))\<^sup>2 \<le> Re ((b - c) * cnj (b - c))
[PROOF STEP]
apply (subst (asm) cmod_square)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c))\<rbrakk> \<Longrightarrow> (sqrt (1 + Re (b * cnj b)) - sqrt (1 + Re (c * cnj c)))\<^sup>2 \<le> Re ((b - c) * cnj (b - c))
[PROOF STEP]
apply (subst power2_diff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c))\<rbrakk> \<Longrightarrow> (sqrt (1 + Re (b * cnj b)))\<^sup>2 + (sqrt (1 + Re (c * cnj c)))\<^sup>2 - 2 * sqrt (1 + Re (b * cnj b)) * sqrt (1 + Re (c * cnj c)) \<le> Re ((b - c) * cnj (b - c))
[PROOF STEP]
apply (subst real_sqrt_pow2, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c))\<rbrakk> \<Longrightarrow> 1 + Re (b * cnj b) + (sqrt (1 + Re (c * cnj c)))\<^sup>2 - 2 * sqrt (1 + Re (b * cnj b)) * sqrt (1 + Re (c * cnj c)) \<le> Re ((b - c) * cnj (b - c))
[PROOF STEP]
apply (subst real_sqrt_pow2, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c)); 1 + Re (c * cnj c) + 1 + Re (b * cnj b) - 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))) \<le> Re ((b - c) * (cnj b - cnj c))\<rbrakk> \<Longrightarrow> 1 + Re (b * cnj b) + (1 + Re (c * cnj c)) - 2 * sqrt (1 + Re (b * cnj b)) * sqrt (1 + Re (c * cnj c)) \<le> Re ((b - c) * cnj (b - c))
[PROOF STEP]
apply (simp add: real_sqrt_mult)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
proof (cases "sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
 2. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)

goal (2 subgoals):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
 2. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
using power2_le_imp_le[OF *]
[PROOF STATE]
proof (prove)
using this:
0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)
0 \<le> cmod (b - c) \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)

goal (1 subgoal):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
hence "0 \<ge> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> 0
[PROOF STEP]
by (metis less_eq_real_def linorder_neqE_linordered_idom)
[PROOF STATE]
proof (state)
this:
sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> 0

goal (1 subgoal):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> 0

goal (1 subgoal):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
have "cmod (b - c) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> cmod (b - c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> cmod (b - c)

goal (1 subgoal):
 1. \<lbrakk>(sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2))\<^sup>2 \<le> (cmod (b - c))\<^sup>2; \<not> 0 < sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2)\<rbrakk> \<Longrightarrow> sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> 0
0 \<le> cmod (b - c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> 0
0 \<le> cmod (b - c)

goal (1 subgoal):
 1. sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)
[PROOF STEP]
by (metis add_increasing monoid_add_class.add.right_neutral)
[PROOF STATE]
proof (state)
this:
sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sqrt (1 + (cmod b)\<^sup>2) - sqrt (1 + (cmod c)\<^sup>2) \<le> cmod (b - c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmod_diff_le:
  shows "cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
have "(cmod (b + c))\<^sup>2 + (1/2*Im(b*cnj c - c*cnj b))\<^sup>2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (cmod (b + c))\<^sup>2 + (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> (cmod (b + c))\<^sup>2 + (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
hence "(cmod (b + c))\<^sup>2 \<ge> - (1/2*Im(b*cnj c - c*cnj b))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
0 \<le> (cmod (b + c))\<^sup>2 + (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2

goal (1 subgoal):
 1. - (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2 \<le> (cmod (b + c))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2 \<le> (cmod (b + c))\<^sup>2

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
hence "(cmod (b + c))\<^sup>2 \<ge> (1/2*Re(b*cnj c + c*cnj b))\<^sup>2 - Re(b*cnj b*c*cnj c) "
[PROOF STATE]
proof (prove)
using this:
- (1 / 2 * Im (b * cnj c - c * cnj b))\<^sup>2 \<le> (cmod (b + c))\<^sup>2

goal (1 subgoal):
 1. (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> (cmod (b + c))\<^sup>2
[PROOF STEP]
by (auto simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> (cmod (b + c))\<^sup>2

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
hence "Re ((b + c)*(cnj b + cnj c)) \<ge> (1/2*Re(b*cnj c + c*cnj b))\<^sup>2 - Re(b*cnj b*c*cnj c)"
[PROOF STATE]
proof (prove)
using this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> (cmod (b + c))\<^sup>2

goal (1 subgoal):
 1. (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b + c) * (cnj b + cnj c))
[PROOF STEP]
by (subst (asm) cmod_square) simp
[PROOF STATE]
proof (state)
this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b + c) * (cnj b + cnj c))

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b + c) * (cnj b + cnj c))

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
have "(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re(b*cnj b) + Re(c*cnj c) + Re(b*cnj b*c*cnj c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)
[PROOF STEP]
by (subst cmod_square)+ (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
have ++: "2*Re(scalprod b c) = Re(b*cnj c + c*cnj b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * Re (scalprod b c) = Re (b * cnj c + c * cnj b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * Re (scalprod b c) = Re (b * cnj c + c * cnj b)

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
have "(1 - Re (scalprod b c))\<^sup>2 = 1 - 2*Re(scalprod b c) + ((Re (scalprod b c))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - Re (scalprod b c))\<^sup>2 = 1 - 2 * Re (scalprod b c) + (Re (scalprod b c))\<^sup>2
[PROOF STEP]
by (subst power2_diff) simp
[PROOF STATE]
proof (state)
this:
(1 - Re (scalprod b c))\<^sup>2 = 1 - 2 * Re (scalprod b c) + (Re (scalprod b c))\<^sup>2

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
hence "(1 - Re (scalprod b c))\<^sup>2 = 1 - Re(b*cnj c + c*cnj b) + (1/2 * Re (b*cnj c + c*cnj b))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(1 - Re (scalprod b c))\<^sup>2 = 1 - 2 * Re (scalprod b c) + (Re (scalprod b c))\<^sup>2

goal (1 subgoal):
 1. (1 - Re (scalprod b c))\<^sup>2 = 1 - Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2
[PROOF STEP]
by (subst ++[symmetric]) simp
[PROOF STATE]
proof (state)
this:
(1 - Re (scalprod b c))\<^sup>2 = 1 - Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b + c) * (cnj b + cnj c))
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)
(1 - Re (scalprod b c))\<^sup>2 = 1 - Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2
[PROOF STEP]
have "(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) \<ge> (1 - Re (scalprod b c))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2 - Re (b * cnj b * c * cnj c) \<le> Re ((b + c) * (cnj b + cnj c))
(1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2) = 1 + Re (b * cnj b) + Re (c * cnj c) + Re (b * cnj b * c * cnj c)
(1 - Re (scalprod b c))\<^sup>2 = 1 - Re (b * cnj c + c * cnj b) + (1 / 2 * Re (b * cnj c + c * cnj b))\<^sup>2

goal (1 subgoal):
 1. (1 - Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(1 - Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 - Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
have "sqrt((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))
[PROOF STEP]
by (metis one_power2 real_sqrt_sum_squares_mult_ge_zero)
[PROOF STATE]
proof (state)
this:
0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(1 - Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)
0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))
[PROOF STEP]
have "sqrt((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)) \<ge> 1 - Re (scalprod b c)"
[PROOF STATE]
proof (prove)
using this:
(1 - Re (scalprod b c))\<^sup>2 \<le> (1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)
0 \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. 1 - Re (scalprod b c) \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))
[PROOF STEP]
by (metis power2_le_imp_le real_sqrt_ge_0_iff real_sqrt_pow2_iff)
[PROOF STATE]
proof (state)
this:
1 - Re (scalprod b c) \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
hence "Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c*cnj c) + 1 + Re (b*cnj b) + 2*sqrt((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))"
[PROOF STATE]
proof (prove)
using this:
1 - Re (scalprod b c) \<le> sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
hence *: "(cmod (b - c))\<^sup>2 \<le> (sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))

goal (1 subgoal):
 1. (cmod (b - c))\<^sup>2 \<le> (sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2))\<^sup>2
[PROOF STEP]
apply (subst cmod_square)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2)); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + (cmod b)\<^sup>2) * (1 + (cmod c)\<^sup>2))\<rbrakk> \<Longrightarrow> Re ((b - c) * cnj (b - c)) \<le> (sqrt (1 + Re (b * cnj b)) + sqrt (1 + Re (c * cnj c)))\<^sup>2
[PROOF STEP]
apply (subst (asm) cmod_square)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c)))\<rbrakk> \<Longrightarrow> Re ((b - c) * cnj (b - c)) \<le> (sqrt (1 + Re (b * cnj b)) + sqrt (1 + Re (c * cnj c)))\<^sup>2
[PROOF STEP]
apply (subst power2_sum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c)))\<rbrakk> \<Longrightarrow> Re ((b - c) * cnj (b - c)) \<le> (sqrt (1 + Re (b * cnj b)))\<^sup>2 + (sqrt (1 + Re (c * cnj c)))\<^sup>2 + 2 * sqrt (1 + Re (b * cnj b)) * sqrt (1 + Re (c * cnj c))
[PROOF STEP]
apply (subst real_sqrt_pow2, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c)))\<rbrakk> \<Longrightarrow> Re ((b - c) * cnj (b - c)) \<le> 1 + Re (b * cnj b) + (sqrt (1 + Re (c * cnj c)))\<^sup>2 + 2 * sqrt (1 + Re (b * cnj b)) * sqrt (1 + Re (c * cnj c))
[PROOF STEP]
apply (subst real_sqrt_pow2, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c))); Re ((b - c) * (cnj b - cnj c)) \<le> 1 + Re (c * cnj c) + 1 + Re (b * cnj b) + 2 * sqrt ((1 + Re (b * cnj b)) * (1 + Re (c * cnj c)))\<rbrakk> \<Longrightarrow> Re ((b - c) * cnj (b - c)) \<le> 1 + Re (b * cnj b) + (1 + Re (c * cnj c)) + 2 * sqrt (1 + Re (b * cnj b)) * sqrt (1 + Re (c * cnj c))
[PROOF STEP]
apply (simp add: real_sqrt_mult)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(cmod (b - c))\<^sup>2 \<le> (sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2))\<^sup>2

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(cmod (b - c))\<^sup>2 \<le> (sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2))\<^sup>2

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
using power2_le_imp_le[OF *]
[PROOF STATE]
proof (prove)
using this:
(cmod (b - c))\<^sup>2 \<le> (sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2))\<^sup>2
0 \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2) \<Longrightarrow> cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)

goal (1 subgoal):
 1. cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (b - c) \<le> sqrt (1 + (cmod b)\<^sup>2) + sqrt (1 + (cmod c)\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_complex_to_complex [simp]:
  fixes z1 z2 :: complex
  assumes "z1 \<noteq> 0" and "z2 \<noteq> 0"
  shows "\<exists>k. k \<noteq> 0 \<and> z2 = k * z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> z2 = k * z1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z1 \<noteq> 0
z2 \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> z2 = k * z1
[PROOF STEP]
by (rule_tac x="z2/z1" in exI) simp


[STATEMENT]
lemma ex_complex_to_one [simp]:
  fixes z::complex
  assumes "z \<noteq> 0"
  shows "\<exists>k. k \<noteq> 0 \<and> k * z = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> k * z = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> k * z = 1
[PROOF STEP]
by (rule_tac x="1/z" in exI) simp


[STATEMENT]
lemma ex_complex_to_complex2 [simp]:
  fixes z::complex
  shows "\<exists>k. k \<noteq> 0 \<and> k * z = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> k * z = z
[PROOF STEP]
by (rule_tac x="1" in exI) simp


[STATEMENT]
lemma CoPw_iDM1: "CoPw \<eta> \<Longrightarrow> iDM1 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CoPw \<eta> \<Longrightarrow> iDM1 \<eta>
[PROOF STEP]
unfolding Defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. contains (\<lambda>b. contains (\<eta> a) (\<eta> b)) (\<lambda>b. contains b a) \<Longrightarrow> \<forall>S. contains \<^bold>\<And>Ra[\<eta>|S] (\<eta> \<^bold>\<Or>S)
[PROOF STEP]
by (smt Ra_restr_all sup_char)


[STATEMENT]
lemma CoPw_iDM2: "CoPw \<eta> \<Longrightarrow> iDM2 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CoPw \<eta> \<Longrightarrow> iDM2 \<eta>
[PROOF STEP]
unfolding Defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. contains (\<lambda>b. contains (\<eta> a) (\<eta> b)) (\<lambda>b. contains b a) \<Longrightarrow> \<forall>S. contains (\<eta> \<^bold>\<And>S) \<^bold>\<Or>Ra[\<eta>|S]
[PROOF STEP]
by (smt Ra_restr_ex inf_char)


[STATEMENT]
lemma CoP2_iDM3: "CoP2 \<eta> \<Longrightarrow> iDM3 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CoP2 \<eta> \<Longrightarrow> iDM3 \<eta>
[PROOF STEP]
by (smt CoP2_def Ra_restr_ex iDM3_def inf_char)


[STATEMENT]
lemma CoP1_iDM4: "CoP1 \<eta> \<Longrightarrow> iDM4 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CoP1 \<eta> \<Longrightarrow> iDM4 \<eta>
[PROOF STEP]
by (smt CoP1_def Ra_restr_all iDM4_def sup_char)


[STATEMENT]
lemma "XCoP \<eta> \<Longrightarrow> iDM3 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. XCoP \<eta> \<Longrightarrow> iDM3 \<eta>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. XCoP \<eta> \<Longrightarrow> iDM3 \<eta>
[PROOF STEP]
oops


[STATEMENT]
lemma "XCoP \<eta> \<Longrightarrow> iDM4 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. XCoP \<eta> \<Longrightarrow> iDM4 \<eta>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. XCoP \<eta> \<Longrightarrow> iDM4 \<eta>
[PROOF STEP]
oops


[STATEMENT]
lemma iDM1_rel: "iDM1 \<eta> \<Longrightarrow> DM1 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
assume idm1: "iDM1 \<eta>"
[PROOF STATE]
proof (state)
this:
iDM1 \<eta>

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
iDM1 \<eta>

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
fix a::"\<sigma>" and b::"\<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
let ?S="\<lambda>Z. Z=a \<or> Z=b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
have "\<^bold>\<And>Ra[\<eta>|?S] = \<^bold>\<forall>\<^sup>R\<lparr>?S\<rparr> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
[PROOF STEP]
using Ra_restr_all
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>Ra[?\<pi>|?D] = (\<lambda>w. contains (\<lambda>X. ?\<pi> X w) ?D)

goal (1 subgoal):
 1. \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
have "\<^bold>\<forall>\<^sup>R\<lparr>?S\<rparr> \<eta> = (\<eta> a) \<^bold>\<and> (\<eta> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
using meet_def
[PROOF STATE]
proof (prove)
using this:
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w

goal (1 subgoal):
 1. (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
(\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
have "\<^bold>\<And>Ra[\<eta>|?S] = (\<eta> a) \<^bold>\<and> (\<eta> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b))
(\<lambda>w. contains (\<lambda>X. \<eta> X w) (\<lambda>X. X = a \<or> X = b)) = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
have "\<^bold>\<Or>?S = a \<^bold>\<or> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
[PROOF STEP]
using supremum_def join_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>?S \<equiv> \<lambda>w. nonEmpty (\<lambda>X. ?S X \<and> X w)
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w

goal (1 subgoal):
 1. \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
from idm1
[PROOF STATE]
proof (chain)
picking this:
iDM1 \<eta>
[PROOF STEP]
have "\<eta>(\<^bold>\<Or>?S) \<^bold>\<preceq> \<^bold>\<And>Ra[\<eta>|?S]"
[PROOF STATE]
proof (prove)
using this:
iDM1 \<eta>

goal (1 subgoal):
 1. contains \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b)
[PROOF STEP]
by (simp add: iDM1_def)
[PROOF STATE]
proof (state)
this:
contains \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b)

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
contains \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b)
[PROOF STEP]
have "\<eta>(a \<^bold>\<or> b) \<^bold>\<preceq> (\<eta> a) \<^bold>\<and> (\<eta> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<and> \<eta> b
\<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<or> b
contains \<^bold>\<And>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] (\<eta> \<^bold>\<Or>\<lambda>Z. Z = a \<or> Z = b)

goal (1 subgoal):
 1. contains (\<eta> a \<^bold>\<and> \<eta> b) (\<eta> (a \<^bold>\<or> b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<eta> a \<^bold>\<and> \<eta> b) (\<eta> (a \<^bold>\<or> b))

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<eta> ?a2 \<^bold>\<and> \<eta> ?b2) (\<eta> (?a2 \<^bold>\<or> ?b2))

goal (1 subgoal):
 1. iDM1 \<eta> \<Longrightarrow> DM1 \<eta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
contains (\<eta> ?a2 \<^bold>\<and> \<eta> ?b2) (\<eta> (?a2 \<^bold>\<or> ?b2))

goal (1 subgoal):
 1. DM1 \<eta>
[PROOF STEP]
by (simp add: DM1_def)
[PROOF STATE]
proof (state)
this:
DM1 \<eta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iDM2_rel: "iDM2 \<eta> \<Longrightarrow> DM2 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
assume idm2: "iDM2 \<eta>"
[PROOF STATE]
proof (state)
this:
iDM2 \<eta>

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
iDM2 \<eta>

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
fix a::"\<sigma>" and b::"\<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
let ?S="\<lambda>Z. Z=a \<or> Z=b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
have "\<^bold>\<Or>Ra[\<eta>|?S] = \<^bold>\<exists>\<^sup>R\<lparr>?S\<rparr> \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
[PROOF STEP]
using Ra_restr_ex
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>Ra[?\<pi>|?D] = (\<lambda>w. nonEmpty (\<lambda>X. ?D X \<and> ?\<pi> X w))

goal (1 subgoal):
 1. \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
have "\<^bold>\<exists>\<^sup>R\<lparr>?S\<rparr> \<eta> = (\<eta> a) \<^bold>\<or> (\<eta> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
using join_def
[PROOF STATE]
proof (prove)
using this:
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w

goal (1 subgoal):
 1. (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
(\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
have "\<^bold>\<Or>Ra[\<eta>|?S] = (\<eta> a) \<^bold>\<or> (\<eta> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = (\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w))
(\<lambda>w. nonEmpty (\<lambda>X. (X = a \<or> X = b) \<and> \<eta> X w)) = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
have "\<^bold>\<And>?S = a \<^bold>\<and> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
[PROOF STEP]
using infimum_def meet_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<And>?S \<equiv> \<lambda>w. contains (\<lambda>X. X w) ?S
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w

goal (1 subgoal):
 1. \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
from idm2
[PROOF STATE]
proof (chain)
picking this:
iDM2 \<eta>
[PROOF STEP]
have "\<^bold>\<Or>Ra[\<eta>|?S] \<^bold>\<preceq> \<eta>(\<^bold>\<And>?S)"
[PROOF STATE]
proof (prove)
using this:
iDM2 \<eta>

goal (1 subgoal):
 1. contains (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]
[PROOF STEP]
by (simp add: iDM2_def)
[PROOF STATE]
proof (state)
this:
contains (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
contains (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]
[PROOF STEP]
have "(\<eta> a) \<^bold>\<or> (\<eta> b) \<^bold>\<preceq> \<eta>(a \<^bold>\<and> b)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b] = \<eta> a \<^bold>\<or> \<eta> b
\<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b = a \<^bold>\<and> b
contains (\<eta> \<^bold>\<And>\<lambda>Z. Z = a \<or> Z = b) \<^bold>\<Or>Ra[\<eta>|\<lambda>Z. Z = a \<or> Z = b]

goal (1 subgoal):
 1. contains (\<eta> (a \<^bold>\<and> b)) (\<eta> a \<^bold>\<or> \<eta> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
contains (\<eta> (a \<^bold>\<and> b)) (\<eta> a \<^bold>\<or> \<eta> b)

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<eta> (?a2 \<^bold>\<and> ?b2)) (\<eta> ?a2 \<^bold>\<or> \<eta> ?b2)

goal (1 subgoal):
 1. iDM2 \<eta> \<Longrightarrow> DM2 \<eta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
contains (\<eta> (?a2 \<^bold>\<and> ?b2)) (\<eta> ?a2 \<^bold>\<or> \<eta> ?b2)

goal (1 subgoal):
 1. DM2 \<eta>
[PROOF STEP]
by (simp add: DM2_def)
[PROOF STATE]
proof (state)
this:
DM2 \<eta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "DM1 \<eta> = iDM1 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DM1 \<eta> = iDM1 \<eta>
[PROOF STEP]
using CoPw_iDM1 DM1_CoPw iDM1_rel
[PROOF STATE]
proof (prove)
using this:
CoPw ?\<eta> \<Longrightarrow> iDM1 ?\<eta>
DM1 ?\<eta> = CoPw ?\<eta>
iDM1 ?\<eta> \<Longrightarrow> DM1 ?\<eta>

goal (1 subgoal):
 1. DM1 \<eta> = iDM1 \<eta>
[PROOF STEP]
by blast


[STATEMENT]
lemma "DM2 \<eta> = iDM2 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DM2 \<eta> = iDM2 \<eta>
[PROOF STEP]
using CoPw_iDM2 DM2_CoPw iDM2_rel
[PROOF STATE]
proof (prove)
using this:
CoPw ?\<eta> \<Longrightarrow> iDM2 ?\<eta>
DM2 ?\<eta> = CoPw ?\<eta>
iDM2 ?\<eta> \<Longrightarrow> DM2 ?\<eta>

goal (1 subgoal):
 1. DM2 \<eta> = iDM2 \<eta>
[PROOF STEP]
by blast


[STATEMENT]
lemma "iDM1 \<eta> = iDM2 \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iDM1 \<eta> = iDM2 \<eta>
[PROOF STEP]
using CoPw_iDM1 CoPw_iDM2 DM1_CoPw DM2_CoPw iDM1_rel iDM2_rel
[PROOF STATE]
proof (prove)
using this:
CoPw ?\<eta> \<Longrightarrow> iDM1 ?\<eta>
CoPw ?\<eta> \<Longrightarrow> iDM2 ?\<eta>
DM1 ?\<eta> = CoPw ?\<eta>
DM2 ?\<eta> = CoPw ?\<eta>
iDM1 ?\<eta> \<Longrightarrow> DM1 ?\<eta>
iDM2 ?\<eta> \<Longrightarrow> DM2 ?\<eta>

goal (1 subgoal):
 1. iDM1 \<eta> = iDM2 \<eta>
[PROOF STEP]
by blast