Nuprl - Proof: rem mul 1

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

At: rem mul 1

1. x:
2. y:
3. n:
4. x = (x n)n+(x rem n)
5. |x rem n| < |n|
6. (x rem n) < 0 x < 0
7. (x rem n) > 0 x > 0
8. y = (y n)n+(y rem n)
9. |y rem n| < |n|
10. (y rem n) < 0 y < 0
11. (y rem n) > 0 y > 0
12. (x rem n)(y rem n) = (((x rem n)(y rem n)) n)n+(((x rem n)(y rem n)) rem n)
13. |((x rem n)(y rem n)) rem n| < |n|
14. (((x rem n)(y rem n)) rem n) < 0 (x rem n)(y rem n) < 0
15. (((x rem n)(y rem n)) rem n) > 0 (x rem n)(y rem n) > 0

((xy) rem n) = (((x rem n)(y rem n)) rem n)

By: Inst Thm* a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n) [xy;n;(x n)(y n)n+(x n)(y rem n)+(x rem n)(y n)+(((x rem n)(y rem n)) n);((x rem n)(y rem n)) rem n]

Generated subgoals:

1 xy = ((x n)(y n)n+(x n)(y rem n)+(x rem n)(y n)+(((x rem n)(y rem n)) n))n+(((x rem n)(y rem n)) rem n) 1 step

2 16. (((x rem n)(y rem n)) rem n) < 0
xy < 0 1 step

3 16. (((x rem n)(y rem n)) rem n) > 0
xy > 0 1 step

About:

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

1	`xy = ((x n)(y n)n+(x n)(y rem n)+(x rem n)(y n)+(((x rem n)(y rem n)) n))n+(((x rem n)(y rem n)) rem n)`	1 step

2	16. `(((x rem n)(y rem n)) rem n) < 0` `xy < 0`	1 step

3	16. `(((x rem n)(y rem n)) rem n) > 0` `xy > 0`	1 step