p:
. prime(p) 
p = 0 & (p ~ 1) & (a:. a | p (a ~ 1) 
(a ~ p))a:. prime(a) atomic(a)| Rank | Theorem | Name |
| 9 | p:. prime(p) p = 0 & (p ~ 1) & (a:. a | p (a ~ 1) (a ~ p)) | [prime_elim] |
| cites the following: | ||
| 8 | a:. prime(a) atomic(a) | [prime_imp_atomic] |