---

Step * 1 1 of Lemma int_is_mono


1. x : ℤ
2. y : Base
3. x ≤ y
4. (y)↓
5. x + 0 ≤ y + 0
6. (y + 0)↓
7. y ∈ ℤ
8. 0 ∈ ℤ
⊢ y ≤ x
BY
{ (MoveToConcl 3 THEN GenConclAtAddr [1;2] THEN ThinVar `y' THEN MoveToConcl 1) }

1
1. 0 ∈ ℤ
2. v : ℤ
⊢ ∀x:ℤ. ((x ≤ v) ⇒ (v ≤ x))

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  Base
3.  x  \mleq{}  y
4.  (y)\mdownarrow{}
5.  x  +  0  \mleq{}  y  +  0
6.  (y  +  0)\mdownarrow{}
7.  y  \mmember{}  \mBbbZ{}
8.  0  \mmember{}  \mBbbZ{}
\mvdash{}  y  \mleq{}  x


By

---

Latex:
(MoveToConcl  3  THEN  GenConclAtAddr  [1;2]  THEN  ThinVar  `y'  THEN  MoveToConcl  1)

---

Home Index