Step
*
1
of Lemma
rabs-nonneg
1. x : ℝ
2. n : ℕ+@i
3. m : {1...}@i
⊢ ((-2) * m) ≤ (n * |x m|)
BY
{ (Assert 0 ≤ |x m| BY
EAuto 1) }
1
1. x : ℝ
2. n : ℕ+@i
3. m : {1...}@i
4. 0 ≤ |x m|
⊢ ((-2) * m) ≤ (n * |x m|)
Latex:
Latex:
1. x : \mBbbR{}
2. n : \mBbbN{}\msupplus{}@i
3. m : \{1...\}@i
\mvdash{} ((-2) * m) \mleq{} (n * |x m|)
By
Latex:
(Assert 0 \mleq{} |x m| BY
EAuto 1)
Home
Index