equal
deleted
inserted
replaced
88 qed "gcd_mult_distrib2"; |
88 qed "gcd_mult_distrib2"; |
89 |
89 |
90 (*This theorem leads immediately to a proof of the uniqueness of factorization. |
90 (*This theorem leads immediately to a proof of the uniqueness of factorization. |
91 If p divides a product of primes then it is one of those primes.*) |
91 If p divides a product of primes then it is one of those primes.*) |
92 goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
92 goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
93 by (Step_tac 1); |
93 by (Clarify_tac 1); |
94 by (subgoal_tac "m = gcd(m*p, m*n)" 1); |
94 by (subgoal_tac "m = gcd(m*p, m*n)" 1); |
95 by (etac ssubst 1); |
95 by (etac ssubst 1); |
96 by (rtac gcd_greatest 1); |
96 by (rtac gcd_greatest 1); |
97 by (ALLGOALS (asm_simp_tac (!simpset addsimps [gcd_mult_distrib2 RS sym]))); |
97 by (ALLGOALS (asm_simp_tac (!simpset addsimps [gcd_mult_distrib2 RS sym]))); |
98 (*Now deduce gcd(p,n)=1 to finish the proof*) |
98 (*Now deduce gcd(p,n)=1 to finish the proof*) |