Nuprl - Proof: composite with prime factor 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: composite with prime factor 1

. 2

prime(x)

(

i,j:{2..x

}. x = i

j & prime(i))

By:	CompNatInd Concl ...

Generated subgoal:

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)
12 steps

About:

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