Step
*
1
1
1
1
2
1
of Lemma
converges-to-cosine
1. x : ℝ
2. k : ℕ+
3. n : {1...}
4. (2 * k) ≤ n
5. a : ℝ
6. |x - a| ≤ (r1/r(n))
7. |cosine(a) - (cosine(a) within 1/n)| ≤ (r1/r(n))
8. |cosine(x) - cosine(a)| ≤ (r1/r(n))
⊢ |cosine(x) - (cosine(a) within 1/n)| ≤ (r1/r(k))
BY
{ ((UseTriangleInequality [⌜cosine(a)⌝]⋅ THENM nRNorm 0) THEN Auto) }
Latex:
Latex:
1. x : \mBbbR{}
2. k : \mBbbN{}\msupplus{}
3. n : \{1...\}
4. (2 * k) \mleq{} n
5. a : \mBbbR{}
6. |x - a| \mleq{} (r1/r(n))
7. |cosine(a) - (cosine(a) within 1/n)| \mleq{} (r1/r(n))
8. |cosine(x) - cosine(a)| \mleq{} (r1/r(n))
\mvdash{} |cosine(x) - (cosine(a) within 1/n)| \mleq{} (r1/r(k))
By
Latex:
((UseTriangleInequality [\mkleeneopen{}cosine(a)\mkleeneclose{}]\mcdot{} THENM nRNorm 0) THEN Auto)
Home
Index