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))"