Nuprl - Proof: nat prime div each factor 1

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

1. X :

X1:

. X1<X

prime(X1)

(

a,b:

. X1 | a

X1 | a

X1 | b)
3. prime(X)

a,b:

. X | a

X | a

X | b

By:	FwdThru: Thm* X:. Thm* prime(X) Thm* Thm* (X1:. X1<X prime(X1) (a,b:. X1 \| ab X1 \| a X1 \| b)) Thm* Thm* (W:. 0<W W<X (t:. X \| tW X \| t)) on [ Hyp:3 \| Hyp:2 ] ... THEN Thin Hyp:2

Generated subgoal:

1 2. prime(X)
3. W:. 0<W W<X (t:. X | tW X | t)
4. a :
5. b :
6. X | ab
X | a X | b
19 steps

About:

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