Nuprl - Proof: mod mul 1 1

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

At: mod mul 1 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

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

By: Subst (xy = ((x n)n+(x mod n))((y n)n+(y mod n))) 0 THEN All ArithSimp

Generated subgoals:

None

About:

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