At:
sqrt prime irrational
1
1
1
2
1
1
1
2
1
1
2
1
3
1
1.
p: 
2.
prime(p)
3.
0 < p
4.
m: 
5.
m1:. m1 < m 
(n:. m1
m1 = pnn n = 0)
6.
n:
7.
0 = nnp
8.
n = 0
9.
m = (m 
p)p+(m mod p)
10.
(m mod p) < p
11.
n@0:. nn = pn@0n@0 n@0 = 0
12.
p | ((m mod p)(m mod p))
13.
c:
14.
(m mod p) = 0
15.
c < 1
16.
c < 0
17.
(m p) = 0
n = 0
By:
Inst
Thm* a,b:
. 0 < ab
[n;p]
THEN
Inst
Thm* a,b:. 0 < ab
[n;np]
Generated subgoals:
None
About:
