Nuprl - Proof: nat prime div each factor 1 1 a 1

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

1. X :

. 0<W

W<X

(

. X | t

X | t)
3. prime(X)
4. a :

5. b :

6. X | a

b
7. 2

X
8. x :

9. r :

X
10. a = x

X+r
11. y :

12. s :

X
13. b = y

X+s

X | a

X | b

By:	SimilarTo: r = 0 s = 0 ...w

Generated subgoals:

1   r = 0  s = 0
2 steps

2 14. r = 0
  X | a
1 step

3 14. s = 0
  X | b
1 step

About:

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