(15steps total)
Remark
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
primes
sqr
roots
LEMMA1
1
2
1
a
1.
a
:
2. prime(
a
)
3.
p
:
4.
q
:
5.
p
p
=
a
q
q
6.
p'
:
7.
p
=
a
p'
a
>0 &
p
>0 &
p'
>0
By:
a
:
,
b
:
.
a
b
>0
a
>0 &
b
>0 By SimilarTo: Thm:
pos
mul
arg
bounds
Generated subgoal:
1
8.
a
:
,
b
:
.
a
b
>0
a
>0 &
b
>0
a
>0 &
p
>0 &
p'
>0
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(15steps total)
Remark
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc