x:{2...}, y:
. prime(y) 
x | y x = y 
a,b:. a | b 
(
c:. b = a
c)x:. prime(x) 2
x & 
(i:{2..x
}. i | x)a,b:. 0<ab 0<a & 0<bi:{2...}, j:
. j<ij| Rank | Theorem | Name |
| 11 | x:{2...}, y:. prime(y) x | y x = y | [prime_nat_divby_self_only] |
| cites the following: | ||
| 2 | a,b:. a | b (c:. b = ac) | [divides_def_on_nat] |
| 10 | x:. prime(x) 2x & (i:{2..x}. i | x) | [prime_nat] |
| 4 | a,b:. 0<ab 0<a & 0<b | [pos_mul_arg_boundsNat] |
| 3 | i:{2...}, j:. j<ij | [factor_smaller2] |