---

Step * 1 5 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)
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
16. a = 0 ∈ ℤ
⊢ a < 0
BY
{ (HypSubst' (-1) (-2) THEN (Subst' -0 ~ 0 -2 THENA (All Thin THEN 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
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. -(0 rem -b) < 0
16. a = 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)
7.  (0  rem  -b)  =  0
8.  (-a)  =  ((((-a)  \mdiv{}  -b)  *  (-b))  +  (-a  rem  -b))
9.  0  \mleq{}  (-a  rem  -b)
10.  -a  rem  -b  <  -b
11.  |-(-a  rem  -b)|  <  |b|
12.  a  =  ((((-a)  \mdiv{}  -b)  *  b)  +  (-(-a  rem  -b)))
13.  (0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  (-(-a  rem  -b)))
14.  0  <  -(-a  rem  -b)  {}\mRightarrow{}  0  <  a
15.  -(-a  rem  -b)  <  0
16.  a  =  0
\mvdash{}  a  <  0


By

---

Latex:
(HypSubst'  (-1)  (-2)  THEN  (Subst'  -0  \msim{}  0  -2  THENA  (All  Thin  THEN  Auto)))

---

Home Index