---

Step * 3 1 2 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 + ((-1) * a)) ≤ m
⊢ 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.  \mneg{}(0  \mleq{}  (m  +  m2))
12.  0  \mgeq{}  m 
13.  (1  +  ((-1)  *  a))  \mleq{}  m
\mvdash{}  False


By

---

Latex:
Omega1Aux  Auto

---

Home Index