Nuprl - Proof: gcd mul 1 1

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

1. a :

2. b :

3. n :

4. y :

5. GCD(a;b;y)
6. z :

7. GCD(n

a;n

b;z)

y) ~ z

By:	(Using [`n',n] (FwdThru Thm* a,b,y,n:. GCD(a;b;y) GCD(na;nb;ny) [5])) THEN (FwdThru Thm* a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2) [-1;-2])

Generated subgoals:

None

About:

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