---

Step * 1 of Lemma absval_elim


1. [P] : ℤ ⟶ ℙ
2. ∀x:ℤ. (P |x|)
3. x : ℕ
⊢ P x
BY
{ (DTerm ⌜x⌝ 2 THENA Auto) }

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

---

Latex:

---

Latex:

1.  [P]  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}x:\mBbbZ{}.  (P  |x|)
3.  x  :  \mBbbN{}
\mvdash{}  P  x


By

---

Latex:
(DTerm  \mkleeneopen{}x\mkleeneclose{}  2  THENA  Auto)

---

Home Index