(42steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
sqrt
prime
irrational
2
1
1
1.
p:
2.
prime(p)
3.
0 < p
4.
m:
5.
n:
6.
m
m = p
n
n
7.
n = 0
p
n
n < 0
By:
RWO
Thm*
a,b:
. a
b < 0
a < 0 & b > 0
a > 0 & b < 0 0
THEN
OrLeft
Generated subgoal:
1
n
n > 0
1
step
About:
(42steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
n
n > 0
0 < p
m = pnn
n = 0
pnn < 0
a,b:. ab < 0 
a < 0 & b > 0 
a > 0 & b < 0
0
nn > 0
