305 let ?g = "gcd (a^n) (b^n)" |
305 let ?g = "gcd (a^n) (b^n)" |
306 let ?gn = "gcd a b^n" |
306 let ?gn = "gcd a b^n" |
307 {fix e assume H: "e dvd a^n" "e dvd b^n" |
307 {fix e assume H: "e dvd a^n" "e dvd b^n" |
308 from bezout_gcd_pow[of a n b] obtain x y |
308 from bezout_gcd_pow[of a n b] obtain x y |
309 where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast |
309 where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast |
310 from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]] |
310 from nat_dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]] |
311 dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy |
311 nat_dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy |
312 have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)} |
312 have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)} |
313 hence th: "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast |
313 hence th: "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast |
314 from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th |
314 from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th |
315 gcd_unique have "?gn = ?g" by blast thus ?thesis by simp |
315 gcd_unique have "?gn = ?g" by blast thus ?thesis by simp |
316 qed |
316 qed |