b:
. b | 1 
prime(b)b:. b | 1 b = 1x:. prime(x) 
2
x & (
i:{2..x
}. i | x)| Rank | Theorem | Name |
| 11 | b:. b | 1 prime(b) | [no_nat_prime_divs_one] |
| cites the following: | ||
| 4 | b:. b | 1 b = 1 | [only_one_nat_divs_one] |
| 10 | x:. prime(x) 2x & (i:{2..x}. i | x) | [prime_nat] |