---

Step * 2 1 1 1 of Lemma div_unique3


1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. r : ℤ
5. |r| < |n|
6. a = (r + (n * p)) ∈ ℤ
7. (0 ≤ a) ⇒ (0 ≤ r)
8. 0 < r ⇒ 0 < a
9. r < 0 ⇒ a < 0
10. a = ((n * (a ÷ n)) + (a rem n)) ∈ ℤ
11. |a rem n| < |n|
⊢ (((-1) * n * (a ÷ n)) + (n * p)) = (((-1) * r) + (a rem n)) ∈ ℤ
BY
{ TACTIC:(Add ⌜-r⌝ 6⋅ THEN (RW IntNormC (-1) THENA Auto)) }

1
.....subterm..... T:t
2:n
1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. r : ℤ
5. |r| < |n|
6. a = (r + (n * p)) ∈ ℤ
7. (0 ≤ a) ⇒ (0 ≤ r)
8. 0 < r ⇒ 0 < a
9. r < 0 ⇒ a < 0
10. a = ((n * (a ÷ n)) + (a rem n)) ∈ ℤ
11. |a rem n| < |n|
⊢ (-r) = (-r) ∈ ℤ

2
1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. r : ℤ
5. |r| < |n|
6. a = (r + (n * p)) ∈ ℤ
7. (0 ≤ a) ⇒ (0 ≤ r)
8. 0 < r ⇒ 0 < a
9. r < 0 ⇒ a < 0
10. a = ((n * (a ÷ n)) + (a rem n)) ∈ ℤ
11. |a rem n| < |n|
12. (a + ((-1) * r)) = (n * p) ∈ ℤ
⊢ (((-1) * n * (a ÷ n)) + (n * p)) = (((-1) * r) + (a rem n)) ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  p  :  \mBbbZ{}
4.  r  :  \mBbbZ{}
5.  |r|  <  |n|
6.  a  =  (r  +  (n  *  p))
7.  (0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  r)
8.  0  <  r  {}\mRightarrow{}  0  <  a
9.  r  <  0  {}\mRightarrow{}  a  <  0
10.  a  =  ((n  *  (a  \mdiv{}  n))  +  (a  rem  n))
11.  |a  rem  n|  <  |n|
\mvdash{}  (((-1)  *  n  *  (a  \mdiv{}  n))  +  (n  *  p))  =  (((-1)  *  r)  +  (a  rem  n))


By

---

Latex:
TACTIC:(Add  \mkleeneopen{}-r\mkleeneclose{}  6\mcdot{}  THEN  (RW  IntNormC  (-1)  THENA  Auto))

---

Home Index