---

Step * 3 1 1 1 1 of Lemma divide-le

.....assertion..... 
1. m3 : ℤ
2. m2 : ℤ
3. m1 : ℤ
4. a : ℕ+
5. m : ℤ
6. ¬0 < m
7. x : ℤ
8. (m + m2) ≤ m3
9. (1 + x) ≤ m1
10. (a + m3) ≤ m2
11. 0 ≤ (m + m2)
12. 0 ≤ m
13. (1 + m) ≤ a
⊢ False
BY
{ Omega1Aux Auto }

---

Latex:

---

Latex:
.....assertion..... 
1.  m3  :  \mBbbZ{}
2.  m2  :  \mBbbZ{}
3.  m1  :  \mBbbZ{}
4.  a  :  \mBbbN{}\msupplus{}
5.  m  :  \mBbbZ{}
6.  \mneg{}0  <  m
7.  x  :  \mBbbZ{}
8.  (m  +  m2)  \mleq{}  m3
9.  (1  +  x)  \mleq{}  m1
10.  (a  +  m3)  \mleq{}  m2
11.  0  \mleq{}  (m  +  m2)
12.  0  \mleq{}  m
13.  (1  +  m)  \mleq{}  a
\mvdash{}  False


By

---

Latex:
Omega1Aux  Auto

---

Home Index