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

(21steps total) Remark 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 factor 1 1 a

1. X :

2.

W:

. 0<W

W<X

(

t:

. X | t

W

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

5. b :

6. X | a

b

X | a

X | b

By:

{Apply Thm*

a:

, b:

.

q:

, r:

b. a = q

b+r to divide a and b by X }
(Inst: Thm*

x:

. prime(x)

2

x Using:[X] ...a

)
THEN
(let T

Inst: Thm*

a:

, b:

.

q:

, r:

b. a = q

b+r in
(T Using:[a | X] ...w

THEN CBV-1:

x:

, r:

X. <prop> THEN ExistHD Hyp:-1
(THEN
(T Using:[b | X] ...w

THEN CBV-1:

y:

, s:

X. <prop> THEN ExistHD Hyp:-1)

Generated subgoal:

1 7. 2X
8. x :
9. r : X
10. a = xX+r
11. y :
12. s : X
13. b = yX+s
X | a X | b
5 steps

About:

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

(21steps total) Remark PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc