---

Step * 1 of Lemma div_4_to_1


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

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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index