---

Step * 1 2 of Lemma nat-retractible


∀x:Base. ((if (x) < (0)  then ⊥  else x)↓ ⇒ (x ∈ ℕ))
BY
{ TACTIC:(RepeatFor 2 ((D 0 THENA Auto)) THEN HasValueD (-1)) }

1
1. x : Base
2. (if (x) < (0)  then ⊥  else x)↓
3. x ∈ ℤ
4. 0 ∈ ℤ
⊢ x ∈ ℕ

---

Latex:

---

Latex:

\mforall{}x:Base.  ((if  (x)  <  (0)    then  \mbot{}    else  x)\mdownarrow{}  {}\mRightarrow{}  (x  \mmember{}  \mBbbN{}))


By

---

Latex:
TACTIC:(RepeatFor  2  ((D  0  THENA  Auto))  THEN  HasValueD  (-1))

---

Home Index