a:
. atomic(a) 
prime(a)a:. atomic(a) 
(a ~ 1) & (b:. b | a (b ~ 1) 
(b ~ a))a,b:. gcd(a;b) | aa,b1,b2:. CoPrime(a,b1) CoPrime(a,b2) CoPrime(a,b1
b2)a,b:. CoPrime(a,b) (gcd(a;b) ~ 1)a,b:. gcd(a;b) | b| Rank | Theorem | Name |
| 9 | a:. atomic(a) prime(a) | [atomic_imp_prime] |
| cites the following: | ||
| 7 | a:. atomic(a) (a ~ 1) & (b:. b | a (b ~ 1) (b ~ a)) | [atomic_char] |
| 0 | a,b:. gcd(a;b) | a | [gcd_is_divisor_1] |
| 8 | a,b1,b2:. CoPrime(a,b1) CoPrime(a,b2) CoPrime(a,b1b2) | [coprime_prod] |
| 1 | a,b:. CoPrime(a,b) (gcd(a;b) ~ 1) | [coprime_elim_a] |
| 0 | a,b:. gcd(a;b) | b | [gcd_is_divisor_2] |