---

Step * 2 of Lemma div_unique3


1. a : ℤ
2. n : ℤ-o
3. p : ℤ
4. ∃r:ℤ. (|r| < |n| ∧ (a = ((p * n) + r) ∈ ℤ) ∧ ((0 ≤ a) ⇒ (0 ≤ r)) ∧ (0 < r ⇒ 0 < a) ∧ (r < 0 ⇒ a < 0))
⊢ (a ÷ n) = p ∈ ℤ
BY
{ TACTIC:(D -1
          THEN (InstLemma `div_rem_sum` [⌜a⌝;⌜n⌝]⋅ THENA Auto)
          THEN (InstLemma `rem_bounds_absval` [⌜n⌝;⌜a⌝]⋅ THENA Auto)) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  p  :  \mBbbZ{}
4.  \mexists{}r:\mBbbZ{}
        (|r|  <  |n|  \mwedge{}  (a  =  ((p  *  n)  +  r))  \mwedge{}  ((0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  r))  \mwedge{}  (0  <  r  {}\mRightarrow{}  0  <  a)  \mwedge{}  (r  <  0  {}\mRightarrow{}  a  <  0))
\mvdash{}  (a  \mdiv{}  n)  =  p


By

---

Latex:
TACTIC:(D  -1
                THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index