Nuprl - Proof: prime divs prod 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime divs prod 1 2 1 1

1. p :

2. prime(p)
3. a1 :

4. a2 :

5. p | a1

a2
6. CoPrime(p,a1)
7. CoPrime(p,a2)

p | a2

By:	(FwdThru Thm* a,b1,b2:. CoPrime(a,b1) CoPrime(a,b2) CoPrime(a,b1b2) ([6;7]) THEN (FwdThru Thm* a,p:. prime(p) (CoPrime(p,a) p \| a) [8])

Generated subgoal:

1 8. CoPrime(p,a1a2)
9. p | a1a2
p | a2
Trivial

About:

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