Step
*
1
1
1
1
1
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. (N ≤ imax(imax(N;N1);n)) ∧ (N1 ≤ imax(imax(N;N1);n))
12. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m))) ∧ (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
⊢ (((-2) * m) * m) ≤ (n * (x m) * (y m))
BY
{ ((Decide ⌜0 ≤ (x m)⌝⋅ THENA Auto) THEN (Decide ⌜0 ≤ (y m)⌝⋅ THENA Auto)) }
1
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. (N ≤ imax(imax(N;N1);n)) ∧ (N1 ≤ imax(imax(N;N1);n))
12. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m))) ∧ (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
13. 0 ≤ (x m)
14. 0 ≤ (y m)
⊢ (((-2) * m) * m) ≤ (n * (x m) * (y 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. (N ≤ imax(imax(N;N1);n)) ∧ (N1 ≤ imax(imax(N;N1);n))
12. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m))) ∧ (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
13. 0 ≤ (x m)
14. ¬(0 ≤ (y m))
⊢ (((-2) * m) * m) ≤ (n * (x m) * (y m))
3
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. (N ≤ imax(imax(N;N1);n)) ∧ (N1 ≤ imax(imax(N;N1);n))
12. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m))) ∧ (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
13. ¬(0 ≤ (x m))
14. 0 ≤ (y m)
⊢ (((-2) * m) * m) ≤ (n * (x m) * (y m))
4
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. (N ≤ imax(imax(N;N1);n)) ∧ (N1 ≤ imax(imax(N;N1);n))
12. (((-2) * m) ≤ (((2 * canonical-bound(y)) * n) * (x m))) ∧ (((-2) * m) ≤ (((2 * canonical-bound(x)) * n) * (y m)))
13. ¬(0 ≤ (x m))
14. ¬(0 ≤ (y m))
⊢ (((-2) * m) * m) ≤ (n * (x m) * (y 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. (N \mleq{} imax(imax(N;N1);n)) \mwedge{} (N1 \mleq{} imax(imax(N;N1);n))
12. (((-2) * m) \mleq{} (((2 * canonical-bound(y)) * n) * (x m)))
\mwedge{} (((-2) * m) \mleq{} (((2 * canonical-bound(x)) * n) * (y m)))
\mvdash{} (((-2) * m) * m) \mleq{} (n * (x m) * (y m))
By
Latex:
((Decide \mkleeneopen{}0 \mleq{} (x m)\mkleeneclose{}\mcdot{} THENA Auto) THEN (Decide \mkleeneopen{}0 \mleq{} (y m)\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index