Nuprl - Proof: coprime divisors prod 1 1 1

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

1. a1 :

2. a2 :

3. b :

4. a1 | b
5. a2 | b
6. x :

7. y :

8. a1

x+a2

y = 1

a2 | b

By:	New [`c2'] (Analyze 5) THEN New [`c1'] (Analyze 4) THEN UnfoldTopAb 0

Generated subgoal:

1 4. c1 :
5. b = a1c1
6. c2 :
7. b = a2c2
8. x :
9. y :
10. a1x+a2y = 1
c:. b = a1a2c
3 steps

About:

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