n,r:
. r<n 
(q:. nmod(q
n+r;n) = r)Thm* (
n:hnum. all
Thm* (
n:hnum. (r:hnum. implies
Thm* (
n:hnum. (r:hnum. (lt(r,n)
Thm* (
n:hnum. (r:hnum. ,all(q:hnum. equal(mod(add(mult(q,n),r),n),r)))))| Theorem | Name |
| n,r:. r<n (q:. nmod(qn+r;n) = r) | [mod_mult] |
| cites the following: | |
Thm* ( n:hnum. all
Thm* ( n:hnum. (r:hnum. implies
Thm* ( n:hnum. (r:hnum. (lt(r,n)
Thm* ( n:hnum. (r:hnum. ,all(q:hnum. equal(mod(add(mult(q,n),r),n),r))))) | [hmod_mult] |