(18steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: composite with prime factor 1 1
1. x : 
2. x1:. x1<x  2x1  prime(x1)  (i,j:{2..x1}. x1 = ij & prime(i))
3. 2x
4. prime(x)
  i,j:{2..x}. x = ij & prime(i)
By: FwdThru: 
Thm*  x:. prime(x)  x<2  (i,j:{2..x}. x = ij)
on [ prime(x) ] ...w
THEN
Analyze-1 ...

Generated subgoal:

1 5. i,j:{2..x}. x = ij
  i,j:{2..x}. x = ij & prime(i)
11 steps

About:
intnatural_numbermultiplyless_thanequalimpliesandorallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(18steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc