43 |
43 |
44 lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m" |
44 lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m" |
45 by (rule prime_dvd_square) (simp_all add: power2_eq_square) |
45 by (rule prime_dvd_square) (simp_all add: power2_eq_square) |
46 |
46 |
47 |
47 |
48 lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" by (induct n, auto) |
48 lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" |
|
49 by (induct n, auto) |
|
50 |
49 lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \<longleftrightarrow> x < y" |
51 lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \<longleftrightarrow> x < y" |
50 using power_less_imp_less_base[of x "Suc n" y] power_strict_mono[of x y "Suc n"] |
52 by(metis linorder_not_less not_less0 power_le_imp_le_base power_less_imp_less_base) |
51 by auto |
53 |
52 lemma exp_mono_le: "(x::nat) ^ (Suc n) \<le> y ^ (Suc n) \<longleftrightarrow> x \<le> y" |
54 lemma exp_mono_le: "(x::nat) ^ (Suc n) \<le> y ^ (Suc n) \<longleftrightarrow> x \<le> y" |
53 by (simp only: linorder_not_less[symmetric] exp_mono_lt) |
55 by (simp only: linorder_not_less[symmetric] exp_mono_lt) |
54 |
56 |
55 lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \<longleftrightarrow> x = y" |
57 lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \<longleftrightarrow> x = y" |
56 using power_inject_base[of x n y] by auto |
58 using power_inject_base[of x n y] by auto |
57 |
59 |
58 |
60 |
305 let ?g = "gcd (a^n) (b^n)" |
307 let ?g = "gcd (a^n) (b^n)" |
306 let ?gn = "gcd a b^n" |
308 let ?gn = "gcd a b^n" |
307 {fix e assume H: "e dvd a^n" "e dvd b^n" |
309 {fix e assume H: "e dvd a^n" "e dvd b^n" |
308 from bezout_gcd_pow[of a n b] obtain x y |
310 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 |
311 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]] |
312 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 |
313 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)} |
314 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 |
315 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 |
316 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 |
317 gcd_unique have "?gn = ?g" by blast thus ?thesis by simp |
316 qed |
318 qed |