Nuprl - Proof: mod add 1

(2steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: mod add 1

1. x:
2. y:
3. n:
4. x = (x n)n+(x mod n)
5. (x mod n) < n
6. y = (y n)n+(y mod n)
7. (y mod n) < n
8. (x mod n)+(y mod n) = (((x mod n)+(y mod n)) n)n+(((x mod n)+(y mod n)) mod n)
9. (((x mod n)+(y mod n)) mod n) < n

((x+y) mod n) = (((x mod n)+(y mod n)) mod n)

By: Inst Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n) [x+y;n;(x n)+(y n)+(((x mod n)+(y mod n)) n);((x mod n)+(y mod n)) mod n]

Generated subgoals:

None

About:

(2steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc