Nuprl - Proof: prime or smaller prime factor

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A number bigger than 1 is divisible by a prime.

x:{2...}.

p:{2...}. p

x & prime(p) & p | x

By:	SimilarTo Thm* x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc ...w

Generated subgoal:

1 1. x : {2...}
2. p : {2...}
3. c:{1...}. px & prime(p) & x = pc
px & prime(p) & p | x
3 steps

About:

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