p:
. prime(p) 
(a1,a2:. p | a1
a2 p | a1 
p | a2)a,p:. prime(p) (CoPrime(p,a) 
p | a)a,b1,b2:. CoPrime(a,b1) CoPrime(a,b2) CoPrime(a,b1b2)| Rank | Theorem | Name |
| 11 | p:. prime(p) (a1,a2:. p | a1a2 p | a1 p | a2) | [prime_divs_prod] |
| cites the following: | ||
| 10 | a,p:. prime(p) (CoPrime(p,a) p | a) | [coprime_iff_ndivides] |
| 8 | a,b1,b2:. CoPrime(a,b1) CoPrime(a,b2) CoPrime(a,b1b2) | [coprime_prod] |