---

Step * 1 1 of Lemma absval_elim


1. [P] : ℤ ⟶ ℙ
2. x : ℕ
3. P |x|
⊢ P x
BY
{ (MoveToConcl 3 THEN (RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  3  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index