Nuprl - Proof: atomic imp prime 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. a :

(a ~ 1)
3.

. b | a

(b ~ 1)

(b ~ a)
4. b :

5. c :

6. a | b

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

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

(gcd(a;c) ~ a)

a | b

a | c

By:

Analyze 8

Generated subgoals:

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

2 8. gcd(a;c) ~ a
a | b a | c
1 step

About:

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

1	8. gcd(a;c) ~ 1 a \| b a \| c	7 steps
2	8. gcd(a;c) ~ a a \| b a \| c	1 step