src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 54489 03ff4d1e6784 parent 54263 c4159fe6fa46 child 55358 85d81bc281d0
1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 19 01:30:14 2013 +0100
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 19 10:05:53 2013 +0100
1.3 @@ -207,12 +207,14 @@
1.4      from unimodular_reduce_norm[OF th0] o
1.5      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
1.6        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
1.7 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp del: minus_one add: minus_one [symmetric])
1.8 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp)
1.9        apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
1.10        apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
1.11        apply (rule_tac x="- ii" in exI, simp add: m power_mult)
1.12        apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
1.13 -      apply (rule_tac x="ii" in exI, simp add: m power_mult)
1.14 +      apply (auto simp add: m power_mult)
1.15 +      apply (rule_tac x="ii" in exI)
1.16 +      apply (auto simp add: m power_mult)
1.17        done
1.18      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
1.19      let ?w = "v / complex_of_real (root n (cmod b))"