a:
, n:
. |a rem n| < |n|a:
, n:
. 0
(a rem n) & (a rem n) < na:, n:. -(a rem n) = ((-a) rem n)a:. -(-a) = aa:, n:. (a rem n) = (a rem -n)i:. |i| = |-i|| Rank | Theorem | Name |
| 7 |
Thm* a:, n:. |a rem n| < |n| | [rem_mag_bound] |
| cites | ||
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |
| 6 |
Thm* a:, n:. -(a rem n) = ((-a) rem n) | [rem_sym_1] |
| 0 | Thm* a:. -(-a) = a | [minus_minus_cancel] |
| 6 |
Thm* a:, n:. (a rem n) = (a rem -n) | [rem_sym_2] |
| 1 |
Thm* i:. |i| = |-i| | [absval_sym] |