Proof of Nuprl Lemma : chain-rule

Step * 1 1 1 1 1 1 2 1 of Lemma chain-rule_0

1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : J ⟶ℝ
6. g' : J ⟶ℝ
7. f[x] (proper)continuous for x ∈ I
8. f'[x] (proper)continuous for x ∈ I
9. g'[x] (proper)continuous for x ∈ J
10. d(f[x])/dx = λx.f'[x] on I
11. d(g[x])/dx = λx.g'[x] on J
12. k : ℕ⁺
13. n : {n:ℕ⁺| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
14. m : {m:ℕ⁺| icompact(i-approx(J;m)) ∧ iproper(i-approx(J;m))}
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))
16. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
17. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
18. mc2 : g'[x] continuous for x ∈ i-approx(J;m)
19. ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b)
20. f' ∈ i-approx(I;n) ⟶ℝ
21. A : ℕ⁺
22. ∀r:ℝ. ((r ∈ i-approx(I;n)) ⇒ (|f'[r]| ≤ (r(A)/r(2 * k))))
23. g ∈ i-approx(J;m) ⟶ℝ
24. g' ∈ i-approx(J;m) ⟶ℝ
25. f ∈ i-approx(I;n) ⟶ℝ
26. d : ℝ
27. r0 < d
28. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ d)
      ⇒ (|g[f[y]] - g[f[x]] - g'[f[x]] * (f[y] - f[x])| ≤ ((r1/r(A)) * |f[y] - f[x]|)))
⊢ ∃del:ℝ [((r0 < del)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;n))
              ⇒ (y ∈ i-approx(I;n))
              ⇒ (|y - x| ≤ del)
              ⇒ (|g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]
BY
{ (Assert ∃B:ℕ⁺. ∀r:ℝ. ((r ∈ i-approx(J;m)) ⇒ (((r1/r(A)) + |g'[r]|) ≤ (r(B)/r(2 * k)))) BY
         (ExRepD
          THEN (InstLemma `r-bound-property` [⌜(r1/r(A)) + b⌝]⋅ THENA Auto)
          THEN With ⌜(2 * k) * r-bound((r1/r(A)) + b)⌝ (D 0)⋅
          THEN Auto
          THEN RWO "21" 0
          THEN Auto
          THEN RWO "-3" 0
          THEN Auto))⋅ }

1
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : J ⟶ℝ
6. g' : J ⟶ℝ
7. f[x] (proper)continuous for x ∈ I
8. f'[x] (proper)continuous for x ∈ I
9. g'[x] (proper)continuous for x ∈ J
10. d(f[x])/dx = λx.f'[x] on I
11. d(g[x])/dx = λx.g'[x] on J
12. k : ℕ⁺
13. n : {n:ℕ⁺| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
14. m : {m:ℕ⁺| icompact(i-approx(J;m)) ∧ iproper(i-approx(J;m))}
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))
16. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
17. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
18. mc2 : g'[x] continuous for x ∈ i-approx(J;m)
19. ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b)
20. f' ∈ i-approx(I;n) ⟶ℝ
21. A : ℕ⁺
22. ∀r:ℝ. ((r ∈ i-approx(I;n)) ⇒ (|f'[r]| ≤ (r(A)/r(2 * k))))
23. g ∈ i-approx(J;m) ⟶ℝ
24. g' ∈ i-approx(J;m) ⟶ℝ
25. f ∈ i-approx(I;n) ⟶ℝ
26. d : ℝ
27. r0 < d
28. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ d)
      ⇒ (|g[f[y]] - g[f[x]] - g'[f[x]] * (f[y] - f[x])| ≤ ((r1/r(A)) * |f[y] - f[x]|)))
29. ∃B:ℕ⁺. ∀r:ℝ. ((r ∈ i-approx(J;m)) ⇒ (((r1/r(A)) + |g'[r]|) ≤ (r(B)/r(2 * k))))
⊢ ∃del:ℝ [((r0 < del)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;n))
              ⇒ (y ∈ i-approx(I;n))
              ⇒ (|y - x| ≤ del)
              ⇒ (|g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]

Latex:

Latex:
1. I : Interval 2. J : Interval 3. f : I {}\mrightarrow{}\mBbbR{} 4. f' : I {}\mrightarrow{}\mBbbR{} 5. g : J {}\mrightarrow{}\mBbbR{} 6. g' : J {}\mrightarrow{}\mBbbR{} 7. f[x] (proper)continuous for x \mmember{} I 8. f'[x] (proper)continuous for x \mmember{} I 9. g'[x] (proper)continuous for x \mmember{} J 10. d(f[x])/dx = \mlambda{}x.f'[x] on I 11. d(g[x])/dx = \mlambda{}x.g'[x] on J 12. k : \mBbbN{}\msupplus{} 13. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))\} 14. m : \{m:\mBbbN{}\msupplus{}| icompact(i-approx(J;m)) \mwedge{} iproper(i-approx(J;m))\} 15. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;n)\} . (f[x] \mmember{} i-approx(J;m)) 16. mc1 : f'[x] continuous for x \mmember{} i-approx(I;n) 17. \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|f'[x]| \mleq{} a) 18. mc2 : g'[x] continuous for x \mmember{} i-approx(J;m) 19. \mexists{}b:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(J;m)\} ]. (|g'[x]| \mleq{} b) 20. f' \mmember{} i-approx(I;n) {}\mrightarrow{}\mBbbR{} 21. A : \mBbbN{}\msupplus{} 22. \mforall{}r:\mBbbR{}. ((r \mmember{} i-approx(I;n)) {}\mRightarrow{} (|f'[r]| \mleq{} (r(A)/r(2 * k)))) 23. g \mmember{} i-approx(J;m) {}\mrightarrow{}\mBbbR{} 24. g' \mmember{} i-approx(J;m) {}\mrightarrow{}\mBbbR{} 25. f \mmember{} i-approx(I;n) {}\mrightarrow{}\mBbbR{} 26. d : \mBbbR{} 27. r0 < d 28. \mforall{}x,y:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} (y \mmember{} i-approx(I;n)) {}\mRightarrow{} (|y - x| \mleq{} d) {}\mRightarrow{} (|g[f[y]] - g[f[x]] - g'[f[x]] * (f[y] - f[x])| \mleq{} ((r1/r(A)) * |f[y] - f[x]|))) \mvdash{} \mexists{}del:\mBbbR{} [((r0 < del) \mwedge{} (\mforall{}x,y:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} (y \mmember{} i-approx(I;n)) {}\mRightarrow{} (|y - x| \mleq{} del) {}\mRightarrow{} (|g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| \mleq{} ((r1/r(k)) * |y - x|)))))] By Latex: (Assert \mexists{}B:\mBbbN{}\msupplus{}. \mforall{}r:\mBbbR{}. ((r \mmember{} i-approx(J;m)) {}\mRightarrow{} (((r1/r(A)) + |g'[r]|) \mleq{} (r(B)/r(2 * k)))) BY (ExRepD THEN (InstLemma `r-bound-property` [\mkleeneopen{}(r1/r(A)) + b\mkleeneclose{}]\mcdot{} THENA Auto) THEN With \mkleeneopen{}(2 * k) * r-bound((r1/r(A)) + b)\mkleeneclose{} (D 0)\mcdot{} THEN Auto THEN RWO "21" 0 THEN Auto THEN RWO "-3" 0 THEN Auto))\mcdot{} Home Index