Nuprl - Proof: coprime prod 1 1 1

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

1. a :

2. b1 :

3. b2 :

4. x1 :

5. y1 :

6. a

x1+b1

y1 = 1
7. x2 :

8. y2 :

9. a

x2+b2

y2 = 1

x,y:

. a

x+b1

y = 1

By:	(Using [`n',(-ax1)] (FwdThru Thm* a,b,n:. a = b a+n = b+n [6])) THEN (Using [`n',(-ax2)] (FwdThru Thm* a,b,n:. a = b a+n = b+n [9])) THEN (OnHyps [9;6] Thin) THEN (ArithSimp 8) THEN (ArithSimp 9)

Generated subgoal:

1 6. x2 :
7. y2 :
8. b1y1 = 1+-ax1
9. b2y2 = 1+-ax2
x,y:. ax+b1b2y = 1
3 steps

About:

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