---

Step * 1 1 1 3 of Lemma int_is_mono


1. 0 ∈ ℤ
2. v : ℤ
3. 0 < v
4. λx,%. Ax ∈ ∀x:ℤ. ((x ≤ v - 1) ⇒ (v - 1 ≤ x))
5. x : ℤ
6. x ≤ v
⊢ v ≤ x
BY
{ (Assert ⌜∀x:ℤ. ((x ≤ v - 1) ⇒ (v - 1 ≤ x))⌝⋅ THENA (UseWitness ⌜λx,%. Ax⌝⋅ THEN Auto)⋅) }

1
1. 0 ∈ ℤ
2. v : ℤ
3. 0 < v
4. λx,%. Ax ∈ ∀x:ℤ. ((x ≤ v - 1) ⇒ (v - 1 ≤ x))
5. x : ℤ
6. x ≤ v
7. ∀x:ℤ. ((x ≤ v - 1) ⇒ (v - 1 ≤ x))
⊢ v ≤ x

---

Latex:

---

Latex:

1.  0  \mmember{}  \mBbbZ{}
2.  v  :  \mBbbZ{}
3.  0  <  v
4.  \mlambda{}x,\%.  Ax  \mmember{}  \mforall{}x:\mBbbZ{}.  ((x  \mleq{}  v  -  1)  {}\mRightarrow{}  (v  -  1  \mleq{}  x))
5.  x  :  \mBbbZ{}
6.  x  \mleq{}  v
\mvdash{}  v  \mleq{}  x


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}x:\mBbbZ{}.  ((x  \mleq{}  v  -  1)  {}\mRightarrow{}  (v  -  1  \mleq{}  x))\mkleeneclose{}\mcdot{}  THENA  (UseWitness  \mkleeneopen{}\mlambda{}x,\%.  Ax\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index