(* Title: HOL/ex/Sqrt.thy Author: Markus Wenzel, Tobias Nipkow, TU Muenchen *) section ‹Square roots of primes are irrational› theory Sqrt imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin text ‹The square root of any prime number (including 2) is irrational.› theorem sqrt_prime_irrational: assumes "prime (p::nat)" shows "sqrt p ∉ \<rat>" proof from ‹prime p› have p: "1 < p" by (simp add: prime_nat_def) assume "sqrt p ∈ \<rat>" then obtain m n :: nat where n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n" and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) have eq: "m⇧^{2}= p * n⇧^{2}" proof - from n and sqrt_rat have "m = ¦sqrt p¦ * n" by simp then have "m⇧^{2}= (sqrt p)⇧^{2}* n⇧^{2}" by (auto simp add: power2_eq_square) also have "(sqrt p)⇧^{2}= p" by simp also have "… * n⇧^{2}= p * n⇧^{2}" by simp finally show ?thesis .. qed have "p dvd m ∧ p dvd n" proof from eq have "p dvd m⇧^{2}" .. with ‹prime p› show "p dvd m" by (rule prime_dvd_power_nat) then obtain k where "m = p * k" .. with eq have "p * n⇧^{2}= p⇧^{2}* k⇧^{2}" by (auto simp add: power2_eq_square ac_simps) with p have "n⇧^{2}= p * k⇧^{2}" by (simp add: power2_eq_square) then have "p dvd n⇧^{2}" .. with ‹prime p› show "p dvd n" by (rule prime_dvd_power_nat) qed then have "p dvd gcd m n" .. with gcd have "p dvd 1" by simp then have "p ≤ 1" by (simp add: dvd_imp_le) with p show False by simp qed corollary sqrt_2_not_rat: "sqrt 2 ∉ \<rat>" using sqrt_prime_irrational[of 2] by simp subsection ‹Variations› text ‹ 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. › theorem assumes "prime (p::nat)" shows "sqrt p ∉ \<rat>" proof from ‹prime p› have p: "1 < p" by (simp add: prime_nat_def) assume "sqrt p ∈ \<rat>" then obtain m n :: nat where n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n" and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) from n and sqrt_rat have "m = ¦sqrt p¦ * n" by simp then have "m⇧^{2}= (sqrt p)⇧^{2}* n⇧^{2}" by (auto simp add: power2_eq_square) also have "(sqrt p)⇧^{2}= p" by simp also have "… * n⇧^{2}= p * n⇧^{2}" by simp finally have eq: "m⇧^{2}= p * n⇧^{2}" .. then have "p dvd m⇧^{2}" .. with ‹prime p› have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) then obtain k where "m = p * k" .. with eq have "p * n⇧^{2}= p⇧^{2}* k⇧^{2}" by (auto simp add: power2_eq_square ac_simps) with p have "n⇧^{2}= p * k⇧^{2}" by (simp add: power2_eq_square) then have "p dvd n⇧^{2}" .. with ‹prime p› have "p dvd n" by (rule prime_dvd_power_nat) with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat) with gcd have "p dvd 1" by simp then have "p ≤ 1" by (simp add: dvd_imp_le) with p show False by simp qed text ‹Another old chestnut, which is a consequence of the irrationality of 2.› lemma "∃a b::real. a ∉ \<rat> ∧ b ∉ \<rat> ∧ a powr b ∈ \<rat>" (is "∃a b. ?P a b") proof cases assume "sqrt 2 powr sqrt 2 ∈ \<rat>" then have "?P (sqrt 2) (sqrt 2)" by (metis sqrt_2_not_rat) then show ?thesis by blast next assume 1: "sqrt 2 powr sqrt 2 ∉ \<rat>" have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2" using powr_realpow [of _ 2] by (simp add: powr_powr power2_eq_square [symmetric]) then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" by (metis 1 Rats_number_of sqrt_2_not_rat) then show ?thesis by blast qed end