---

Step * 1 of Lemma div_3_to_1


1. a : ℤ
2. a ≤ 0
3. b : ℤ
4. b ≤ (-1)
5. 0 ≤ ((-1) * a)
6. 1 ≤ ((-1) * b)
⊢ (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 Auto
   THEN Try ((Mul ⌜-1⌝ 0⋅ THEN Complete (Auto)))) }

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

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

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

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

5
1. a : ℤ
2. a ≤ 0
3. b : ℤ
4. b ≤ (-1)
5. 0 ≤ ((-1) * a)
6. 1 ≤ ((-1) * b)
7. (0 rem -b) = 0 ∈ ℤ
8. (-a) = ((((-a) ÷ -b) * (-b)) + (-a rem -b)) ∈ ℤ
9. 0 ≤ (-a rem -b)
10. -a rem -b < -b
11. |-(-a rem -b)| < |b|
12. a = ((((-a) ÷ -b) * b) + (-(-a rem -b))) ∈ ℤ
13. (0 ≤ a) ⇒ (0 ≤ (-(-a rem -b)))
14. 0 < -(-a rem -b) ⇒ 0 < a
15. -(-a rem -b) < 0
⊢ a < 0

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  a  \mleq{}  0
3.  b  :  \mBbbZ{}
4.  b  \mleq{}  (-1)
5.  0  \mleq{}  ((-1)  *  a)
6.  1  \mleq{}  ((-1)  *  b)
\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  Auto
  THEN  Try  ((Mul  \mkleeneopen{}-1\mkleeneclose{}  0\mcdot{}  THEN  Complete  (Auto))))

---

Home Index