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

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

1. X :

2. prime(X)
3.

. 0<W

W<X

(

. X | t

X | t)
4. a :

5. b :

6. X | a

b
7. x :

8. r :

X
9. a = x

X+r
10. y :

11. s :

X
12. b = y

X+s
13.

r = 0
14. e :

15. a

b = X

e
16. (x

X+r)

X+s) = X

e
17. X

y+r

y+s

x)+r

s = X

X | r

By:	FwdThru: Thm* k:, n:, x,y:. kx+n = ky xy on [ Hyp:-1 ] ...

Generated subgoal:

1 18. Xxy+ry+sxe
X | rs
1 step

About:

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