Nuprl - Proof: coprime prod 1 1 1 1 1

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

1. a :

2. b1 :

3. b2 :

4. x1 :

5. y1 :

6. x2 :

7. y2 :

8. b1

y1 = 1+-a

x1
9. b2

y2 = 1+-a

(x1+x2-a

x2)+b1

y2 = 1

By:	(Using [`n',((1-ax1)(1-ax2)-1)] (BackThru Thm* a,b,n:. a = b a+n = b+n)) THEN (ArithSimp 0)

Generated subgoal:

1 b1b2y1y2 = 1+aax1x2+-ax1+-ax2
1 step

About:

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