Step
*
1
1
of Lemma
derivative-add
1. I : Interval
2. f1 : I ⟶ℝ
3. f2 : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
8. del : ℝ
9. r0 < del
10. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
11. d1 : ℝ
12. r0 < d1
13. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d1)
⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
14. r0 < rmin(del;d1)
15. x : ℝ
16. y : ℝ
17. x ∈ i-approx(I;n)
18. y ∈ i-approx(I;n)
19. |y - x| ≤ rmin(del;d1)
20. y ∈ I
21. x ∈ I
22. |f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)
23. |f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)
⊢ |(f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
BY
{ Assert ⌜((f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x))
= ((f1[y] - f1[x] - g1[x] * (y - x)) + (f2[y] - f2[x] - g2[x] * (y - x)))⌝⋅ }
1
.....assertion.....
1. I : Interval
2. f1 : I ⟶ℝ
3. f2 : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
8. del : ℝ
9. r0 < del
10. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
11. d1 : ℝ
12. r0 < d1
13. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d1)
⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
14. r0 < rmin(del;d1)
15. x : ℝ
16. y : ℝ
17. x ∈ i-approx(I;n)
18. y ∈ i-approx(I;n)
19. |y - x| ≤ rmin(del;d1)
20. y ∈ I
21. x ∈ I
22. |f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)
23. |f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)
⊢ ((f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x))
= ((f1[y] - f1[x] - g1[x] * (y - x)) + (f2[y] - f2[x] - g2[x] * (y - x)))
2
1. I : Interval
2. f1 : I ⟶ℝ
3. f2 : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
8. del : ℝ
9. r0 < del
10. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
11. d1 : ℝ
12. r0 < d1
13. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d1)
⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
14. r0 < rmin(del;d1)
15. x : ℝ
16. y : ℝ
17. x ∈ i-approx(I;n)
18. y ∈ i-approx(I;n)
19. |y - x| ≤ rmin(del;d1)
20. y ∈ I
21. x ∈ I
22. |f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)
23. |f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)
24. ((f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x))
= ((f1[y] - f1[x] - g1[x] * (y - x)) + (f2[y] - f2[x] - g2[x] * (y - x)))
⊢ |(f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
Latex:
Latex:
1. I : Interval
2. f1 : I {}\mrightarrow{}\mBbbR{}
3. f2 : I {}\mrightarrow{}\mBbbR{}
4. g1 : I {}\mrightarrow{}\mBbbR{}
5. g2 : I {}\mrightarrow{}\mBbbR{}
6. k : \mBbbN{}\msupplus{}
7. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))\}
8. del : \mBbbR{}
9. r0 < del
10. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} del)
{}\mRightarrow{} (|f2[y] - f2[x] - g2[x] * (y - x)| \mleq{} ((r1/r(2 * k)) * |y - x|)))
11. d1 : \mBbbR{}
12. r0 < d1
13. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} d1)
{}\mRightarrow{} (|f1[y] - f1[x] - g1[x] * (y - x)| \mleq{} ((r1/r(2 * k)) * |y - x|)))
14. r0 < rmin(del;d1)
15. x : \mBbbR{}
16. y : \mBbbR{}
17. x \mmember{} i-approx(I;n)
18. y \mmember{} i-approx(I;n)
19. |y - x| \mleq{} rmin(del;d1)
20. y \mmember{} I
21. x \mmember{} I
22. |f1[y] - f1[x] - g1[x] * (y - x)| \mleq{} ((r1/r(2 * k)) * |y - x|)
23. |f2[y] - f2[x] - g2[x] * (y - x)| \mleq{} ((r1/r(2 * k)) * |y - x|)
\mvdash{} |(f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x)| \mleq{} ((r1/r(k)) * |y - x|)
By
Latex:
Assert \mkleeneopen{}((f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x))
= ((f1[y] - f1[x] - g1[x] * (y - x)) + (f2[y] - f2[x] - g2[x] * (y - x)))\mkleeneclose{}\mcdot{}
Home
Index