---

Step * of Lemma div_unique3

∀a:ℤ. ∀n:ℤ-o.
  ∀[p:ℤ]
    uiff((a ÷ n) = p ∈ ℤ;∃r:ℤ
                          (|r| < |n|
                          ∧ (a = ((p * n) + r) ∈ ℤ)
                          ∧ ((0 ≤ a) ⇒ (0 ≤ r))
                          ∧ (0 < r ⇒ 0 < a)
                          ∧ (r < 0 ⇒ a < 0)))
BY
{ TACTIC:Auto }

1
1. a : ℤ
2. n : ℤ-o
3. [p] : ℤ
4. (a ÷ n) = p ∈ ℤ
⊢ ∃r:ℤ. (|r| < |n| ∧ (a = ((p * n) + r) ∈ ℤ) ∧ ((0 ≤ a) ⇒ (0 ≤ r)) ∧ (0 < r ⇒ 0 < a) ∧ (r < 0 ⇒ a < 0))

2
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 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}n:\mBbbZ{}\msupminus{}\msupzero{}.
    \mforall{}[p:\mBbbZ{}]
        uiff((a  \mdiv{}  n)  =  p;\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)))


By

---

Latex:
TACTIC:Auto

---

Home Index