a,b:
. prime(a
b) 
ab = a 
ab = bx:. prime(x) 
2
x & 
(
i:{2..x
}. i | x) ((A & B) A B)i,j:
. iij & jija,b:. 0<ab 0<a & 0<b| Rank | Theorem | Name |
| 11 | a,b:. prime(ab) ab = a ab = b | [prime_among_factors] |
| cites the following: | ||
| 10 | x:. prime(x) 2x & (i:{2..x}. i | x) | [prime_nat] |
| 1 | ((A & B) A B) | [not_over_and] |
| 2 | i,j:. iij & jij | [factors_bound] |
| 4 | a,b:. 0<ab 0<a & 0<b | [pos_mul_arg_boundsNat] |