Step
*
of Lemma
rabs-rminus
∀[x:ℝ]. (|-(x)| = |x| ∈ ℝ)
BY
{ (Auto THEN EqTypeCD THEN Auto) }
1
1. x : ℝ
⊢ |-(x)| = |x| ∈ (ℕ
+
⟶ ℤ)
Latex:
Latex:
\mforall{}[x:\mBbbR{}]. (|-(x)| = |x|)
By
Latex:
(Auto THEN EqTypeCD THEN Auto)
Home
Index