---

Step * of Lemma test-add-member-elim

∀x,y:Base. ∀d:ℤ.  ((x + y ~ d) ⇒ (0 < x ∨ (x ≤ 0)))
BY
{ ((UnivCD THENA Auto) THEN Assert ⌜x ∈ ℤ⌝⋅) }

1
.....assertion..... 
1. x : Base@i
2. y : Base@i
3. d : ℤ@i
4. x + y ~ d@i
⊢ x ∈ ℤ

2
1. x : Base@i
2. y : Base@i
3. d : ℤ@i
4. x + y ~ d@i
5. x ∈ ℤ
⊢ 0 < x ∨ (x ≤ 0)

---

Latex:

---

Latex:
\mforall{}x,y:Base.  \mforall{}d:\mBbbZ{}.    ((x  +  y  \msim{}  d)  {}\mRightarrow{}  (0  <  x  \mvee{}  (x  \mleq{}  0)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Assert  \mkleeneopen{}x  \mmember{}  \mBbbZ{}\mkleeneclose{}\mcdot{})

---

Home Index