Nuprl - Proof: prime divs prod 1 2 1

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

1. p :

2. prime(p)
3. a1 :

4. a2 :

5. p | a1

a2
6.

p | a1
7.

p | a2

By:	(FwdThru Thm* a,p:. prime(p) (CoPrime(p,a) p \| a) [6]) THEN (FwdThru Thm* a,p:. prime(p) (CoPrime(p,a) p \| a) [7]) THEN (OnHyps [7;6] Thin)

Generated subgoal:

1 6. CoPrime(p,a1)
7. CoPrime(p,a2)
p | a2
2 steps

About:

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