Nuprl - Proof: rem add 2 3

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

At: rem add 2 3

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
17. (((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 < 0

x+y < 0

By: MoveToConcl -1 THEN AutoBoolCase (x+y < 0) THEN AutoBoolCase ((((x rem n)+(y rem n)) rem n) < 0) THEN ThinTrivial THEN AutoBoolCase (0 < x+y)

Generated subgoal:

1 14. (((x rem n)+(y rem n)) rem n) > 0 (x rem n)+(y rem n) > 0
15. x+y = 0
16. 0x+y
17. (((x rem n)+(y rem n)) rem n) < 0
18. (x rem n)+(y rem n) < 0
19. 0 < x+y
(((x rem n)+(y rem n)) rem n)+|n| < 0 x+y < 0 1 step

About:

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