---

Step * of Lemma absval_elim

∀[P:ℤ ⟶ ℙ]. (∀x:ℤ. P[|x|] ⇐⇒ ∀x:ℕ. P[x])
BY
{ ((Unfolds ``guard so_apply`` 0 THEN GenUnivCD) THENA Auto) }

1
1. [P] : ℤ ⟶ ℙ
2. ∀x:ℤ. (P |x|)
3. x : ℕ
⊢ P x

2
1. [P] : ℤ ⟶ ℙ
2. ∀x:ℕ. (P x)
3. x : ℤ
⊢ P |x|

---

Latex:

---

Latex:
\mforall{}[P:\mBbbZ{}  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}x:\mBbbZ{}.  P[|x|]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:\mBbbN{}.  P[x])


By

---

Latex:
((Unfolds  ``guard  so\_apply``  0  THEN  GenUnivCD)  THENA  Auto)

---

Home Index