(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. pp = aqq
6. p' : 
7. p = ap'
  a>0 & p>0 & p'>0


By: a:b:ab>0  a>0 & b>0  By SimilarTo: Thm: pos mul arg bounds


Generated subgoal:

1 8. a:b:ab>0  a>0 & b>0
  a>0 & p>0 & p'>0

1 step

About:
intnatural_numbermultiplyless_thanequalandorall
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