(42steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
sqrt
prime
irrational
1
1
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
n = 0
By:
InstHyp [n] 5
Generated subgoals:
1
n < m
10
steps
2
11.
n@0:
. n
n = p
n@0
n@0
n@0 = 0
n = 0
22
steps
About:
(42steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
n < m
n@0:
. n
n = pn@0n@0 
n@0 = 0 n = 0
m1:. m1 < m (n:. m1m1 = pnn n = 0)
m = pnn
n = 0
p)p+(m mod p)
n = 0
n < mn@0:. nn = pn@0n@0 n@0 = 0 n = 0
