48 apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) |
48 apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) |
49 apply (blast dest: rearrange reduction) |
49 apply (blast dest: rearrange reduction) |
50 done |
50 done |
51 |
51 |
52 |
52 |
53 subsection {* The set of rational numbers *} |
|
54 |
|
55 definition |
|
56 rationals :: "real set" ("\<rat>") where |
|
57 "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
|
58 |
|
59 |
|
60 subsection {* Main theorem *} |
53 subsection {* Main theorem *} |
61 |
54 |
62 text {* |
55 text {* |
63 The square root of any prime number (including @{text 2}) is |
56 The square root of any prime number (including @{text 2}) is |
64 irrational. |
57 irrational. |
65 *} |
58 *} |
66 |
59 |
67 theorem prime_sqrt_irrational: |
60 theorem prime_sqrt_irrational: |
68 "prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>" |
61 "prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>" |
69 apply (simp add: rationals_def real_abs_def) |
62 apply (rule notI) |
70 apply clarify |
63 apply (erule Rats_abs_nat_div_natE) |
71 apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp) |
|
72 apply (simp del: real_of_nat_mult |
64 apply (simp del: real_of_nat_mult |
73 add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) |
65 add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) |
74 done |
66 done |
75 |
67 |
76 lemmas two_sqrt_irrational = |
68 lemmas two_sqrt_irrational = |
77 prime_sqrt_irrational [OF two_is_prime] |
69 prime_sqrt_irrational [OF two_is_prime] |
78 |
70 |