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