(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
  x:{2...}. prime(x)  (i,j:{2..x}. x = ij & prime(i))
By: SideProof

Generated subgoal:

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

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

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