Nuprl - Proof: coprime divisors prod 1 1 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 1

1. a1 :

2. a2 :

3. b :

4. c1 :

5. b = a1

c1
6. c2 :

7. b = a2

c2
8. x :

9. y :

10. a1

x+a2

y = b

. b = a1

By:	Rewrite (NthC 1 (HypC 7) THENC NthC 1 (HypC 5)) 10

Generated subgoal:

1 10. a1a2c2x+a2a1c1y = b
c:. b = a1a2c
1 step

About:

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