Step
*
1
1
1
1
2
2
of Lemma
absval_cases
.....wf..... 
1. x : ℤ
2. y : ℕ
3. 0 < x
⊢ x = y ∈ ℤ ∈ ℙ
BY
{ Auto }
Latex:
Latex:
.....wf..... 
1.  x  :  \mBbbZ{}
2.  y  :  \mBbbN{}
3.  0  <  x
\mvdash{}  x  =  y  \mmember{}  \mBbbP{}
By
Latex:
Auto
Home
Index