Nuprl - Proof: gcd p mul 3

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

1. a :

2. b :

3. y :

4. n :

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

7. z | n

a & z | n

z | n

By:	(Inst Thm* a,b:. u,v:. GCD(a;b;ua+vb) [a;b]) THEN ExRepD THEN (FwdThru Thm* a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2) [5;-1])

Generated subgoal:

1 7. z | na
8. z | nb
9. u :
10. v :
11. GCD(a;b;ua+vb)
12. y ~ (ua+vb)
z | ny
3 steps

About:

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