p:
. prime(p) 
(b,z:. p | z
b b 
0 & p | z)b:
. b | 1 
prime(b)p:.
Thm* prime(p)
Thm*
Thm* (
a,b:, e:({a..b
}
).
Thm* (a<b
p | (
i:{a..b}. e(i)) (
i:{a..b}. p | e(i)))| Rank | Theorem | Name |
| 18 | p:. prime(p) (b,z:. p | zb b 0 & p | z) | [prime_divs_exp] |
| cites the following: | ||
| 12 | b:. b | 1 prime(b) | [no_prime_divs_one] |
| 17 | p:.
Thm* prime(p) Thm*
Thm* ( a,b:, e:({a..b}).
Thm* (a<b p | ( i:{a..b}. e(i)) (i:{a..b}. p | e(i))) | [prime_divs_mul_via_intseg] |