(* 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 ∉ ℚ" proof from ‹prime p› have p: "1 < p" by (simp add: prime_nat_iff) assume "sqrt p ∈ ℚ" then obtain 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⇧^{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 using of_nat_eq_iff by blast 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" by simp with ‹coprime m n› 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 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 ∉ ℚ" proof from ‹prime p› have p: "1 < p" by (simp add: prime_nat_iff) assume "sqrt p ∈ ℚ" then obtain 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 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}" using of_nat_eq_iff by blast 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) with ‹coprime m n› have "p = 1" by simp 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 ∉ ℚ ∧ b ∉ ℚ ∧ a powr b ∈ ℚ" (is "∃a b. ?P a b") proof cases assume "sqrt 2 powr sqrt 2 ∈ ℚ" 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 ∉ ℚ" 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