1. a : 
2. p : 
3. prime(p)
4. p | a
5. c : 
6. c | p
7. c | a
  c | 1

By:	(Simple ((FwdThru ((Thm* p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p)) (([3])) THEN RepD

1

8. p = 0 9. (p ~ 1) 10. a:. a | p  (a ~ 1)  (a ~ p)   c | 1

4 steps

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