x:{2...}. 
prime(x) 
(
i,j:{2..x
}. x = i
j & prime(i))x:
. prime(x) 
x<2 
(i,j:{2..x}. x = ij)x,y:, z:
. x
y xyzi:{2...}, j:. j<ijx,y:. xy 
| Rank | Theorem | Name |
| 12 | x:{2...}. prime(x) (i,j:{2..x}. x = ij & prime(i)) | [composite_with_prime_factor] |
| cites the following: | ||
| 11 | x:. prime(x) x<2 (i,j:{2..x}. x = ij) | [nonprime_nat] |
| 2 | x,y:, z:. xy xyz | [le_mul_rt_by_pos] |
| 3 | i:{2...}, j:. j<ij | [factor_smaller2] |
| 3 | x,y:. xy | [mul_nat_plus] |