Nuprl - Proof: coprime iff ndivides 1 1 1 1

(12steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: coprime iff ndivides 1 1 1 1

1. a :

2. p :

3.

p = 0
4.

(p ~ 1)
5.

b,c:

. p | b

c

p | b

p | c
6.

c:

. c | p

c | a

(c ~ 1)
7. p | a

p | p

By:

RelRST

Generated subgoals:

None

About:

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

(12steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc