Nuprl - Proof: atomic imp prime 1 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: atomic imp prime 1 1 1 1 1 1

1. a :

(a ~ 1)
3.

. b | a

(b ~ 1)

(b ~ a)
4. b :

5. c :

6. a | b

c
7. gcd(a;b) ~ 1
8. gcd(a;c) ~ 1

a | b

a | c

By:	(FwdThru Thm* a,b:. CoPrime(a,b) (gcd(a;b) ~ 1) [7]) THEN (FwdThru Thm* a,b:. CoPrime(a,b) (gcd(a;b) ~ 1) [8]) THEN (FwdThru Thm* a,b1,b2:. CoPrime(a,b1) CoPrime(a,b2) CoPrime(a,b1b2) ([9;10])

Generated subgoal:

1 9. CoPrime(a,b)
10. CoPrime(a,c)
11. CoPrime(a,bc)
a | b a | c
4 steps

About:

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