---

Step * 1 1 1 1 1 of Lemma int_is_mono


1. 0 ∈ ℤ
2. v : ℤ
3. v < 0
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
BY
{ ((Subst ⌜x ~ (x + 1) - 1⌝ 0⋅ THENA Auto)
   THEN (Subst ⌜v ~ (v + 1) - 1⌝ 0⋅ THENA Auto)
   THEN SqLeCD
   THEN Try (Complete (Auto))
   THEN BHyp 7
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst  \mkleeneopen{}x  \msim{}  (x  +  1)  -  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}v  \msim{}  (v  +  1)  -  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  SqLeCD
  THEN  Try  (Complete  (Auto))
  THEN  BHyp  7
  THEN  Auto)

---

Home Index