---

Step * 1 of Lemma div_2_to_1


1. a : ℤ
2. a ≤ 0
3. b : ℤ
4. 0 < b
5. 0 ≤ ((-1) * a)
⊢ (a ÷ b) = (-((-a) ÷ b)) ∈ ℤ
BY
{ ((BLemma `div_unique3` THEN Try (Complete (Auto)))
   THEN Auto
   THEN (InstLemma `rem-zero` [⌜b⌝]⋅ THENA Try (Complete (Auto)))
   THEN (InstLemma `div_rem_sum` [⌜-a⌝;⌜b⌝] THENA Try (Complete (Auto)))
   THEN (InstLemma `rem_bounds_1` [⌜-a⌝;⌜b⌝] THENA Try (Complete (Auto)))
   THEN (InstConcl [⌜-(-a rem b)⌝]⋅ THENW Try (Complete (Auto)))) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  a  \mleq{}  0
3.  b  :  \mBbbZ{}
4.  0  <  b
5.  0  \mleq{}  ((-1)  *  a)
\mvdash{}  (a  \mdiv{}  b)  =  (-((-a)  \mdiv{}  b))


By

---

Latex:
((BLemma  `div\_unique3`  THEN  Try  (Complete  (Auto)))
  THEN  Auto
  THEN  (InstLemma  `rem-zero`  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Try  (Complete  (Auto)))
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}-a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  THENA  Try  (Complete  (Auto)))
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}-a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  THENA  Try  (Complete  (Auto)))
  THEN  (InstConcl  [\mkleeneopen{}-(-a  rem  b)\mkleeneclose{}]\mcdot{}  THENW  Try  (Complete  (Auto))))

---

Home Index