Nuprl - Proof: rem add

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

x,y:, n:. ((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi

By: Auto THEN Inst Thm* a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0) [x;n] THEN Inst Thm* a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0) [y;n] THEN Inst Thm* a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0) [(x rem n)+(y rem n);n] THEN RepDHyps THEN Decide (x+y = 0)

Generated subgoals:

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
16. x+y = 0
((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi 4 steps

2 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
16. x+y = 0
((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi 7 steps

About:

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

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` 16. `x+y = 0` `((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-\|n\| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)\|n\| else 0 fi`	4 steps

2	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` 16. `x+y = 0` `((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-\|n\| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)\|n\| else 0 fi`	7 steps