6 |
6 |
7 theory Sqrt |
7 theory Sqrt |
8 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" |
8 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* The square root of any prime number (including 2) is irrational. *} |
12 The square root of any prime number (including @{text 2}) is |
|
13 irrational. |
|
14 *} |
|
15 |
12 |
16 theorem sqrt_prime_irrational: |
13 theorem sqrt_prime_irrational: |
17 assumes "prime (p::nat)" |
14 assumes "prime (p::nat)" |
18 shows "sqrt (real p) \<notin> \<rat>" |
15 shows "sqrt (real p) \<notin> \<rat>" |
19 proof |
16 proof |
86 then have "p \<le> 1" by (simp add: dvd_imp_le) |
83 then have "p \<le> 1" by (simp add: dvd_imp_le) |
87 with p show False by simp |
84 with p show False by simp |
88 qed |
85 qed |
89 |
86 |
90 |
87 |
91 text{* Another old chestnut, which is a consequence of the irrationality of 2. *} |
88 text {* Another old chestnut, which is a consequence of the irrationality of 2. *} |
92 |
89 |
93 lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "EX a b. ?P a b") |
90 lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "EX a b. ?P a b") |
94 proof cases |
91 proof cases |
95 assume "sqrt 2 powr sqrt 2 \<in> \<rat>" |
92 assume "sqrt 2 powr sqrt 2 \<in> \<rat>" |
96 hence "?P (sqrt 2) (sqrt 2)" by(metis sqrt_real_2_not_rat[simplified]) |
93 then have "?P (sqrt 2) (sqrt 2)" |
97 thus ?thesis by blast |
94 by (metis sqrt_real_2_not_rat [simplified]) |
|
95 then show ?thesis by blast |
98 next |
96 next |
99 assume 1: "sqrt 2 powr sqrt 2 \<notin> \<rat>" |
97 assume 1: "sqrt 2 powr sqrt 2 \<notin> \<rat>" |
100 have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2" |
98 have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2" |
101 using powr_realpow[of _ 2] |
99 using powr_realpow [of _ 2] |
102 by (simp add: powr_powr power2_eq_square[symmetric]) |
100 by (simp add: powr_powr power2_eq_square [symmetric]) |
103 hence "?P (sqrt 2 powr sqrt 2) (sqrt 2)" |
101 then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" |
104 by (metis 1 Rats_number_of sqrt_real_2_not_rat[simplified]) |
102 by (metis 1 Rats_number_of sqrt_real_2_not_rat [simplified]) |
105 thus ?thesis by blast |
103 then show ?thesis by blast |
106 qed |
104 qed |
107 |
105 |
108 end |
106 end |