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

At: rem minus
x:, n:. ((-x) rem n) = -(x rem n)
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:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n) [-x;n;-(x n);-(x rem n)]
Generated subgoals:

11. x:
2. n:
3. x = (x n)n+(x rem n)
4. |x rem n| < |n|
5. (x rem n) < 0 x < 0
6. (x rem n) > 0 x > 0
|-(x rem n)| < |n|		2 steps
 
21. x:
2. n:
3. x = (x n)n+(x rem n)
4. |x rem n| < |n|
5. (x rem n) < 0 x < 0
6. (x rem n) > 0 x > 0
7. -(x rem n) < 0
-x < 0		1 step
 
31. x:
2. n:
3. x = (x n)n+(x rem n)
4. |x rem n| < |n|
5. (x rem n) < 0 x < 0
6. (x rem n) > 0 x > 0
7. -(x rem n) > 0
-x > 0		1 step

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequalimpliesandall

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