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

. b = a1

By:	(Using [`n',b] (FwdThru Thm* a,b,n:. a = b na = nb [10])) THEN (Thin 10) THEN (ArithSimp 10)

Generated subgoal:

1 10. a1bx+a2by = b
c:. b = a1a2c
2 steps

About:

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