---

Step * 1 1 1 of Lemma int_is_mono


1. 0 ∈ ℤ
2. v : ℤ
⊢ ∀x:ℤ. ((x ≤ v) ⇒ (v ≤ x))
BY
{ (UseWitness ⌜λx,%. Ax⌝⋅
   THEN WeakIntInd (-1)
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN Try (TACTIC:(Unfold `member` 0 THEN Refine_axiomSqleEquality))
   THEN Try (Complete (Auto))) }

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

2
1. 0 ∈ ℤ
2. v : ℤ
3. x : ℤ
4. x ≤ 0
⊢ 0 ≤ x

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

---

Latex:

---

Latex:

1.  0  \mmember{}  \mBbbZ{}
2.  v  :  \mBbbZ{}
\mvdash{}  \mforall{}x:\mBbbZ{}.  ((x  \mleq{}  v)  {}\mRightarrow{}  (v  \mleq{}  x))


By

---

Latex:
(UseWitness  \mkleeneopen{}\mlambda{}x,\%.  Ax\mkleeneclose{}\mcdot{}
  THEN  WeakIntInd  (-1)
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  Try  (TACTIC:(Unfold  `member`  0  THEN  Refine\_axiomSqleEquality))
  THEN  Try  (Complete  (Auto)))

---

Home Index