---

Step * 1 1 1 2 of Lemma int_is_mono


1. 0 ∈ ℤ
2. v : ℤ
3. x : ℤ
4. x ≤ 0
⊢ 0 ≤ x
BY
{ (MoveToConcl (-1) THEN UseWitness ⌜λ%.Ax⌝⋅ THEN WeakIntInd (-1) THEN (MemCD⋅ THENA Auto)) }

1
.....subterm..... T:t
1:n
1. 0 ∈ ℤ
2. v : ℤ
3. x : ℤ
4. x < 0
5. λ%.Ax ∈ (x + 1 ≤ 0) ⇒ (0 ≤ x + 1)
6. x ≤ 0
⊢ Ax ∈ 0 ≤ x

2
.....subterm..... T:t
1:n
1. 0 ∈ ℤ
2. v : ℤ
3. x : ℤ
4. 0 ≤ 0
⊢ Ax ∈ 0 ≤ 0

3
.....subterm..... T:t
1:n
1. 0 ∈ ℤ
2. v : ℤ
3. x : ℤ
4. 0 < x
5. λ%.Ax ∈ (x - 1 ≤ 0) ⇒ (0 ≤ x - 1)
6. x ≤ 0
⊢ Ax ∈ 0 ≤ x

---

Latex:

---

Latex:

1.  0  \mmember{}  \mBbbZ{}
2.  v  :  \mBbbZ{}
3.  x  :  \mBbbZ{}
4.  x  \mleq{}  0
\mvdash{}  0  \mleq{}  x


By

---

Latex:
(MoveToConcl  (-1)  THEN  UseWitness  \mkleeneopen{}\mlambda{}\%.Ax\mkleeneclose{}\mcdot{}  THEN  WeakIntInd  (-1)  THEN  (MemCD\mcdot{}  THENA  Auto))

---

Home Index