---

Step * of Lemma div_3_to_1

∀[a:{...0}]. ∀[b:{...-1}].  ((a ÷ b) = ((-a) ÷ -b) ∈ ℤ)
BY
{ (Auto
   THEN (D 2 THENA Auto)
   THEN (D 1 THENA Auto)
   THEN Add ⌜-a⌝ 2⋅
   THEN (RW  IntNormC (-1) THENA Auto)
   THEN Add ⌜1 - b⌝ (-2)⋅
   THEN (RW  IntNormC (-1) THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[a:\{...0\}].  \mforall{}[b:\{...-1\}].    ((a  \mdiv{}  b)  =  ((-a)  \mdiv{}  -b))


By

---

Latex:
(Auto
  THEN  (D  2  THENA  Auto)
  THEN  (D  1  THENA  Auto)
  THEN  Add  \mkleeneopen{}-a\mkleeneclose{}  2\mcdot{}
  THEN  (RW    IntNormC  (-1)  THENA  Auto)
  THEN  Add  \mkleeneopen{}1  -  b\mkleeneclose{}  (-2)\mcdot{}
  THEN  (RW    IntNormC  (-1)  THENA  Auto))

---

Home Index