At:
sqrt prime irrational11121112112121
1.
p:
2.
prime(p)
3.
0 < p
4.
m:
5.
m1:. m1 < m (n:. m1m1 = pnn n = 0)
6.
n:
7.
pp(m p)(m p) = 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
nn = p(m p)(m p)
By:
Using [`n',p]
(BackThru
Thm*a,b:, n:. na = nb a = b)
Generated subgoals:
m1:
(
m1 = p
p)
n = 0
n