# 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 "\z. ?P z n" ..} moreover {assume o: "odd n" - from b have b': "b^2 \ 0" unfolding power2_eq_square by simp - have "Im (inverse b) * (Im (inverse b) * \Im b * Im b + Re b * Re b\) + - Re (inverse b) * (Re (inverse b) * \Im b * Im b + Re b * Re b\) = - ((Re (inverse b))^2 + (Im (inverse b))^2) * \Im b * Im b + Re b * Re b\" by algebra - also have "\ = 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) * \Im b * Im b + Re b * Re b\) + - Re (inverse b) * (Re (inverse b) * \Im b * Im b + Re b * Re b\) = - 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 "\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