Proof of Nuprl Lemma : differentiable-continuous

Step * 1 1 1 1 of Lemma differentiable-continuous

1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. d(f[x])/dx = λx.g[x] on I
6. g[x] (proper)continuous for x ∈ I
7. m : {m:ℕ⁺| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))}
8. n : ℕ⁺
9. i-approx(I;m) ⊆ I
10. M : ℕ⁺
11. |g x|(x∈i-approx(I;m)) ≤ r(M)
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|g[x] * (y - x)| ≤ (r(M) * |y - x|)))
⊢ ∃d:ℝ [((r0 < d)
       ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))]
BY

{ xxx(OnMaybeHyp 5 (\h. (Unfold `derivative` h THEN (InstHyp [⌜1⌝;⌜m⌝] h⋅ THENA Auto) THEN D -1))

      THEN (Assert ∀y,x:ℝ.
                     ((x ∈ i-approx(I;m))
                     ⇒ (y ∈ i-approx(I;m))
                     ⇒ (|x - y| ≤ del)
                     ⇒ (|f[x] - f[y]| ≤ (r(M + 1) * |y - x|))) BY
                  ((ParallelOp -3 THEN ParallelLast')
                   THEN Auto
                   THEN (InstHyp [⌜y⌝;⌜x⌝] (-7)⋅ THENA Auto)

                   THEN (InstLemma `r-triangle-inequality` [⌜f[x] - f[y] - g[y] * (x - y)⌝;⌜g[y] * (x - y)⌝]⋅

                         THENA Auto
                         )
                   THEN (RWO "-2 -3" (-1) THENA Auto)
                   THEN (RW (AddrC [2;2] (LemmaC `rabs-difference-symmetry`)) 0 THENA Auto)
                   THEN MoveToConcl (-1)

                   THEN GenConclTerms Auto [⌜|x - y|⌝;⌜f[x] - f[y]⌝;⌜g[y] * (x - y)⌝]⋅

                   THEN All Thin
                   THEN (D 0 THENA Auto)
                   THEN (nRNorm (-1) THENA Auto)
                   THEN (RWO "-1" 0 THEN Auto)
                   THEN (RWO "radd-int<" 0 THENA Auto)
                   THEN (RWO "rmul-distrib2" 0 THENA Auto)
                   THEN (GenConclTerm ⌜r(M) * v⌝⋅ THEN Auto)
                   THEN nRNorm 0
                   THEN Auto))
      )xxx }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. ∀k:ℕ⁺. ∀n:{n:ℕ⁺| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} .
     (∃del:ℝ [((r0 < del)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;n))
                  ⇒ (y ∈ i-approx(I;n))
                  ⇒ (|y - x| ≤ del)
                  ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))])
6. g[x] (proper)continuous for x ∈ I
7. m : {m:ℕ⁺| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))}
8. n : ℕ⁺
9. i-approx(I;m) ⊆ I
10. M : ℕ⁺
11. |g x|(x∈i-approx(I;m)) ≤ r(M)
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|g[x] * (y - x)| ≤ (r(M) * |y - x|)))
13. del : ℝ
14. [%18] : (r0 < del)
∧ (∀x,y:ℝ.
     ((x ∈ i-approx(I;m))
     ⇒ (y ∈ i-approx(I;m))
     ⇒ (|y - x| ≤ del)
     ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r1) * |y - x|))))
15. ∀y,x:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ del) ⇒ (|f[x] - f[y]| ≤ (r(M + 1) * |y - x|)))
⊢ ∃d:ℝ [((r0 < d)
       ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))]

Latex:

Latex:
1. I : Interval 2. f : I {}\mrightarrow{}\mBbbR{} 3. g : I {}\mrightarrow{}\mBbbR{} 4. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . ((x = y) {}\mRightarrow{} (g[x] = g[y])) 5. d(f[x])/dx = \mlambda{}x.g[x] on I 6. g[x] (proper)continuous for x \mmember{} I 7. m : \{m:\mBbbN{}\msupplus{}| icompact(i-approx(I;m)) \mwedge{} iproper(i-approx(I;m))\} 8. n : \mBbbN{}\msupplus{} 9. i-approx(I;m) \msubseteq{} I 10. M : \mBbbN{}\msupplus{} 11. |g x|(x\mmember{}i-approx(I;m)) \mleq{} r(M) 12. \mforall{}x,y:\mBbbR{}. ((x \mmember{} i-approx(I;m)) {}\mRightarrow{} (y \mmember{} i-approx(I;m)) {}\mRightarrow{} (|g[x] * (y - x)| \mleq{} (r(M) * |y - x|))) \mvdash{} \mexists{}d:\mBbbR{} [((r0 < d) \mwedge{} (\mforall{}x,y:\mBbbR{}. ((x \mmember{} i-approx(I;m)) {}\mRightarrow{} (y \mmember{} i-approx(I;m)) {}\mRightarrow{} (|x - y| \mleq{} d) {}\mRightarrow{} (|f[x] - f[y]| \mleq{} (r1/r(n))))))] By Latex: xxx(OnMaybeHyp 5 (\mbackslash{}h. (Unfold `derivative` h THEN (InstHyp [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}] h\mcdot{} THENA Auto) THEN D -1)) THEN (Assert \mforall{}y,x:\mBbbR{}. ((x \mmember{} i-approx(I;m)) {}\mRightarrow{} (y \mmember{} i-approx(I;m)) {}\mRightarrow{} (|x - y| \mleq{} del) {}\mRightarrow{} (|f[x] - f[y]| \mleq{} (r(M + 1) * |y - x|))) BY ((ParallelOp -3 THEN ParallelLast') THEN Auto THEN (InstHyp [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}] (-7)\mcdot{} THENA Auto) THEN (InstLemma `r-triangle-inequality` [\mkleeneopen{}f[x] - f[y] - g[y] * (x - y)\mkleeneclose{};\mkleeneopen{}g[y] * (x - y)\mkleeneclose{} ]\mcdot{} THENA Auto ) THEN (RWO "-2 -3" (-1) THENA Auto) THEN (RW (AddrC [2;2] (LemmaC `rabs-difference-symmetry`)) 0 THENA Auto) THEN MoveToConcl (-1) THEN GenConclTerms Auto [\mkleeneopen{}|x - y|\mkleeneclose{};\mkleeneopen{}f[x] - f[y]\mkleeneclose{};\mkleeneopen{}g[y] * (x - y)\mkleeneclose{}]\mcdot{} THEN All Thin THEN (D 0 THENA Auto) THEN (nRNorm (-1) THENA Auto) THEN (RWO "-1" 0 THEN Auto) THEN (RWO "radd-int<" 0 THENA Auto) THEN (RWO "rmul-distrib2" 0 THENA Auto) THEN (GenConclTerm \mkleeneopen{}r(M) * v\mkleeneclose{}\mcdot{} THEN Auto) THEN nRNorm 0 THEN Auto)) )xxx Home Index