# HG changeset patch
# User wenzelm
# Date 1236700107 3600
# Node ID 9c9b6511ad1b6a9d45ac636009f4c35b6b36abc0
# Parent ef670320e281fc44371b11c5f63041c6cfc6f62c
tuned proofs;
tuned document;
diff r ef670320e281 r 9c9b6511ad1b src/HOL/ex/Sqrt.thy
 a/src/HOL/ex/Sqrt.thy Tue Mar 10 16:44:20 2009 +0100
+++ b/src/HOL/ex/Sqrt.thy Tue Mar 10 16:48:27 2009 +0100
@@ 1,6 +1,5 @@
(* Title: HOL/ex/Sqrt.thy
Author: Markus Wenzel, TU Muenchen

*)
header {* Square roots of primes are irrational *}
@@ 9,13 +8,6 @@
imports Complex_Main Primes
begin
text {* The definition and the key representation theorem for the set of
rational numbers has been moved to a core theory. *}

declare Rats_abs_nat_div_natE[elim?]

subsection {* Main theorem *}

text {*
The square root of any prime number (including @{text 2}) is
irrational.
@@ 29,7 +21,7 @@
assume "sqrt (real p) \ \"
then obtain m n where
n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n"
 and gcd: "gcd m n = 1" ..
+ and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
have eq: "m\ = p * n\"
proof 
from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp
@@ 75,7 +67,7 @@
assume "sqrt (real p) \ \"
then obtain m n where
n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n"
 and gcd: "gcd m n = 1" ..
+ and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp
then have "real (m\) = (sqrt (real p))\ * real (n\)"
by (auto simp add: power2_eq_square)