---

Step * 3 2 of Lemma div_div


1. a : ℤ
2. n : ℤ-o
3. m : ℤ-o
4. 0 ≤ a
5. ¬(0 ≤ n)
6. 0 ≤ m
7. n * m < 0
⊢ (-((-(a ÷ n)) ÷ m)) = (-(a ÷ -n ÷ m)) ∈ ℤ
BY
{ TACTIC:RepeatFor 2 ((EqCD THEN Auto)) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  m  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  0  \mleq{}  a
5.  \mneg{}(0  \mleq{}  n)
6.  0  \mleq{}  m
7.  n  *  m  <  0
\mvdash{}  (-((-(a  \mdiv{}  n))  \mdiv{}  m))  =  (-(a  \mdiv{}  -n  \mdiv{}  m))


By

---

Latex:
TACTIC:RepeatFor  2  ((EqCD  THEN  Auto))

---

Home Index