src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 36975 fa6244be5215 parent 36778 739a9379e29b child 37093 8808a1aa12a2
1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon May 17 15:58:32 2010 -0700
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon May 17 16:52:34 2010 -0700
1.3 @@ -214,23 +214,8 @@
1.4      hence "\<exists>z. ?P z n" ..}
1.5    moreover
1.6    {assume o: "odd n"
1.7 -    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
1.8 -    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
1.9 -    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
1.10 -    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
1.11 -    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
1.12 -      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
1.13 -      by (simp add: power2_eq_square)
1.14 -    finally
1.15 -    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
1.16 -    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
1.17 -    1"
1.18 -      apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
1.19 -      using right_inverse[OF b']
1.20 -      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
1.21      have th0: "cmod (complex_of_real (cmod b) / b) = 1"
1.22 -      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
1.23 -      by (simp add: real_sqrt_mult[symmetric] th0)
1.24 +      using b by (simp add: norm_divide)
1.25      from o have "\<exists>m. n = Suc (2*m)" by presburger+
1.26      then obtain m where m: "n = Suc (2*m)" by blast
1.27      from unimodular_reduce_norm[OF th0] o