[STATEMENT]
lemma closed_segment_degen_complex:
  "\<lbrakk>Re lb = Re ub; Im lb \<le> Im ub \<rbrakk>
    \<Longrightarrow> x \<in> closed_segment lb ub \<longleftrightarrow> Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub "
  "\<lbrakk>Im lb = Im ub; Re lb \<le> Re ub \<rbrakk>
    \<Longrightarrow> x \<in> closed_segment lb ub \<longleftrightarrow> Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> (x \<in> closed_segment lb ub) = (Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub)) &&& (\<lbrakk>Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> (x \<in> closed_segment lb ub) = (Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> (x \<in> closed_segment lb ub) = (Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub)
 2. \<lbrakk>Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> (x \<in> closed_segment lb ub) = (Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub)
[PROOF STEP]
show "x \<in> closed_segment lb ub \<longleftrightarrow> Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub"
    when "Re lb = Re ub" "Im lb \<le> Im ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> closed_segment lb ub) = (Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
show "Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub" when "x \<in> closed_segment lb ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
using closed_segment_imp_Re_Im[OF that] \<open>Re lb = Re ub\<close> \<open>Im lb \<le> Im ub\<close>
[PROOF STATE]
proof (prove)
using this:
Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
Re lb = Re ub
Im lb \<le> Im ub

goal (1 subgoal):
 1. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment lb ub \<Longrightarrow> Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
assume asm:"Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub"
[PROOF STATE]
proof (state)
this:
Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
define u where "u=(Im x - Im lb)/ (Im ub - Im lb)"
[PROOF STATE]
proof (state)
this:
u = (Im x - Im lb) / (Im ub - Im lb)

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
have "x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (1 - (Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R lb + ((Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R ub
[PROOF STEP]
using asm \<open>Re lb = Re ub\<close> \<open>Im lb \<le> Im ub\<close>
[PROOF STATE]
proof (prove)
using this:
Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub
Re lb = Re ub
Im lb \<le> Im ub

goal (1 subgoal):
 1. x = (1 - (Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R lb + ((Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R ub
[PROOF STEP]
apply (intro complex_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub; Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> Re x = Re ((1 - (Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R lb + ((Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R ub)
 2. \<lbrakk>Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub; Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> Im x = Im ((1 - (Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R lb + ((Im x - Im lb) / (Im ub - Im lb)) *\<^sub>R ub)
[PROOF STEP]
apply (auto simp add:field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Re lb = Re ub; Re x = Re ub; Im lb \<le> Im x; Im x \<le> Im ub\<rbrakk> \<Longrightarrow> Im x + (Im lb * Im x - Im lb * Im lb) / (Im ub - Im lb) = Im lb + (Im ub * Im x - Im lb * Im ub) / (Im ub - Im lb)
[PROOF STEP]
apply (cases "Im ub - Im lb =0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Re lb = Re ub; Re x = Re ub; Im lb \<le> Im x; Im x \<le> Im ub; Im ub - Im lb = 0\<rbrakk> \<Longrightarrow> Im x + (Im lb * Im x - Im lb * Im lb) / (Im ub - Im lb) = Im lb + (Im ub * Im x - Im lb * Im ub) / (Im ub - Im lb)
 2. \<lbrakk>Re lb = Re ub; Re x = Re ub; Im lb \<le> Im x; Im x \<le> Im ub; Im ub - Im lb \<noteq> 0\<rbrakk> \<Longrightarrow> Im x + (Im lb * Im x - Im lb * Im lb) / (Im ub - Im lb) = Im lb + (Im ub * Im x - Im lb * Im ub) / (Im ub - Im lb)
[PROOF STEP]
apply (auto simp add:field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
have "0\<le>u" "u\<le>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> u &&& u \<le> 1
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (Im x - Im lb) / (Im ub - Im lb) &&& (Im x - Im lb) / (Im ub - Im lb) \<le> 1
[PROOF STEP]
using \<open>Im lb \<le> Im ub\<close> asm
[PROOF STATE]
proof (prove)
using this:
Im lb \<le> Im ub
Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub

goal (1 subgoal):
 1. 0 \<le> (Im x - Im lb) / (Im ub - Im lb) &&& (Im x - Im lb) / (Im ub - Im lb) \<le> 1
[PROOF STEP]
by (cases "Im ub - Im lb =0",auto simp add:field_simps)+
[PROOF STATE]
proof (state)
this:
0 \<le> u
u \<le> 1

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
0 \<le> u
u \<le> 1
[PROOF STEP]
show "x \<in> closed_segment lb ub"
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. x \<in> closed_segment lb ub
[PROOF STEP]
unfolding closed_segment_def
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. x \<in> {(1 - u) *\<^sub>R lb + u *\<^sub>R ub |u. 0 \<le> u \<and> u \<le> 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment lb ub

goal (1 subgoal):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> (x \<in> closed_segment lb ub) = (Re x = Re lb \<and> Im lb \<le> Im x \<and> Im x \<le> Im ub)

goal (3 subgoals):
 1. \<lbrakk>Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> Re lb = Re ub
 2. \<lbrakk>Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> Im lb \<le> Im ub
 3. \<lbrakk>Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> (x \<in> closed_segment lb ub) = (Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub)
[PROOF STEP]
show "x \<in> closed_segment lb ub \<longleftrightarrow> Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub"
    when "Im lb = Im ub" "Re lb \<le> Re ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> closed_segment lb ub) = (Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
show "Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub" when "x \<in> closed_segment lb ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub
[PROOF STEP]
using closed_segment_imp_Re_Im[OF that] \<open>Im lb = Im ub\<close> \<open>Re lb \<le> Re ub\<close>
[PROOF STATE]
proof (prove)
using this:
Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
Im lb = Im ub
Re lb \<le> Re ub

goal (1 subgoal):
 1. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment lb ub \<Longrightarrow> Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
assume asm:"Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub"
[PROOF STATE]
proof (state)
this:
Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
define u where "u=(Re x - Re lb)/ (Re ub - Re lb)"
[PROOF STATE]
proof (state)
this:
u = (Re x - Re lb) / (Re ub - Re lb)

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
have "x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (1 - (Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R lb + ((Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R ub
[PROOF STEP]
using asm \<open>Im lb = Im ub\<close> \<open>Re lb \<le> Re ub\<close>
[PROOF STATE]
proof (prove)
using this:
Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub
Im lb = Im ub
Re lb \<le> Re ub

goal (1 subgoal):
 1. x = (1 - (Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R lb + ((Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R ub
[PROOF STEP]
apply (intro complex_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub; Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> Re x = Re ((1 - (Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R lb + ((Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R ub)
 2. \<lbrakk>Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub; Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> Im x = Im ((1 - (Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R lb + ((Re x - Re lb) / (Re ub - Re lb)) *\<^sub>R ub)
[PROOF STEP]
apply (auto simp add:field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Im lb = Im ub; Im x = Im ub; Re lb \<le> Re x; Re x \<le> Re ub\<rbrakk> \<Longrightarrow> Re x + (Re lb * Re x - Re lb * Re lb) / (Re ub - Re lb) = Re lb + (Re ub * Re x - Re lb * Re ub) / (Re ub - Re lb)
[PROOF STEP]
apply (cases "Re ub - Re lb =0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Im lb = Im ub; Im x = Im ub; Re lb \<le> Re x; Re x \<le> Re ub; Re ub - Re lb = 0\<rbrakk> \<Longrightarrow> Re x + (Re lb * Re x - Re lb * Re lb) / (Re ub - Re lb) = Re lb + (Re ub * Re x - Re lb * Re ub) / (Re ub - Re lb)
 2. \<lbrakk>Im lb = Im ub; Im x = Im ub; Re lb \<le> Re x; Re x \<le> Re ub; Re ub - Re lb \<noteq> 0\<rbrakk> \<Longrightarrow> Re x + (Re lb * Re x - Re lb * Re lb) / (Re ub - Re lb) = Re lb + (Re ub * Re x - Re lb * Re ub) / (Re ub - Re lb)
[PROOF STEP]
apply (auto simp add:field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
have "0\<le>u" "u\<le>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> u &&& u \<le> 1
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (Re x - Re lb) / (Re ub - Re lb) &&& (Re x - Re lb) / (Re ub - Re lb) \<le> 1
[PROOF STEP]
using \<open>Re lb \<le> Re ub\<close> asm
[PROOF STATE]
proof (prove)
using this:
Re lb \<le> Re ub
Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub

goal (1 subgoal):
 1. 0 \<le> (Re x - Re lb) / (Re ub - Re lb) &&& (Re x - Re lb) / (Re ub - Re lb) \<le> 1
[PROOF STEP]
by (cases "Re ub - Re lb =0",auto simp add:field_simps)+
[PROOF STATE]
proof (state)
this:
0 \<le> u
u \<le> 1

goal (2 subgoals):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
 2. Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
0 \<le> u
u \<le> 1
[PROOF STEP]
show "x \<in> closed_segment lb ub"
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. x \<in> closed_segment lb ub
[PROOF STEP]
unfolding closed_segment_def
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. x \<in> {(1 - u) *\<^sub>R lb + u *\<^sub>R ub |u. 0 \<le> u \<and> u \<le> 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment lb ub

goal (1 subgoal):
 1. x \<in> closed_segment lb ub \<Longrightarrow> x \<in> closed_segment lb ub
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> (x \<in> closed_segment lb ub) = (Im x = Im lb \<and> Re lb \<le> Re x \<and> Re x \<le> Re ub)

goal (4 subgoals):
 1. \<lbrakk>Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> Re lb = Re ub
 2. \<lbrakk>Re lb = Re ub; Im lb \<le> Im ub\<rbrakk> \<Longrightarrow> Im lb \<le> Im ub
 3. \<lbrakk>Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> Im lb = Im ub
 4. \<lbrakk>Im lb = Im ub; Re lb \<le> Re ub\<rbrakk> \<Longrightarrow> Re lb \<le> Re ub
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_ball:
  fixes a :: "'a::euclidean_space"
  assumes "r > 0"
  shows "infinite (ball a r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (ball a r)
[PROOF STEP]
using uncountable_ball[OF assms, THEN uncountable_infinite]
[PROOF STATE]
proof (prove)
using this:
infinite (ball ?a1 r)

goal (1 subgoal):
 1. infinite (ball a r)
[PROOF STEP]
.


[STATEMENT]
lemma infinite_cball:
  fixes a :: "'a::euclidean_space"
  assumes "r > 0"
  shows "infinite (cball a r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (cball a r)
[PROOF STEP]
using uncountable_cball[OF assms, THEN uncountable_infinite,of a]
[PROOF STATE]
proof (prove)
using this:
infinite (cball a r)

goal (1 subgoal):
 1. infinite (cball a r)
[PROOF STEP]
.


[STATEMENT]
lemma infinite_sphere:
  fixes a :: complex
  assumes "r > 0"
  shows "infinite (sphere a r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (sphere a r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (sphere a r)
[PROOF STEP]
have "uncountable (path_image (circlepath a r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uncountable (path_image (circlepath a r))
[PROOF STEP]
apply (rule simple_path_image_uncountable)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_path (circlepath a r)
[PROOF STEP]
using simple_path_circlepath assms
[PROOF STATE]
proof (prove)
using this:
simple_path (circlepath ?z ?r) = (?r \<noteq> 0)
0 < r

goal (1 subgoal):
 1. simple_path (circlepath a r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
uncountable (path_image (circlepath a r))

goal (1 subgoal):
 1. infinite (sphere a r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uncountable (path_image (circlepath a r))
[PROOF STEP]
have "uncountable (sphere a r)"
[PROOF STATE]
proof (prove)
using this:
uncountable (path_image (circlepath a r))

goal (1 subgoal):
 1. uncountable (sphere a r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
uncountable (path_image (circlepath a r))
0 < r

goal (1 subgoal):
 1. uncountable (sphere a r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
uncountable (sphere a r)

goal (1 subgoal):
 1. infinite (sphere a r)
[PROOF STEP]
from uncountable_infinite[OF this]
[PROOF STATE]
proof (chain)
picking this:
infinite (sphere a r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite (sphere a r)

goal (1 subgoal):
 1. infinite (sphere a r)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
infinite (sphere a r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_halfspace_Im_gt: "infinite {x. Im x > b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {x. b < Im x}
[PROOF STEP]
apply (rule connected_uncountable[THEN uncountable_infinite,of _ "(b+1)* \<i>" "(b+2)*\<i>"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. connected {x. b < Im x}
 2. complex_of_real (b + 1) * \<i> \<in> {x. b < Im x}
 3. complex_of_real (b + 2) * \<i> \<in> {x. b < Im x}
 4. complex_of_real (b + 1) * \<i> \<noteq> complex_of_real (b + 2) * \<i>
[PROOF STEP]
by (auto intro!:convex_connected simp add: convex_halfspace_Im_gt)


[STATEMENT]
lemma (in ring_1) Ints_minus2: "- a \<in> \<int> \<Longrightarrow> a \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - a \<in> \<int> \<Longrightarrow> a \<in> \<int>
[PROOF STEP]
using Ints_minus[of "-a"]
[PROOF STATE]
proof (prove)
using this:
- a \<in> \<int> \<Longrightarrow> - (- a) \<in> \<int>

goal (1 subgoal):
 1. - a \<in> \<int> \<Longrightarrow> a \<in> \<int>
[PROOF STEP]
by auto


[STATEMENT]
lemma dvd_divide_Ints_iff:
  "b dvd a \<or> b=0 \<longleftrightarrow> of_int a / of_int b \<in> (\<int> :: 'a :: {field,ring_char_0} set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b dvd a \<or> b = 0) = (of_int a / of_int b \<in> \<int>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b dvd a \<or> b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
 2. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
assume asm:"b dvd a \<or> b=0"
[PROOF STATE]
proof (state)
this:
b dvd a \<or> b = 0

goal (2 subgoals):
 1. b dvd a \<or> b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
 2. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
let ?thesis = "of_int a / of_int b \<in> (\<int> :: 'a :: {field,ring_char_0} set)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b dvd a \<or> b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
 2. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
have ?thesis when "b dvd a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
obtain c where "a=b * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. a = b * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>b dvd a\<close>
[PROOF STATE]
proof (prove)
using this:
b dvd a

goal (1 subgoal):
 1. (\<And>c. a = b * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. a = b * k

goal (1 subgoal):
 1. (\<And>c. a = b * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = b * c

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = b * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b * c

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
of_int a / of_int b \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b dvd a \<Longrightarrow> of_int a / of_int b \<in> \<int>

goal (2 subgoals):
 1. b dvd a \<or> b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
 2. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b dvd a \<Longrightarrow> of_int a / of_int b \<in> \<int>

goal (2 subgoals):
 1. b dvd a \<or> b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
 2. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
have ?thesis when "b=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
b = 0

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>

goal (2 subgoals):
 1. b dvd a \<or> b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
 2. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b dvd a \<Longrightarrow> of_int a / of_int b \<in> \<int>
b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b dvd a \<Longrightarrow> of_int a / of_int b \<in> \<int>
b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
b dvd a \<Longrightarrow> of_int a / of_int b \<in> \<int>
b = 0 \<Longrightarrow> of_int a / of_int b \<in> \<int>
b dvd a \<or> b = 0

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int a / of_int b \<in> \<int>

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
assume "of_int a / of_int b \<in> (\<int> :: 'a :: {field,ring_char_0} set)"
[PROOF STATE]
proof (state)
this:
of_int a / of_int b \<in> \<int>

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
from Ints_cases[OF this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>z. of_int a / of_int b = of_int z \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain c where *:"(of_int::_ \<Rightarrow> 'a) c= of_int a / of_int b"
[PROOF STATE]
proof (prove)
using this:
(\<And>z. of_int a / of_int b = of_int z \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c. of_int c = of_int a / of_int b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
of_int c = of_int a / of_int b

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
have "b dvd a" when "b\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b dvd a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b dvd a
[PROOF STEP]
have "(of_int::_ \<Rightarrow> 'a) a = of_int b * of_int c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int a = of_int b * of_int c
[PROOF STEP]
using that *
[PROOF STATE]
proof (prove)
using this:
b \<noteq> 0
of_int c = of_int a / of_int b

goal (1 subgoal):
 1. of_int a = of_int b * of_int c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int a = of_int b * of_int c

goal (1 subgoal):
 1. b dvd a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
of_int a = of_int b * of_int c
[PROOF STEP]
have "a = b * c"
[PROOF STATE]
proof (prove)
using this:
of_int a = of_int b * of_int c

goal (1 subgoal):
 1. a = b * c
[PROOF STEP]
using of_int_eq_iff
[PROOF STATE]
proof (prove)
using this:
of_int a = of_int b * of_int c
(of_int ?w = of_int ?z) = (?w = ?z)

goal (1 subgoal):
 1. a = b * c
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a = b * c

goal (1 subgoal):
 1. b dvd a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = b * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b * c

goal (1 subgoal):
 1. b dvd a
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
a = b * c

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

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

goal (1 subgoal):
 1. of_int a / of_int b \<in> \<int> \<Longrightarrow> b dvd a \<or> b = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> 0 \<Longrightarrow> b dvd a
[PROOF STEP]
show " b dvd a \<or> b = 0"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> 0 \<Longrightarrow> b dvd a

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_int_div_field:
  assumes "d dvd n"
  shows "(of_int::_\<Rightarrow>'a::field_char_0) (n div d) = of_int n / of_int d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (n div d) = of_int n / of_int d
[PROOF STEP]
apply (subst (2) dvd_mult_div_cancel[OF assms,symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (n div d) = of_int (d * (n div d)) / of_int d
[PROOF STEP]
by (auto simp add:field_simps)


[STATEMENT]
lemma powr_eq_1_iff:
  assumes "a>0"
  shows "(a::real) powr b =1 \<longleftrightarrow> a=1 \<or> b=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a powr b = 1) = (a = 1 \<or> b = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a powr b = 1 \<Longrightarrow> a = 1 \<or> b = 0
 2. a = 1 \<or> b = 0 \<Longrightarrow> a powr b = 1
[PROOF STEP]
assume "a powr b = 1"
[PROOF STATE]
proof (state)
this:
a powr b = 1

goal (2 subgoals):
 1. a powr b = 1 \<Longrightarrow> a = 1 \<or> b = 0
 2. a = 1 \<or> b = 0 \<Longrightarrow> a powr b = 1
[PROOF STEP]
have "b * ln a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * ln a = 0
[PROOF STEP]
using \<open>a powr b = 1\<close> ln_powr[of a b] assms
[PROOF STATE]
proof (prove)
using this:
a powr b = 1
a \<noteq> 0 \<Longrightarrow> ln (a powr b) = b * ln a
0 < a

goal (1 subgoal):
 1. b * ln a = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b * ln a = 0

goal (2 subgoals):
 1. a powr b = 1 \<Longrightarrow> a = 1 \<or> b = 0
 2. a = 1 \<or> b = 0 \<Longrightarrow> a powr b = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b * ln a = 0
[PROOF STEP]
have "b=0 \<or> ln a =0"
[PROOF STATE]
proof (prove)
using this:
b * ln a = 0

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

goal (2 subgoals):
 1. a powr b = 1 \<Longrightarrow> a = 1 \<or> b = 0
 2. a = 1 \<or> b = 0 \<Longrightarrow> a powr b = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = 0 \<or> ln a = 0
[PROOF STEP]
show "a = 1 \<or> b = 0"
[PROOF STATE]
proof (prove)
using this:
b = 0 \<or> ln a = 0

goal (1 subgoal):
 1. a = 1 \<or> b = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b = 0 \<or> ln a = 0
0 < a

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

goal (1 subgoal):
 1. a = 1 \<or> b = 0 \<Longrightarrow> a powr b = 1
[PROOF STEP]
qed (insert assms, auto)


[STATEMENT]
lemma tan_inj_pi:
  "- (pi/2) < x \<Longrightarrow> x < pi/2 \<Longrightarrow> - (pi/2) < y \<Longrightarrow> y < pi/2 \<Longrightarrow> tan x = tan y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- (pi / 2) < x; x < pi / 2; - (pi / 2) < y; y < pi / 2; tan x = tan y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (metis arctan_tan)


[STATEMENT]
lemma finite_ReZ_segments_poly_circlepath:
          "finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
proof (cases "\<forall>t\<in>({0..1} - {1/2}). Re ((poly p \<circ> circlepath z0 r) t) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
 2. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0

goal (2 subgoals):
 1. \<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
 2. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
have "isCont (Re \<circ> poly p \<circ> circlepath z0 r) (1/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont (Re \<circ> poly p \<circ> circlepath z0 r) (1 / 2)
[PROOF STEP]
by (auto intro!:continuous_intros simp:circlepath)
[PROOF STATE]
proof (state)
this:
isCont (Re \<circ> poly p \<circ> circlepath z0 r) (1 / 2)

goal (2 subgoals):
 1. \<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
 2. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isCont (Re \<circ> poly p \<circ> circlepath z0 r) (1 / 2)

goal (2 subgoals):
 1. \<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
 2. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
have "(Re \<circ> poly p \<circ> circlepath z0 r)\<midarrow> 1/2 \<rightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0
[PROOF STEP]
have "\<forall>\<^sub>F x in at (1 / 2). (Re \<circ> poly p \<circ> circlepath z0 r) x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at (1 / 2). (Re \<circ> poly p \<circ> circlepath z0 r) x = 0
[PROOF STEP]
unfolding eventually_at_le
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>d>0. \<forall>x\<in>UNIV. x \<noteq> 1 / 2 \<and> dist x (1 / 2) \<le> d \<longrightarrow> (Re \<circ> poly p \<circ> circlepath z0 r) x = 0
[PROOF STEP]
apply (rule exI[where x="1/2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 / 2 \<and> (\<forall>x\<in>UNIV. x \<noteq> 1 / 2 \<and> dist x (1 / 2) \<le> 1 / 2 \<longrightarrow> (Re \<circ> poly p \<circ> circlepath z0 r) x = 0)
[PROOF STEP]
unfolding dist_real_def abs_diff_le_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 / 2 \<and> (\<forall>x\<in>UNIV. x \<noteq> 1 / 2 \<and> 1 / 2 - 1 / 2 \<le> x \<and> x \<le> 1 / 2 + 1 / 2 \<longrightarrow> (Re \<circ> poly p \<circ> circlepath z0 r) x = 0)
[PROOF STEP]
by (auto intro!:True[rule_format, unfolded comp_def])
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at (1 / 2). (Re \<circ> poly p \<circ> circlepath z0 r) x = 0

goal (1 subgoal):
 1. (Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at (1 / 2). (Re \<circ> poly p \<circ> circlepath z0 r) x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at (1 / 2). (Re \<circ> poly p \<circ> circlepath z0 r) x = 0

goal (1 subgoal):
 1. (Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0
[PROOF STEP]
by (rule tendsto_eventually)
[PROOF STATE]
proof (state)
this:
(Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0

goal (2 subgoals):
 1. \<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
 2. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isCont (Re \<circ> poly p \<circ> circlepath z0 r) (1 / 2)
(Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0
[PROOF STEP]
have "Re ((poly p \<circ> circlepath z0 r) (1/2)) = 0"
[PROOF STATE]
proof (prove)
using this:
isCont (Re \<circ> poly p \<circ> circlepath z0 r) (1 / 2)
(Re \<circ> poly p \<circ> circlepath z0 r) \<midarrow>1 / 2\<rightarrow> 0

goal (1 subgoal):
 1. Re ((poly p \<circ> circlepath z0 r) (1 / 2)) = 0
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
using this:
isCont (\<lambda>x. Re (poly p (circlepath z0 r x))) (1 / 2)
(\<lambda>x. Re (poly p (circlepath z0 r x))) \<midarrow>1 / 2\<rightarrow> 0

goal (1 subgoal):
 1. Re (poly p (circlepath z0 r (1 / 2))) = 0
[PROOF STEP]
by (simp add: LIM_unique continuous_within)
[PROOF STATE]
proof (state)
this:
Re ((poly p \<circ> circlepath z0 r) (1 / 2)) = 0

goal (2 subgoals):
 1. \<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
 2. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Re ((poly p \<circ> circlepath z0 r) (1 / 2)) = 0
[PROOF STEP]
have "\<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0"
[PROOF STATE]
proof (prove)
using this:
Re ((poly p \<circ> circlepath z0 r) (1 / 2)) = 0

goal (1 subgoal):
 1. \<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
Re ((poly p \<circ> circlepath z0 r) (1 / 2)) = 0
\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0

goal (1 subgoal):
 1. \<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0

goal (2 subgoals):
 1. \<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
 2. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0

goal (1 subgoal):
 1. finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
apply (rule_tac finite_ReZ_segments_constI[THEN finite_ReZ_segments_congE])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<Longrightarrow> \<forall>t. 0 < t \<and> t < 1 \<longrightarrow> ?p1.1 t = ?c2
 2. \<And>t. \<lbrakk>\<forall>t\<in>{0..1}. Re ((poly p \<circ> circlepath z0 r) t) = 0; 0 < t; t < 1\<rbrakk> \<Longrightarrow> Re (?p1.1 t - ?z1.1) = Re ((poly p \<circ> circlepath z0 r) t - 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0)

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
define q1 q2 where "q1=fcompose p [:(z0+r)*\<i>,z0-r:] [:\<i>,1:]" and
                      "q2=([:\<i>, 1:] ^ degree p)"
[PROOF STATE]
proof (state)
this:
q1 = fcompose p [:(z0 + complex_of_real r) * \<i>, z0 - complex_of_real r:] [:\<i>, 1:]
q2 = [:\<i>, 1:] ^ degree p

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
define q1R q1I where "q1R=map_poly Re q1" and "q1I=map_poly Im q1"
[PROOF STATE]
proof (state)
this:
q1R = map_poly Re q1
q1I = map_poly Im q1

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
define q2R q2I where "q2R=map_poly Re q2" and "q2I=map_poly Im q2"
[PROOF STATE]
proof (state)
this:
q2R = map_poly Re q2
q2I = map_poly Im q2

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
define qq where "qq=q1R*q2R + q1I*q2I"
[PROOF STATE]
proof (state)
this:
qq = q1R * q2R + q1I * q2I

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
have poly_eq:"Re ((poly p \<circ> circlepath z0 r) t) = 0 \<longleftrightarrow> poly qq (tan (pi * t)) = 0"
    when "0\<le>t" "t\<le>1" "t\<noteq>1/2" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
define tt where "tt=tan (pi * t)"
[PROOF STATE]
proof (state)
this:
tt = tan (pi * t)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
have "Re ((poly p \<circ> circlepath z0 r) t) = 0 \<longleftrightarrow> Re (poly q1 tt / poly q2 tt) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0)
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re (poly p (circlepath z0 r t)) = 0) = (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0)
[PROOF STEP]
apply (subst poly_circlepath_tan_eq[of t p z0 r,folded q1_def q2_def tt_def])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. 0 \<le> t
 2. t \<le> 1
 3. t \<noteq> 1 / 2
 4. (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0) = (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> 1
t \<noteq> 1 / 2

goal (4 subgoals):
 1. 0 \<le> t
 2. t \<le> 1
 3. t \<noteq> 1 / 2
 4. (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0) = (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(Re ((poly p \<circ> circlepath z0 r) t) = 0) = (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Re ((poly p \<circ> circlepath z0 r) t) = 0) = (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
have "... \<longleftrightarrow> poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0) = (poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0)
[PROOF STEP]
unfolding q1I_def q1R_def q2R_def q2I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0) = (poly (map_poly Re q1) tt * poly (map_poly Re q2) tt + poly (map_poly Im q1) tt * poly (map_poly Im q2) tt = 0)
[PROOF STEP]
by (simp add:Re_complex_div_eq_0 Re_poly_of_real Im_poly_of_real)
[PROOF STATE]
proof (state)
this:
(Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0) = (poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Re (poly q1 (complex_of_real tt) / poly q2 (complex_of_real tt)) = 0) = (poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
have "... \<longleftrightarrow> poly qq tt = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0) = (poly qq tt = 0)
[PROOF STEP]
unfolding qq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0) = (poly (q1R * q2R + q1I * q2I) tt = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(poly q1R tt * poly q2R tt + poly q1I tt * poly q2I tt = 0) = (poly qq tt = 0)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq tt = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq tt = 0)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
unfolding tt_def
[PROOF STATE]
proof (prove)
using this:
(Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)

goal (1 subgoal):
 1. (Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(Re ((poly p \<circ> circlepath z0 r) t) = 0) = (poly qq (tan (pi * t)) = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?t; ?t \<le> 1; ?t \<noteq> 1 / 2\<rbrakk> \<Longrightarrow> (Re ((poly p \<circ> circlepath z0 r) ?t) = 0) = (poly qq (tan (pi * ?t)) = 0)

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
have "finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
define P where "P=(\<lambda>t. Re ((poly p \<circ> circlepath z0 r) t) = 0)"
[PROOF STATE]
proof (state)
this:
P = (\<lambda>t. Re ((poly p \<circ> circlepath z0 r) t) = 0)

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
define A where "A= ({0..1}::real set)"
[PROOF STATE]
proof (state)
this:
A = {0..1}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
define S where "S={t\<in>A-{1,1/2}. P t}"
[PROOF STATE]
proof (state)
this:
S = {t \<in> A - {1, 1 / 2}. P t}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
have "finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t\<noteq>1/2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
[PROOF STEP]
define A where "A={t::real. 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}"
[PROOF STATE]
proof (state)
this:
A = {t. 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}

goal (1 subgoal):
 1. finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
[PROOF STEP]
have "finite ((\<lambda>t. tan (pi * t))  -`  {x. poly qq x=0} \<inter> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>t. tan (pi * t)) -` {x. poly qq x = 0} \<inter> A)
[PROOF STEP]
proof (rule finite_vimage_IntI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {x. poly qq x = 0}
 2. inj_on (\<lambda>t. tan (pi * t)) A
[PROOF STEP]
have "x = y" when "tan (pi * x) = tan (pi * y)" "x\<in>A" "y\<in>A" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
define x' where "x'=(if x<1/2 then x else x-1)"
[PROOF STATE]
proof (state)
this:
x' = (if x < 1 / 2 then x else x - 1)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
define y' where "y'=(if y<1/2 then y else y-1)"
[PROOF STATE]
proof (state)
this:
y' = (if y < 1 / 2 then y else y - 1)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "x'*pi = y'*pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' * pi = y' * pi
[PROOF STEP]
proof (rule tan_inj_pi)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. - (pi / 2) < x' * pi
 2. x' * pi < pi / 2
 3. - (pi / 2) < y' * pi
 4. y' * pi < pi / 2
 5. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
have *:"- 1 / 2 < x'" "x' < 1 / 2" "- 1 / 2 < y'" "y' < 1 / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- 1 / 2 < x' &&& x' < 1 / 2) &&& - 1 / 2 < y' &&& y' < 1 / 2
[PROOF STEP]
using that(2,3)
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A

goal (1 subgoal):
 1. (- 1 / 2 < x' &&& x' < 1 / 2) &&& - 1 / 2 < y' &&& y' < 1 / 2
[PROOF STEP]
unfolding x'_def y'_def A_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {t. 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
y \<in> {t. 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}

goal (1 subgoal):
 1. (- 1 / 2 < (if x < 1 / 2 then x else x - 1) &&& (if x < 1 / 2 then x else x - 1) < 1 / 2) &&& - 1 / 2 < (if y < 1 / 2 then y else y - 1) &&& (if y < 1 / 2 then y else y - 1) < 1 / 2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
- 1 / 2 < x'
x' < 1 / 2
- 1 / 2 < y'
y' < 1 / 2

goal (5 subgoals):
 1. - (pi / 2) < x' * pi
 2. x' * pi < pi / 2
 3. - (pi / 2) < y' * pi
 4. y' * pi < pi / 2
 5. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
show "- (pi / 2) < x'  * pi" "x'  * pi < pi / 2" "- (pi / 2) < y'  * pi"
                  "y'*pi < pi / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (pi / 2) < x' * pi &&& x' * pi < pi / 2) &&& - (pi / 2) < y' * pi &&& y' * pi < pi / 2
[PROOF STEP]
using mult_strict_right_mono[OF *(1),of pi]
                    mult_strict_right_mono[OF *(2),of pi]
                    mult_strict_right_mono[OF *(3),of pi]
                    mult_strict_right_mono[OF *(4),of pi]
[PROOF STATE]
proof (prove)
using this:
0 < pi \<Longrightarrow> - 1 / 2 * pi < x' * pi
0 < pi \<Longrightarrow> x' * pi < 1 / 2 * pi
0 < pi \<Longrightarrow> - 1 / 2 * pi < y' * pi
0 < pi \<Longrightarrow> y' * pi < 1 / 2 * pi

goal (1 subgoal):
 1. (- (pi / 2) < x' * pi &&& x' * pi < pi / 2) &&& - (pi / 2) < y' * pi &&& y' * pi < pi / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- (pi / 2) < x' * pi
x' * pi < pi / 2
- (pi / 2) < y' * pi
y' * pi < pi / 2

goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
have "tan (x' * pi) = tan (x * pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tan (x' * pi) = tan (x * pi)
[PROOF STEP]
unfolding x'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tan ((if x < 1 / 2 then x else x - 1) * pi) = tan (x * pi)
[PROOF STEP]
using tan_periodic_int[of _ "- 1",simplified]
[PROOF STATE]
proof (prove)
using this:
tan (?x - pi) = tan ?x

goal (1 subgoal):
 1. tan ((if x < 1 / 2 then x else x - 1) * pi) = tan (x * pi)
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
tan (x' * pi) = tan (x * pi)

goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
tan (x' * pi) = tan (x * pi)

goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
have "... = tan (y * pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tan (x * pi) = tan (y * pi)
[PROOF STEP]
using \<open>tan (pi * x) = tan (pi * y)\<close>
[PROOF STATE]
proof (prove)
using this:
tan (pi * x) = tan (pi * y)

goal (1 subgoal):
 1. tan (x * pi) = tan (y * pi)
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
tan (x * pi) = tan (y * pi)

goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
tan (x * pi) = tan (y * pi)

goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
have "... = tan (y' * pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tan (y * pi) = tan (y' * pi)
[PROOF STEP]
unfolding y'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tan (y * pi) = tan ((if y < 1 / 2 then y else y - 1) * pi)
[PROOF STEP]
using tan_periodic_int[of _ "- 1",simplified]
[PROOF STATE]
proof (prove)
using this:
tan (?x - pi) = tan ?x

goal (1 subgoal):
 1. tan (y * pi) = tan ((if y < 1 / 2 then y else y - 1) * pi)
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
tan (y * pi) = tan (y' * pi)

goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
show "tan (x' * pi) = tan (y' * pi)"
[PROOF STATE]
proof (prove)
using this:
tan (x' * pi) = tan (y' * pi)

goal (1 subgoal):
 1. tan (x' * pi) = tan (y' * pi)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
tan (x' * pi) = tan (y' * pi)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x' * pi = y' * pi

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' * pi = y' * pi
[PROOF STEP]
have "x'=y'"
[PROOF STATE]
proof (prove)
using this:
x' * pi = y' * pi

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' = y'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x' = y'

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using that(2,3)
[PROOF STATE]
proof (prove)
using this:
x' = y'
x \<in> A
y \<in> A

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding x'_def y'_def A_def
[PROOF STATE]
proof (prove)
using this:
(if x < 1 / 2 then x else x - 1) = (if y < 1 / 2 then y else y - 1)
x \<in> {t. 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
y \<in> {t. 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (auto split:if_splits)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>tan (pi * ?x) = tan (pi * ?y); ?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> ?x = ?y

goal (2 subgoals):
 1. finite {x. poly qq x = 0}
 2. inj_on (\<lambda>t. tan (pi * t)) A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>tan (pi * ?x) = tan (pi * ?y); ?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> ?x = ?y
[PROOF STEP]
show "inj_on (\<lambda>t. tan (pi * t)) A"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tan (pi * ?x) = tan (pi * ?y); ?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. inj_on (\<lambda>t. tan (pi * t)) A
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tan (pi * ?x) = tan (pi * ?y); ?x \<in> A; ?y \<in> A\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. tan (pi * x) = tan (pi * y) \<longrightarrow> x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>t. tan (pi * t)) A

goal (1 subgoal):
 1. finite {x. poly qq x = 0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. poly qq x = 0}
[PROOF STEP]
have "qq\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qq \<noteq> 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> qq \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> qq \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<not> qq \<noteq> 0

goal (1 subgoal):
 1. \<not> qq \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> qq \<noteq> 0
[PROOF STEP]
have "Re ((poly p \<circ> circlepath z0 r) t) = 0" when "t\<in>{0..1} - {1/2}" for t
[PROOF STATE]
proof (prove)
using this:
\<not> qq \<noteq> 0

goal (1 subgoal):
 1. Re ((poly p \<circ> circlepath z0 r) t) = 0
[PROOF STEP]
apply (subst poly_eq)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<not> qq \<noteq> 0 \<Longrightarrow> 0 \<le> t
 2. \<not> qq \<noteq> 0 \<Longrightarrow> t \<le> 1
 3. \<not> qq \<noteq> 0 \<Longrightarrow> t \<noteq> 1 / 2
 4. \<not> qq \<noteq> 0 \<Longrightarrow> poly qq (tan (pi * t)) = 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
t \<in> {0..1} - {1 / 2}

goal (4 subgoals):
 1. \<not> qq \<noteq> 0 \<Longrightarrow> 0 \<le> t
 2. \<not> qq \<noteq> 0 \<Longrightarrow> t \<le> 1
 3. \<not> qq \<noteq> 0 \<Longrightarrow> t \<noteq> 1 / 2
 4. \<not> qq \<noteq> 0 \<Longrightarrow> poly qq (tan (pi * t)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?t \<in> {0..1} - {1 / 2} \<Longrightarrow> Re ((poly p \<circ> circlepath z0 r) ?t) = 0

goal (1 subgoal):
 1. \<not> qq \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t \<in> {0..1} - {1 / 2} \<Longrightarrow> Re ((poly p \<circ> circlepath z0 r) ?t) = 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..1} - {1 / 2} \<Longrightarrow> Re ((poly p \<circ> circlepath z0 r) ?t) = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..1} - {1 / 2} \<Longrightarrow> Re ((poly p \<circ> circlepath z0 r) ?t) = 0
\<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0)

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

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

goal (1 subgoal):
 1. finite {x. poly qq x = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qq \<noteq> 0
[PROOF STEP]
show "finite {x. poly qq x = 0}"
[PROOF STATE]
proof (prove)
using this:
qq \<noteq> 0

goal (1 subgoal):
 1. finite {x. poly qq x = 0}
[PROOF STEP]
by (simp add: poly_roots_finite)
[PROOF STATE]
proof (state)
this:
finite {x. poly qq x = 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>t. tan (pi * t)) -` {x. poly qq x = 0} \<inter> A)

goal (1 subgoal):
 1. finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite ((\<lambda>t. tan (pi * t)) -` {x. poly qq x = 0} \<inter> A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite ((\<lambda>t. tan (pi * t)) -` {x. poly qq x = 0} \<inter> A)

goal (1 subgoal):
 1. finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
[PROOF STEP]
by (elim rev_finite_subset) (auto simp:A_def)
[PROOF STATE]
proof (state)
this:
finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
have "{t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t\<noteq>1/2} = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2} = S
[PROOF STEP]
unfolding S_def P_def A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2} = {t \<in> {0..1} - {1, 1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0}
[PROOF STEP]
using poly_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?t; ?t \<le> 1; ?t \<noteq> 1 / 2\<rbrakk> \<Longrightarrow> (Re ((poly p \<circ> circlepath z0 r) ?t) = 0) = (poly qq (tan (pi * ?t)) = 0)

goal (1 subgoal):
 1. {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2} = {t \<in> {0..1} - {1, 1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2} = S

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
{t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2} = S
[PROOF STEP]
have "finite S"
[PROOF STATE]
proof (prove)
using this:
finite {t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2}
{t. poly qq (tan (pi * t)) = 0 \<and> 0 \<le> t \<and> t < 1 \<and> t \<noteq> 1 / 2} = S

goal (1 subgoal):
 1. finite S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite S

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite S
[PROOF STEP]
have "finite (S \<union> (if P 1 then {1} else {}) \<union> (if P (1/2) then {1/2} else {}))"
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. finite (S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}))

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}))

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
have "(S \<union> (if P 1 then {1} else {}) \<union> (if P (1/2) then {1/2} else {}))
                      = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
have "1\<in>A" "1/2 \<in>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<in> A &&& 1 / 2 \<in> A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<in> {0..1} &&& 1 / 2 \<in> {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<in> A
1 / 2 \<in> A

goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<in> A
1 / 2 \<in> A
[PROOF STEP]
have "(S \<union> (if P 1 then {1} else {}) \<union> (if P (1/2) then {1/2} else {}))
                      = {t\<in>A. P t}"
[PROOF STATE]
proof (prove)
using this:
1 \<in> A
1 / 2 \<in> A

goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t \<in> A. P t}
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
using this:
1 \<in> A
1 / 2 \<in> A

goal (1 subgoal):
 1. {t \<in> A - {1, 1 / 2}. P t} \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t \<in> A. P t}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>1 \<in> A; 1 / 2 \<in> A; P 1; \<not> P (1 / 2); x \<in> A; P x; x * 2 = 1\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>1 \<in> A; 1 / 2 \<in> A; \<not> P 1; \<not> P (1 / 2); x \<in> A; P x; x * 2 = 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis eq_divide_eq_numeral1(1) zero_neq_numeral)+
[PROOF STATE]
proof (state)
this:
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t \<in> A. P t}

goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t \<in> A. P t}

goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
have "... = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t \<in> A. P t} = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t \<in> {0..1}. P t} = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{t \<in> A. P t} = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}))
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
have "finite {t. P t \<and> 0 \<le> t \<and> t \<le> 1}"
[PROOF STATE]
proof (prove)
using this:
finite (S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}))
S \<union> (if P 1 then {1} else {}) \<union> (if P (1 / 2) then {1 / 2} else {}) = {t. P t \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. finite {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {t. P t \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {t. P t \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {t. P t \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
using this:
finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. \<not> (\<forall>t\<in>{0..1} - {1 / 2}. Re ((poly p \<circ> circlepath z0 r) t) = 0) \<Longrightarrow> finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1}

goal (1 subgoal):
 1. finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0
[PROOF STEP]
apply (rule_tac finite_imp_finite_ReZ_segments)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {t. Re ((poly p \<circ> circlepath z0 r) t) = 0 \<and> 0 \<le> t \<and> t \<le> 1} \<Longrightarrow> finite {t. Re ((poly p \<circ> circlepath z0 r) t - 0) = 0 \<and> 0 \<le> t \<and> t \<le> 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_ReZ_segments (poly p \<circ> circlepath z0 r) 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma changes_itv_smods_ext_geq_0:
  assumes "a<b" "poly p a\<noteq>0" "poly p b \<noteq>0"
  shows "changes_itv_smods_ext a b p (pderiv p) \<ge>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> changes_itv_smods_ext a b p (pderiv p)
[PROOF STEP]
using sturm_ext_interval[OF assms]
[PROOF STATE]
proof (prove)
using this:
int (proots_count p {x. a < x \<and> x < b}) = changes_itv_smods_ext a b p (pderiv p)

goal (1 subgoal):
 1. 0 \<le> changes_itv_smods_ext a b p (pderiv p)
[PROOF STEP]
by auto


[STATEMENT]
lemma bij_betw_plane_ball:"bij_betw (\<lambda>x. (\<i>-x)/(\<i>+x)) {x. Im x>0} (ball 0 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. 0 < Im x} (ball 0 1)
[PROOF STEP]
proof (rule bij_betw_imageI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. 0 < Im x}
 2. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1
[PROOF STEP]
have neq:"\<i> + x \<noteq>0" when "Im x>0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> + x \<noteq> 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < Im x

goal (1 subgoal):
 1. \<i> + x \<noteq> 0
[PROOF STEP]
by (metis add_less_same_cancel2 add_uminus_conv_diff diff_0 diff_add_cancel
        imaginary_unit.simps(2) not_one_less_zero uminus_complex.sel(2))
[PROOF STATE]
proof (state)
this:
0 < Im ?x \<Longrightarrow> \<i> + ?x \<noteq> 0

goal (2 subgoals):
 1. inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. 0 < Im x}
 2. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < Im ?x \<Longrightarrow> \<i> + ?x \<noteq> 0
[PROOF STEP]
show "inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. 0 < Im x}"
[PROOF STATE]
proof (prove)
using this:
0 < Im ?x \<Longrightarrow> \<i> + ?x \<noteq> 0

goal (1 subgoal):
 1. inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. 0 < Im x}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
0 < Im ?x \<Longrightarrow> \<i> + ?x \<noteq> 0

goal (1 subgoal):
 1. \<forall>x\<in>{x. 0 < Im x}. \<forall>y\<in>{x. 0 < Im x}. (\<i> - x) / (\<i> + x) = (\<i> - y) / (\<i> + y) \<longrightarrow> x = y
[PROOF STEP]
by (auto simp add:divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. 0 < Im x}

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1
[PROOF STEP]
have "cmod ((\<i> - x) / (\<i> + x)) < 1" when "0 < Im x " for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod ((\<i> - x) / (\<i> + x)) < 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod ((\<i> - x) / (\<i> + x)) < 1
[PROOF STEP]
have "cmod (\<i> - x) < cmod (\<i> + x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (\<i> - x) < cmod (\<i> + x)
[PROOF STEP]
unfolding norm_lt inner_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (\<i> - x) * Re (\<i> - x) + Im (\<i> - x) * Im (\<i> - x) < Re (\<i> + x) * Re (\<i> + x) + Im (\<i> + x) * Im (\<i> + x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < Im x

goal (1 subgoal):
 1. Re (\<i> - x) * Re (\<i> - x) + Im (\<i> - x) * Im (\<i> - x) < Re (\<i> + x) * Re (\<i> + x) + Im (\<i> + x) * Im (\<i> + x)
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
cmod (\<i> - x) < cmod (\<i> + x)

goal (1 subgoal):
 1. cmod ((\<i> - x) / (\<i> + x)) < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cmod (\<i> - x) < cmod (\<i> + x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod (\<i> - x) < cmod (\<i> + x)

goal (1 subgoal):
 1. cmod ((\<i> - x) / (\<i> + x)) < 1
[PROOF STEP]
unfolding norm_divide
[PROOF STATE]
proof (prove)
using this:
cmod (\<i> - x) < cmod (\<i> + x)

goal (1 subgoal):
 1. cmod (\<i> - x) / cmod (\<i> + x) < 1
[PROOF STEP]
using neq[OF that]
[PROOF STATE]
proof (prove)
using this:
cmod (\<i> - x) < cmod (\<i> + x)
\<i> + x \<noteq> 0

goal (1 subgoal):
 1. cmod (\<i> - x) / cmod (\<i> + x) < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod ((\<i> - x) / (\<i> + x)) < 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < Im ?x \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) < 1

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < Im ?x \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) < 1

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1
[PROOF STEP]
have "x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x}" when "cmod x < 1" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x}
[PROOF STEP]
proof (rule rev_image_eqI[of "\<i>*(1-x)/(1+x)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. 0 < Im x}
 2. x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))
[PROOF STEP]
have "1 + x\<noteq>0" "\<i> * 2 + \<i> * (x * 2) \<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + x \<noteq> 0 &&& \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + x \<noteq> 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cmod x < 1

goal (1 subgoal):
 1. 1 + x \<noteq> 0
[PROOF STEP]
by (metis complex_mod_triangle_sub norm_one norm_zero not_le pth_7(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cmod x < 1

goal (1 subgoal):
 1. \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
by (metis \<open>1 + x \<noteq> 0\<close> complex_i_not_zero div_mult_self4 mult_2
            mult_zero_right nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right
            one_add_one zero_neq_numeral)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
1 + x \<noteq> 0
\<i> * 2 + \<i> * (x * 2) \<noteq> 0

goal (2 subgoals):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. 0 < Im x}
 2. x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 + x \<noteq> 0
\<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
show "x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))"
[PROOF STATE]
proof (prove)
using this:
1 + x \<noteq> 0
\<i> * 2 + \<i> * (x * 2) \<noteq> 0

goal (1 subgoal):
 1. x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))

goal (1 subgoal):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. 0 < Im x}
[PROOF STEP]
show " \<i> * (1 - x) / (1 + x) \<in> {x. 0 < Im x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. 0 < Im x}
[PROOF STEP]
apply (auto simp:Im_complex_div_gt_0 algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x * Im x + Re x * Re x < 1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cmod x < 1

goal (1 subgoal):
 1. Im x * Im x + Re x * Re x < 1
[PROOF STEP]
unfolding cmod_def
[PROOF STATE]
proof (prove)
using this:
sqrt ((Re x)\<^sup>2 + (Im x)\<^sup>2) < 1

goal (1 subgoal):
 1. Im x * Im x + Re x * Re x < 1
[PROOF STEP]
by (auto simp:power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<i> * (1 - x) / (1 + x) \<in> {x. 0 < Im x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cmod ?x < 1 \<Longrightarrow> ?x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x}

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < Im ?x \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) < 1
cmod ?x < 1 \<Longrightarrow> ?x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x}
[PROOF STEP]
show "(\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1"
[PROOF STATE]
proof (prove)
using this:
0 < Im ?x \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) < 1
cmod ?x < 1 \<Longrightarrow> ?x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x}

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. 0 < Im x} = ball 0 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_axis_sphere:"bij_betw (\<lambda>x. (\<i>-x)/(\<i>+x)) {x. Im x=0} (sphere 0 1 - {-1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. Im x = 0} (sphere 0 1 - {- 1})
[PROOF STEP]
proof (rule bij_betw_imageI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. Im x = 0}
 2. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}
[PROOF STEP]
have neq:"\<i> + x \<noteq>0" when "Im x=0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> + x \<noteq> 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Im x = 0

goal (1 subgoal):
 1. \<i> + x \<noteq> 0
[PROOF STEP]
by (metis add_diff_cancel_left' imaginary_unit.simps(2) minus_complex.simps(2)
         right_minus_eq zero_complex.simps(2) zero_neq_one)
[PROOF STATE]
proof (state)
this:
Im ?x = 0 \<Longrightarrow> \<i> + ?x \<noteq> 0

goal (2 subgoals):
 1. inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. Im x = 0}
 2. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Im ?x = 0 \<Longrightarrow> \<i> + ?x \<noteq> 0
[PROOF STEP]
show "inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. Im x = 0}"
[PROOF STATE]
proof (prove)
using this:
Im ?x = 0 \<Longrightarrow> \<i> + ?x \<noteq> 0

goal (1 subgoal):
 1. inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. Im x = 0}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
Im ?x = 0 \<Longrightarrow> \<i> + ?x \<noteq> 0

goal (1 subgoal):
 1. \<forall>x\<in>{x. Im x = 0}. \<forall>y\<in>{x. Im x = 0}. (\<i> - x) / (\<i> + x) = (\<i> - y) / (\<i> + y) \<longrightarrow> x = y
[PROOF STEP]
by (auto simp add:divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. (\<i> - x) / (\<i> + x)) {x. Im x = 0}

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}
[PROOF STEP]
have "cmod ((\<i> - x) / (\<i> + x)) = 1" "(\<i> - x) / (\<i> + x) \<noteq> - 1" when "Im x = 0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod ((\<i> - x) / (\<i> + x)) = 1 &&& (\<i> - x) / (\<i> + x) \<noteq> - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cmod ((\<i> - x) / (\<i> + x)) = 1
 2. (\<i> - x) / (\<i> + x) \<noteq> - 1
[PROOF STEP]
have "cmod (\<i> + x) = cmod (\<i> - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (\<i> + x) = cmod (\<i> - x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Im x = 0

goal (1 subgoal):
 1. cmod (\<i> + x) = cmod (\<i> - x)
[PROOF STEP]
unfolding cmod_def
[PROOF STATE]
proof (prove)
using this:
Im x = 0

goal (1 subgoal):
 1. sqrt ((Re (\<i> + x))\<^sup>2 + (Im (\<i> + x))\<^sup>2) = sqrt ((Re (\<i> - x))\<^sup>2 + (Im (\<i> - x))\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (\<i> + x) = cmod (\<i> - x)

goal (2 subgoals):
 1. cmod ((\<i> - x) / (\<i> + x)) = 1
 2. (\<i> - x) / (\<i> + x) \<noteq> - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cmod (\<i> + x) = cmod (\<i> - x)
[PROOF STEP]
show "cmod ((\<i> - x) / (\<i> + x)) = 1"
[PROOF STATE]
proof (prove)
using this:
cmod (\<i> + x) = cmod (\<i> - x)

goal (1 subgoal):
 1. cmod ((\<i> - x) / (\<i> + x)) = 1
[PROOF STEP]
unfolding norm_divide
[PROOF STATE]
proof (prove)
using this:
cmod (\<i> + x) = cmod (\<i> - x)

goal (1 subgoal):
 1. cmod (\<i> - x) / cmod (\<i> + x) = 1
[PROOF STEP]
using neq[OF that]
[PROOF STATE]
proof (prove)
using this:
cmod (\<i> + x) = cmod (\<i> - x)
\<i> + x \<noteq> 0

goal (1 subgoal):
 1. cmod (\<i> - x) / cmod (\<i> + x) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod ((\<i> - x) / (\<i> + x)) = 1

goal (1 subgoal):
 1. (\<i> - x) / (\<i> + x) \<noteq> - 1
[PROOF STEP]
show "(\<i> - x) / (\<i> + x) \<noteq> - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<i> - x) / (\<i> + x) \<noteq> - 1
[PROOF STEP]
using neq[OF that]
[PROOF STATE]
proof (prove)
using this:
\<i> + x \<noteq> 0

goal (1 subgoal):
 1. (\<i> - x) / (\<i> + x) \<noteq> - 1
[PROOF STEP]
by (auto simp add:divide_simps)
[PROOF STATE]
proof (state)
this:
(\<i> - x) / (\<i> + x) \<noteq> - 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Im ?x = 0 \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) = 1
Im ?x = 0 \<Longrightarrow> (\<i> - ?x) / (\<i> + ?x) \<noteq> - 1

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Im ?x = 0 \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) = 1
Im ?x = 0 \<Longrightarrow> (\<i> - ?x) / (\<i> + ?x) \<noteq> - 1

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}
[PROOF STEP]
have "x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0}"
    when "cmod x = 1" "x\<noteq>-1" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0}
[PROOF STEP]
proof (rule rev_image_eqI[of "\<i>*(1-x)/(1+x)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. Im x = 0}
 2. x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))
[PROOF STEP]
have "1 + x\<noteq>0" "\<i> * 2 + \<i> * (x * 2) \<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + x \<noteq> 0 &&& \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + x \<noteq> 0
[PROOF STEP]
using that(2)
[PROOF STATE]
proof (prove)
using this:
x \<noteq> - 1

goal (1 subgoal):
 1. 1 + x \<noteq> 0
[PROOF STEP]
by algebra
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cmod x = 1
x \<noteq> - 1

goal (1 subgoal):
 1. \<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
by (metis \<open>1 + x \<noteq> 0\<close> complex_i_not_zero div_mult_self4 mult_2
            mult_zero_right nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right
            one_add_one zero_neq_numeral)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
1 + x \<noteq> 0
\<i> * 2 + \<i> * (x * 2) \<noteq> 0

goal (2 subgoals):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. Im x = 0}
 2. x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 + x \<noteq> 0
\<i> * 2 + \<i> * (x * 2) \<noteq> 0
[PROOF STEP]
show "x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))"
[PROOF STATE]
proof (prove)
using this:
1 + x \<noteq> 0
\<i> * 2 + \<i> * (x * 2) \<noteq> 0

goal (1 subgoal):
 1. x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
x = (\<i> - \<i> * (1 - x) / (1 + x)) / (\<i> + \<i> * (1 - x) / (1 + x))

goal (1 subgoal):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. Im x = 0}
[PROOF STEP]
show " \<i> * (1 - x) / (1 + x) \<in> {x. Im x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i> * (1 - x) / (1 + x) \<in> {x. Im x = 0}
[PROOF STEP]
apply (auto simp:algebra_simps Im_complex_div_eq_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x * Im x + Re x * Re x = 1
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
cmod x = 1

goal (1 subgoal):
 1. Im x * Im x + Re x * Re x = 1
[PROOF STEP]
unfolding cmod_def
[PROOF STATE]
proof (prove)
using this:
sqrt ((Re x)\<^sup>2 + (Im x)\<^sup>2) = 1

goal (1 subgoal):
 1. Im x * Im x + Re x * Re x = 1
[PROOF STEP]
by (auto simp:power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<i> * (1 - x) / (1 + x) \<in> {x. Im x = 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>cmod ?x = 1; ?x \<noteq> - 1\<rbrakk> \<Longrightarrow> ?x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0}

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Im ?x = 0 \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) = 1
Im ?x = 0 \<Longrightarrow> (\<i> - ?x) / (\<i> + ?x) \<noteq> - 1
\<lbrakk>cmod ?x = 1; ?x \<noteq> - 1\<rbrakk> \<Longrightarrow> ?x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0}
[PROOF STEP]
show "(\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}"
[PROOF STATE]
proof (prove)
using this:
Im ?x = 0 \<Longrightarrow> cmod ((\<i> - ?x) / (\<i> + ?x)) = 1
Im ?x = 0 \<Longrightarrow> (\<i> - ?x) / (\<i> + ?x) \<noteq> - 1
\<lbrakk>cmod ?x = 1; ?x \<noteq> - 1\<rbrakk> \<Longrightarrow> ?x \<in> (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0}

goal (1 subgoal):
 1. (\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (\<i> - x) / (\<i> + x)) ` {x. Im x = 0} = sphere 0 1 - {- 1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_ball_uball:
  assumes "r>0"
  shows "bij_betw (\<lambda>x. complex_of_real r*x + z0) (ball 0 1) (ball z0 r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>x. complex_of_real r * x + z0) (ball 0 1) (ball z0 r)
[PROOF STEP]
proof (rule bij_betw_imageI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>x. complex_of_real r * x + z0) (ball 0 1)
 2. (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1 = ball z0 r
[PROOF STEP]
show "inj_on (\<lambda>x. complex_of_real r * x + z0) (ball 0 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. complex_of_real r * x + z0) (ball 0 1)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>ball 0 1. \<forall>y\<in>ball 0 1. complex_of_real r * x + z0 = complex_of_real r * y + z0 \<longrightarrow> x = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. \<forall>x\<in>ball 0 1. \<forall>y\<in>ball 0 1. complex_of_real r * x + z0 = complex_of_real r * y + z0 \<longrightarrow> x = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. complex_of_real r * x + z0) (ball 0 1)

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1 = ball z0 r
[PROOF STEP]
have "dist z0 (complex_of_real r * x + z0) < r" when "cmod x<1" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist z0 (complex_of_real r * x + z0) < r
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
cmod x < 1
0 < r

goal (1 subgoal):
 1. dist z0 (complex_of_real r * x + z0) < r
[PROOF STEP]
by (auto simp:dist_norm norm_mult abs_of_pos)
[PROOF STATE]
proof (state)
this:
cmod ?x < 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) < r

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1 = ball z0 r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cmod ?x < 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) < r

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1 = ball z0 r
[PROOF STEP]
have "x \<in> (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1" when "dist z0 x < r" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1
[PROOF STEP]
apply (rule rev_image_eqI[of "(x-z0)/r"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (x - z0) / complex_of_real r \<in> ball 0 1
 2. x = complex_of_real r * ((x - z0) / complex_of_real r) + z0
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
dist z0 x < r
0 < r

goal (2 subgoals):
 1. (x - z0) / complex_of_real r \<in> ball 0 1
 2. x = complex_of_real r * ((x - z0) / complex_of_real r) + z0
[PROOF STEP]
by (auto simp add: dist_norm norm_divide norm_minus_commute)
[PROOF STATE]
proof (state)
this:
dist z0 ?x < r \<Longrightarrow> ?x \<in> (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1 = ball z0 r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cmod ?x < 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) < r
dist z0 ?x < r \<Longrightarrow> ?x \<in> (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1
[PROOF STEP]
show "(\<lambda>x. complex_of_real r  * x + z0) ` ball 0 1 = ball z0 r"
[PROOF STATE]
proof (prove)
using this:
cmod ?x < 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) < r
dist z0 ?x < r \<Longrightarrow> ?x \<in> (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` ball 0 1 = ball z0 r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. complex_of_real r * x + z0) ` ball 0 1 = ball z0 r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_sphere_usphere:
  assumes "r>0"
  shows "bij_betw (\<lambda>x. complex_of_real r*x + z0) (sphere 0 1) (sphere z0 r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>x. complex_of_real r * x + z0) (sphere 0 1) (sphere z0 r)
[PROOF STEP]
proof (rule bij_betw_imageI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>x. complex_of_real r * x + z0) (sphere 0 1)
 2. (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1 = sphere z0 r
[PROOF STEP]
show "inj_on (\<lambda>x. complex_of_real r * x + z0) (sphere 0 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. complex_of_real r * x + z0) (sphere 0 1)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>sphere 0 1. \<forall>y\<in>sphere 0 1. complex_of_real r * x + z0 = complex_of_real r * y + z0 \<longrightarrow> x = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. \<forall>x\<in>sphere 0 1. \<forall>y\<in>sphere 0 1. complex_of_real r * x + z0 = complex_of_real r * y + z0 \<longrightarrow> x = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. complex_of_real r * x + z0) (sphere 0 1)

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1 = sphere z0 r
[PROOF STEP]
have "dist z0 (complex_of_real r * x + z0) = r" when "cmod x=1" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist z0 (complex_of_real r * x + z0) = r
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
cmod x = 1
0 < r

goal (1 subgoal):
 1. dist z0 (complex_of_real r * x + z0) = r
[PROOF STEP]
by (auto simp:dist_norm norm_mult abs_of_pos)
[PROOF STATE]
proof (state)
this:
cmod ?x = 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) = r

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1 = sphere z0 r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cmod ?x = 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) = r

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1 = sphere z0 r
[PROOF STEP]
have "x \<in> (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1" when "dist z0 x = r" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1
[PROOF STEP]
apply (rule rev_image_eqI[of "(x-z0)/r"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (x - z0) / complex_of_real r \<in> sphere 0 1
 2. x = complex_of_real r * ((x - z0) / complex_of_real r) + z0
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
dist z0 x = r
0 < r

goal (2 subgoals):
 1. (x - z0) / complex_of_real r \<in> sphere 0 1
 2. x = complex_of_real r * ((x - z0) / complex_of_real r) + z0
[PROOF STEP]
by (auto simp add: dist_norm norm_divide norm_minus_commute)
[PROOF STATE]
proof (state)
this:
dist z0 ?x = r \<Longrightarrow> ?x \<in> (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1 = sphere z0 r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cmod ?x = 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) = r
dist z0 ?x = r \<Longrightarrow> ?x \<in> (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1
[PROOF STEP]
show "(\<lambda>x. complex_of_real r  * x + z0) ` sphere 0 1 = sphere z0 r"
[PROOF STATE]
proof (prove)
using this:
cmod ?x = 1 \<Longrightarrow> dist z0 (complex_of_real r * ?x + z0) = r
dist z0 ?x = r \<Longrightarrow> ?x \<in> (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1

goal (1 subgoal):
 1. (\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1 = sphere z0 r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. complex_of_real r * x + z0) ` sphere 0 1 = sphere z0 r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_ball_plane_eq:
  defines "q1\<equiv>[:\<i>,-1:]" and "q2\<equiv>[:\<i>,1:]"
  assumes "p\<noteq>0"
  shows "proots_count p (ball 0 1) = proots_count (fcompose p q1 q2) {x. 0 < Im x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (ball 0 1) = proots_count (fcompose p q1 q2) {x. 0 < Im x}
[PROOF STEP]
unfolding q1_def q2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (ball 0 1) = proots_count (fcompose p [:\<i>, - 1:] [:\<i>, 1:]) {x. 0 < Im x}
[PROOF STEP]
proof (rule proots_fcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 < Im x} (ball 0 1)
 2. \<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0
 3. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 4. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 5. infinite UNIV
[PROOF STEP]
show "\<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. 0 < Im x \<longrightarrow> \<i> + x \<noteq> 0
[PROOF STEP]
by (metis add_less_same_cancel2 imaginary_unit.simps(2) not_one_less_zero
          plus_complex.simps(2) zero_complex.simps(2))
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0

goal (4 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 < Im x} (ball 0 1)
 2. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 3. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 4. infinite UNIV
[PROOF STEP]
show "infinite (UNIV::complex set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
by (simp add: infinite_UNIV_char_0)
[PROOF STATE]
proof (state)
this:
infinite UNIV

goal (3 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 < Im x} (ball 0 1)
 2. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 3. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
[PROOF STEP]
qed (use bij_betw_plane_ball in auto)