---

Step * of Lemma not-equal-2

∀x,y:ℤ.  uiff(¬(x = y ∈ ℤ);((1 + x) ≤ y) ∨ ((1 + y) ≤ x))
BY
{ TACTIC:((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. x : ℤ@i
2. y : ℤ@i
3. ¬(x = y ∈ ℤ)
⊢ ((1 + x) ≤ y) ∨ ((1 + y) ≤ x)

2
1. x : ℤ@i
2. y : ℤ@i
3. ((1 + x) ≤ y) ∨ ((1 + y) ≤ x)
⊢ ¬(x = y ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(\mneg{}(x  =  y);((1  +  x)  \mleq{}  y)  \mvee{}  ((1  +  y)  \mleq{}  x))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index