---

Step * 1 2 of Lemma div_4_to_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
⊢ 0 < a rem -b ⇒ 0 < a
BY
{ ((D 0 THENA Auto) THEN CaseNat 0 `a') }

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
10. 0 < a rem -b
11. a = 0 ∈ ℤ
⊢ 0 < 0

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
10. 0 < a rem -b
11. ¬(a = 0 ∈ ℤ)
⊢ 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
7.  (0  rem  -b)  =  0
8.  a  =  (((a  \mdiv{}  -b)  *  (-b))  +  (a  rem  -b))
9.  (0  \mleq{}  (a  rem  -b))  \mwedge{}  a  rem  -b  <  -b
\mvdash{}  0  <  a  rem  -b  {}\mRightarrow{}  0  <  a


By

---

Latex:
((D  0  THENA  Auto)  THEN  CaseNat  0  `a')

---

Home Index