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