Step
*
of Lemma
absval_wf
∀[x:ℤ]. (|x| ∈ ℕ)
BY
{ ((D 0 THENA Auto) THEN RWO "absval_unfold2" 0 THEN Auto) }
1
1. x : ℤ
2. 0 ∈ ℤ
3. x ∈ ℤ
4. ¬0 < x
⊢ -x ∈ ℕ
Latex:
Latex:
\mforall{}[x:\mBbbZ{}]. (|x| \mmember{} \mBbbN{})
By
Latex:
((D 0 THENA Auto) THEN RWO "absval\_unfold2" 0 THEN Auto)
Home
Index