Nuprl - Proof: coprime bezout id2 1 1 3 1

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

1. a :

2. b :

3. x :

4. y :

5. a

x+b

y = 1
6. z :

7. z | a
8. z | b
9. z | a

x
10. z | b

z | 1

By:	FwdThru Thm* a,b1,b2:. a \| b1 a \| b2 a \| b1+b2 [9;10]

Generated subgoal:

1 11. z | ax+by
z | 1
2 steps

About:

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