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

At: div rem unique

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


Generated subgoal:

11. a:
2. n:
3. q:
4. r:
5. a = qn+r
6. |r| < |n|
7. r < 0 a < 0
8. r > 0 a > 0
9. a = (a n)n+(a rem n)
10. |a rem n| < |n|
11. (a rem n) < 0 a < 0
12. (a rem n) > 0 a > 0
q = (a n) & r = (a rem n)
15 steps

About:
intnatural_numberaddmultiplydivideremainderless_thanequalimpliesandall

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