At:
sqrt prime irrational111211121111
1.
p:
2.
prime(p)
3.
0 < p
4.
m:
5.
m1:. m1 < m (n:. m1m1 = pnn n = 0)
6.
n:
7.
((m p)p+(m mod p))((m p)p+(m mod p)) = pnn
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) = pc
15.
c < 1
16.
c < 0
pc < 0
By:
BackThru
Thm*a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0
THEN
OrRight
Generated subgoals:
m1:
(
m1 = p
p)
n = 0
p
a > 0 & b < 0