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

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

y2 = 1+a

x2+-a

x1+-a

By:	FwdThru Thm* i1,i2,j1,j2:. i1 = j1 i2 = j2 i1i2 = j1j2 [8;9]

Generated subgoals:

None

About:

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