1. a : 
2. b1 : 
3. b2 : 
4. CoPrime(a,b1)
5. CoPrime(a,b2)
  CoPrime(a,b1b2)

By:	(FwdThru Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1) [4]) THEN (FwdThru Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1) [5]) THEN (OnHyps [5;4] Thin) THEN (BackThru Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1))

1

4. x,y:. ax+b1y = 1 5. x,y:. ax+b2y = 1   x,y:. ax+b1b2y = 1

5 steps

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