src/HOL/Number_Theory/Primes.thy
changeset 33946 fcc20072df9a
parent 33718 06e9aff51d17
child 35644 d20cf282342e
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Dec 04 08:26:25 2009 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Dec 04 08:52:09 2009 +0100
     1.3 @@ -360,16 +360,15 @@
     1.4      from prime_dvd_mult_nat[OF p pab']
     1.5      have "p dvd a \<or> p dvd b" .
     1.6      moreover
     1.7 -    {assume pa: "p dvd a"
     1.8 -      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
     1.9 +    { assume pa: "p dvd a"
    1.10        from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
    1.11        with p have "coprime b p"
    1.12          by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
    1.13        hence pnb: "coprime (p^n) b"
    1.14          by (subst gcd_commute_nat, rule coprime_exp_nat)
    1.15 -      from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
    1.16 +      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
    1.17      moreover
    1.18 -    {assume pb: "p dvd b"
    1.19 +    { assume pb: "p dvd b"
    1.20        have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
    1.21        from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
    1.22          by auto
    1.23 @@ -377,7 +376,7 @@
    1.24          by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
    1.25        hence pna: "coprime (p^n) a"
    1.26          by (subst gcd_commute_nat, rule coprime_exp_nat)
    1.27 -      from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
    1.28 +      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
    1.29      ultimately have ?thesis by blast}
    1.30    ultimately show ?thesis by blast
    1.31  qed