Nuprl - Proof: nat prime div each factorLEMMA 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat prime div each factorLEMMA 1

1. X :

2. prime(X)
3.

X1:

. X1<X

prime(X1)

(

a,b:

. X1 | a

X1 | a

X1 | b)

. 0<W

W<X

(

. X | t

X | t)

By:	CompNatInd Concl ...

Generated subgoal:

1 4. W :
5. W1:. W1<W 0<W1 W1<X (t:. X | tW1 X | t)
6. 0<W
7. W<X
8. t :
9. X | tW
X | t
18 steps

About:

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