At:
sqrt prime irrational
1
1
1
1
1
2
1
1.
p: 

2.
prime(p)
3.
0 < p
4.
m:
5.
m1:
. m1 < m 
(
n:
. m1
m1 = p
n
n 
n = 0)
6.
n:
7.
m
m = p
n
n
8.
n = 0
9.
m = (m 
p)
p+(m mod p)
10.
(m mod p) < p
11.
m
n
12.
0 < n
n
13.
n
m
n
n
14.
m
m
m
n
15.
m
n = n
m
n < m
By:
Inst
Thm*
a,b:
, n:
. a
b 
n
a
n
b
[2;p;n
n]
Generated subgoal:
1 | 2 p | 5 steps |
About: