---

Step * of Lemma div_anti_sym2

∀[a:ℤ]. ∀[b:ℤ-o].  (((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ)
BY
{ (Auto
   THEN (Assert -b ≠ 0 BY
               ((D 0 THENA Auto) THEN Add ⌜b⌝ (-1)⋅ THEN Auto))
   THEN TACTIC:((Decide 0 ≤ a THENA Auto) THEN (Decide 0 ≤ b THENA Auto))) }

1
1. a : ℤ
2. b : ℤ-o
3. -b ≠ 0
4. 0 ≤ a
5. 0 ≤ b
⊢ ((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ

2
1. a : ℤ
2. b : ℤ-o
3. -b ≠ 0
4. 0 ≤ a
5. ¬(0 ≤ b)
⊢ ((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ

3
1. a : ℤ
2. b : ℤ-o
3. -b ≠ 0
4. ¬(0 ≤ a)
5. 0 ≤ b
⊢ ((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ

4
1. a : ℤ
2. b : ℤ-o
3. -b ≠ 0
4. ¬(0 ≤ a)
5. ¬(0 ≤ b)
⊢ ((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    (((-a)  \mdiv{}  b)  =  (-(a  \mdiv{}  b)))


By

---

Latex:
(Auto
  THEN  (Assert  -b  \mneq{}  0  BY
                          ((D  0  THENA  Auto)  THEN  Add  \mkleeneopen{}b\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  TACTIC:((Decide  0  \mleq{}  a  THENA  Auto)  THEN  (Decide  0  \mleq{}  b  THENA  Auto)))

---

Home Index