equal
deleted
inserted
replaced
66 "p \<in> prime \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>" |
66 "p \<in> prime \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>" |
67 apply (simp add: rationals_def real_abs_def) |
67 apply (simp add: rationals_def real_abs_def) |
68 apply clarify |
68 apply clarify |
69 apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp) |
69 apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp) |
70 apply (simp del: real_of_nat_mult |
70 apply (simp del: real_of_nat_mult |
71 add: real_divide_eq_eq prime_not_square |
71 add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) |
72 real_of_nat_mult [symmetric]) |
|
73 done |
72 done |
74 |
73 |
75 lemmas two_sqrt_irrational = |
74 lemmas two_sqrt_irrational = |
76 prime_sqrt_irrational [OF two_is_prime] |
75 prime_sqrt_irrational [OF two_is_prime] |
77 |
76 |