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

a | b

a | c

By:

Analyze 7

Generated subgoals:

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

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

About:

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

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