# HG changeset patch
# User huffman
# Date 1274140354 25200
# Node ID fa6244be5215d80bcce41ca29062ac51d6574f33
# Parent  b877866b5b001fe13997827471d6df3533e3cd79
simplify proof

diff -r b877866b5b00 -r fa6244be5215 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon May 17 15:58:32 2010 -0700
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon May 17 16:52:34 2010 -0700
@@ -214,23 +214,8 @@
     hence "\<exists>z. ?P z n" ..}
   moreover
   {assume o: "odd n"
-    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
-    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
-    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
-    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
-    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
-      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
-      by (simp add: power2_eq_square)
-    finally
-    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
-    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
-    1"
-      apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
-      using right_inverse[OF b']
-      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
     have th0: "cmod (complex_of_real (cmod b) / b) = 1"
-      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
-      by (simp add: real_sqrt_mult[symmetric] th0)
+      using b by (simp add: norm_divide)
     from o have "\<exists>m. n = Suc (2*m)" by presburger+
     then obtain m where m: "n = Suc (2*m)" by blast
     from unimodular_reduce_norm[OF th0] o