section \<open>Square roots of primes are irrational\<close>
theory Sqrt imports Complex_Main "HOL-Computational_Algebra.Primes" begin
text\<open>
The square root of any prime number (including 2) is irrational. \<close>
theorem sqrt_prime_irrational: fixes p :: nat assumes"prime p" shows"sqrt p \ \" proof from\<open>prime p\<close> have p: "p > 1" by (rule prime_gt_1_nat) assume"sqrt p \ \" thenobtain m n :: nat where n: "n \ 0" and sqrt_rat: "\sqrt p\ = m / n" and"coprime m n"by (rule Rats_abs_nat_div_natE) have eq: "m\<^sup>2 = p * n\<^sup>2" proof - from n and sqrt_rat have"m = \sqrt p\ * n" by simp thenhave"m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" by (simp add: power_mult_distrib) alsohave"(sqrt p)\<^sup>2 = p" by simp alsohave"\ * n\<^sup>2 = p * n\<^sup>2" by simp finallyshow ?thesis by linarith qed have"p dvd m \ p dvd n" proof from eq have"p dvd m\<^sup>2" .. with\<open>prime p\<close> show "p dvd m" by (rule prime_dvd_power) thenobtain k where"m = p * k" .. with eq have"p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by algebra with p have"n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) thenhave"p dvd n\<^sup>2" .. with\<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power) qed thenhave"p dvd gcd m n"by simp with\<open>coprime m n\<close> have "p = 1" by simp with p show False by simp qed
corollary sqrt_2_not_rat: "sqrt 2 \ \" using sqrt_prime_irrational [of 2] by simp
text\<open>
Here is an alternative version of the main proof, using mostly linear
forward-reasoning. While this results in less top-down structure, it is
probably closer to proofs seen in mathematics. \<close>
theorem fixes p :: nat assumes"prime p" shows"sqrt p \ \" proof from\<open>prime p\<close> have p: "p > 1" by (rule prime_gt_1_nat) assume"sqrt p \ \" thenobtain m n :: nat where n: "n \ 0" and sqrt_rat: "\sqrt p\ = m / n" and"coprime m n"by (rule Rats_abs_nat_div_natE) from n and sqrt_rat have"m = \sqrt p\ * n" by simp thenhave"m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" by (auto simp add: power2_eq_square) alsohave"(sqrt p)\<^sup>2 = p" by simp alsohave"\ * n\<^sup>2 = p * n\<^sup>2" by simp finallyhave eq: "m\<^sup>2 = p * n\<^sup>2" by linarith thenhave"p dvd m\<^sup>2" .. with\<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power) thenobtain k where"m = p * k" .. with eq have"p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by algebra with p have"n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) thenhave"p dvd n\<^sup>2" .. with\<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power) with dvd_m have"p dvd gcd m n"by (rule gcd_greatest) with\<open>coprime m n\<close> have "p = 1" by simp with p show False by simp qed
text\<open>
Another old chestnut, which is a consequence of the irrationality of \<^term>\<open>sqrt 2\<close>. \<close>
lemma"\a b::real. a \ \ \ b \ \ \ a powr b \ \" (is "\a b. ?P a b") proof (cases "sqrt 2 powr sqrt 2 \ \") case True with sqrt_2_not_rat have"?P (sqrt 2) (sqrt 2)"by simp thenshow ?thesis by blast next case False with sqrt_2_not_rat powr_powr have"?P (sqrt 2 powr sqrt 2) (sqrt 2)"by simp thenshow ?thesis by blast qed
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
