Step
*
1
1
1
1
2
1
of Lemma
rnonneg-rmul
1. x : ℝ
2. y : ℝ
3. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))
4. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (y m)))
5. n : ℕ+
6. N1 : ℕ+
7. ∀m:{N1...}. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m)))
8. N : ℕ+
9. ∀m:{N...}. (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
10. m : {imax(imax(N;N1);n)...}
11. (((-2) * m) * m) ≤ (n * (x m) * (y m))
12. 1 ≤ imax(N;N1)
13. 1 ≤ imax(imax(N;N1);n)
14. m ∈ ℕ+
⊢ ((2 * m) * (-2) * m) ≤ ((n * (x m) * (y m)) - n * ((x m) * (y m) rem 2 * m))
BY
{ Assert ⌜(n * ((x m) * (y m) rem 2 * m)) ≤ ((2 * m) * m)⌝⋅ }
1
.....assertion.....
1. x : ℝ
2. y : ℝ
3. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))
4. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (y m)))
5. n : ℕ+
6. N1 : ℕ+
7. ∀m:{N1...}. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m)))
8. N : ℕ+
9. ∀m:{N...}. (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
10. m : {imax(imax(N;N1);n)...}
11. (((-2) * m) * m) ≤ (n * (x m) * (y m))
12. 1 ≤ imax(N;N1)
13. 1 ≤ imax(imax(N;N1);n)
14. m ∈ ℕ+
⊢ (n * ((x m) * (y m) rem 2 * m)) ≤ ((2 * m) * m)
2
1. x : ℝ
2. y : ℝ
3. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))
4. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (y m)))
5. n : ℕ+
6. N1 : ℕ+
7. ∀m:{N1...}. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m)))
8. N : ℕ+
9. ∀m:{N...}. (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
10. m : {imax(imax(N;N1);n)...}
11. (((-2) * m) * m) ≤ (n * (x m) * (y m))
12. 1 ≤ imax(N;N1)
13. 1 ≤ imax(imax(N;N1);n)
14. m ∈ ℕ+
15. (n * ((x m) * (y m) rem 2 * m)) ≤ ((2 * m) * m)
⊢ ((2 * m) * (-2) * m) ≤ ((n * (x m) * (y m)) - n * ((x m) * (y m) rem 2 * m))
Latex:
Latex:
1. x : \mBbbR{}
2. y : \mBbbR{}
3. \mforall{}n:\mBbbN{}\msupplus{}. \mexists{}N:\mBbbN{}\msupplus{}. \mforall{}m:\{N...\}. (((-2) * m) \mleq{} (n * (x m)))
4. \mforall{}n:\mBbbN{}\msupplus{}. \mexists{}N:\mBbbN{}\msupplus{}. \mforall{}m:\{N...\}. (((-2) * m) \mleq{} (n * (y m)))
5. n : \mBbbN{}\msupplus{}
6. N1 : \mBbbN{}\msupplus{}
7. \mforall{}m:\{N1...\}. (((-2) * m) \mleq{} (((2 * canonical-bound(y)) * n) * (x m)))
8. N : \mBbbN{}\msupplus{}
9. \mforall{}m:\{N...\}. (((-2) * m) \mleq{} (((2 * canonical-bound(x)) * n) * (y m)))
10. m : \{imax(imax(N;N1);n)...\}
11. (((-2) * m) * m) \mleq{} (n * (x m) * (y m))
12. 1 \mleq{} imax(N;N1)
13. 1 \mleq{} imax(imax(N;N1);n)
14. m \mmember{} \mBbbN{}\msupplus{}
\mvdash{} ((2 * m) * (-2) * m) \mleq{} ((n * (x m) * (y m)) - n * ((x m) * (y m) rem 2 * m))
By
Latex:
Assert \mkleeneopen{}(n * ((x m) * (y m) rem 2 * m)) \mleq{} ((2 * m) * m)\mkleeneclose{}\mcdot{}
Home
Index