equal
deleted
inserted
replaced
58 |
58 |
59 theorem prime_sqrt_irrational: |
59 theorem prime_sqrt_irrational: |
60 "prime (p::nat) \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>" |
60 "prime (p::nat) \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>" |
61 apply (rule notI) |
61 apply (rule notI) |
62 apply (erule Rats_abs_nat_div_natE) |
62 apply (erule Rats_abs_nat_div_natE) |
63 apply (simp del: real_of_nat_mult |
63 apply (simp del: of_nat_mult |
64 add: abs_if divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) |
64 add: abs_if divide_eq_eq prime_not_square of_nat_mult [symmetric]) |
65 done |
65 done |
66 |
66 |
67 lemmas two_sqrt_irrational = |
67 lemmas two_sqrt_irrational = |
68 prime_sqrt_irrational [OF two_is_prime_nat] |
68 prime_sqrt_irrational [OF two_is_prime_nat] |
69 |
69 |