Nuprl - Proof: nat prime div each factorLEMMA 1 1 1 2

(20steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

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

1. X :

2. prime(X)
3.

X1:

. X1<X

prime(X1)

(

a,b:

. X1 | a

b

X1 | a

X1 | b)
4. W :

5.

W1:

. W1<W

0<W1

W1<X

(

t:

. X | t

W1

X | t)
6. 0<W
7. W<X
8. t :

9. u :

10. t

W = X

u
11.

W = 1

X | t

By:	Inst: Thm* x:{2...}. p:{2...}. px & prime(p) & p \| x Using:[W] ...w THEN New:X1 (ExistHD Hyp:-1)

Generated subgoal:

1 12. X1 : {2...}
13. X1W
14. prime(X1)
15. X1 | W
X | t
14 steps

About:

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

(20steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc