| Rank | Theorem | Name |
| 5 | Thm*  p:   . prime(p)   (m,n: . m m = pnn n = 0) | [sqrt_prime_irrational] |
| cites |
| 2 | Thm* a:, n: . a = (a   n)n+(a mod n) & (a mod n) < n | [div_floor_mod_properties] |
| 0 | Thm* a,b:. ab = ba | [mul_com] |
| 0 | Thm* a,b:, n:. a b nanb | [mul_preserves_le] |
| 1 | Thm* a,b:, n:. na < nb a < b | [mul_cancel_in_lt] |
| 3 | Thm* a,b:, n:. na = nb a = b | [mul_cancel_in_eq] |
| 2 | Thm* a,b:. 0 < ab | [mul_bounds_1b] |
| 4 | Thm* a,b:. ab < 0  a < 0 & b > 0  a > 0 & b < 0 | [neg_mul_arg_bounds] |
| 3 | Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0 | [pos_mul_arg_bounds] |
| 1 | Thm* a,b:. 0ab | [mul_bounds_1a] |