equal
deleted
inserted
replaced
24 from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp |
24 from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp |
25 then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" |
25 then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" |
26 by (auto simp add: power2_eq_square) |
26 by (auto simp add: power2_eq_square) |
27 also have "(sqrt p)\<^sup>2 = p" by simp |
27 also have "(sqrt p)\<^sup>2 = p" by simp |
28 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp |
28 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp |
29 finally show ?thesis .. |
29 finally show ?thesis using of_nat_eq_iff by blast |
30 qed |
30 qed |
31 have "p dvd m \<and> p dvd n" |
31 have "p dvd m \<and> p dvd n" |
32 proof |
32 proof |
33 from eq have "p dvd m\<^sup>2" .. |
33 from eq have "p dvd m\<^sup>2" .. |
34 with \<open>prime p\<close> show "p dvd m" by (rule prime_dvd_power_nat) |
34 with \<open>prime p\<close> show "p dvd m" by (rule prime_dvd_power_nat) |
67 from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp |
67 from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp |
68 then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" |
68 then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" |
69 by (auto simp add: power2_eq_square) |
69 by (auto simp add: power2_eq_square) |
70 also have "(sqrt p)\<^sup>2 = p" by simp |
70 also have "(sqrt p)\<^sup>2 = p" by simp |
71 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp |
71 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp |
72 finally have eq: "m\<^sup>2 = p * n\<^sup>2" .. |
72 finally have eq: "m\<^sup>2 = p * n\<^sup>2" using of_nat_eq_iff by blast |
73 then have "p dvd m\<^sup>2" .. |
73 then have "p dvd m\<^sup>2" .. |
74 with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) |
74 with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) |
75 then obtain k where "m = p * k" .. |
75 then obtain k where "m = p * k" .. |
76 with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps) |
76 with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps) |
77 with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) |
77 with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) |