Proof of Nuprl Lemma : fun-converges-to-derivative

Step * 2 1 1 1 1 3 of Lemma fun-converges-to-derivative

1. I : Interval
2. iproper(I)
3. f : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. F : I ⟶ℝ
6. G : I ⟶ℝ
7. ∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y]))
8. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
9. lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
10. ∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I
11. r : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))
14. lim n→∞.r_∫^-x f'[n;t] dt = λx.r_∫^-x G[t] dt for x ∈ I
15. λx.G[x] ∈ {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))}
16. d(r_∫^-x G[t] dt)/dx = λx.G[x] on I
17. ∀f1,f2:ℕ ⟶ I ⟶ℝ. ∀g1,g2:I ⟶ℝ.
      (lim n→∞.f1[n;x] = λy.g1[y] for x ∈ I
      ⇒ lim n→∞.f2[n;x] = λy.g2[y] for x ∈ I
      ⇒ lim n→∞.f1[n;x] - f2[n;x] = λy.g1[y] - g2[y] for x ∈ I)
18. lim n→∞.f[n;x] - r_∫^-x f'[n;t] dt = λy.F[y] - r_∫^-y G[t] dt for x ∈ I
⊢ ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . (F[x] = (r_∫^-x G[t] dt + c))
BY
{ ((Assert ∀n:ℕ. (r_∫^- f'[n;t] dt ∈ I ⟶ℝ) BY
          (Auto
           THEN InstLemma `integrate_wf` [⌜I⌝;⌜r⌝;⌜λ₂x.f'[n;x]⌝]⋅
           THEN Auto
           THEN MemTypeCD
           THEN Reduce 0
           THEN Auto))

   THEN Assert ⌜∀n:ℕ. ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . ((f[n;x] - r_∫^- f'[n;t] dt x) = c)⌝⋅

   ) }

1
.....assertion.....
1. I : Interval
2. iproper(I)
3. f : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. F : I ⟶ℝ
6. G : I ⟶ℝ
7. ∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y]))
8. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
9. lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
10. ∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I
11. r : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))
14. lim n→∞.r_∫^-x f'[n;t] dt = λx.r_∫^-x G[t] dt for x ∈ I
15. λx.G[x] ∈ {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))}
16. d(r_∫^-x G[t] dt)/dx = λx.G[x] on I
17. ∀f1,f2:ℕ ⟶ I ⟶ℝ. ∀g1,g2:I ⟶ℝ.
      (lim n→∞.f1[n;x] = λy.g1[y] for x ∈ I
      ⇒ lim n→∞.f2[n;x] = λy.g2[y] for x ∈ I
      ⇒ lim n→∞.f1[n;x] - f2[n;x] = λy.g1[y] - g2[y] for x ∈ I)
18. lim n→∞.f[n;x] - r_∫^-x f'[n;t] dt = λy.F[y] - r_∫^-y G[t] dt for x ∈ I
19. ∀n:ℕ. (r_∫^- f'[n;t] dt ∈ I ⟶ℝ)
⊢ ∀n:ℕ. ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . ((f[n;x] - r_∫^- f'[n;t] dt x) = c)

2
1. I : Interval
2. iproper(I)
3. f : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. F : I ⟶ℝ
6. G : I ⟶ℝ
7. ∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (f'[n;x] = f'[n;y]))
8. lim n→∞.f[n;x] = λy.F[y] for x ∈ I
9. lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
10. ∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I
11. r : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (G[x] = G[y]))
14. lim n→∞.r_∫^-x f'[n;t] dt = λx.r_∫^-x G[t] dt for x ∈ I
15. λx.G[x] ∈ {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))}
16. d(r_∫^-x G[t] dt)/dx = λx.G[x] on I
17. ∀f1,f2:ℕ ⟶ I ⟶ℝ. ∀g1,g2:I ⟶ℝ.
      (lim n→∞.f1[n;x] = λy.g1[y] for x ∈ I
      ⇒ lim n→∞.f2[n;x] = λy.g2[y] for x ∈ I
      ⇒ lim n→∞.f1[n;x] - f2[n;x] = λy.g1[y] - g2[y] for x ∈ I)
18. lim n→∞.f[n;x] - r_∫^-x f'[n;t] dt = λy.F[y] - r_∫^-y G[t] dt for x ∈ I
19. ∀n:ℕ. (r_∫^- f'[n;t] dt ∈ I ⟶ℝ)
20. ∀n:ℕ. ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . ((f[n;x] - r_∫^- f'[n;t] dt x) = c)
⊢ ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . (F[x] = (r_∫^-x G[t] dt + c))

Latex:

Latex:
1. I : Interval 2. iproper(I) 3. f : \mBbbN{} {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{} 4. f' : \mBbbN{} {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{} 5. F : I {}\mrightarrow{}\mBbbR{} 6. G : I {}\mrightarrow{}\mBbbR{} 7. \mforall{}n:\mBbbN{}. \mforall{}x,y:\{a:\mBbbR{}| a \mmember{} I\} . ((x = y) {}\mRightarrow{} (f'[n;x] = f'[n;y])) 8. lim n\mrightarrow{}\minfty{}.f[n;x] = \mlambda{}y.F[y] for x \mmember{} I 9. lim n\mrightarrow{}\minfty{}.f'[n;x] = \mlambda{}y.G[y] for x \mmember{} I 10. \mforall{}n:\mBbbN{}. d(f[n;x])/dx = \mlambda{}x.f'[n;x] on I 11. r : \mBbbR{} 12. r \mmember{} I 13. \mforall{}x,y:\{a:\mBbbR{}| a \mmember{} I\} . ((x = y) {}\mRightarrow{} (G[x] = G[y])) 14. lim n\mrightarrow{}\minfty{}.r\_\mint{}\msupminus{}x f'[n;t] dt = \mlambda{}x.r\_\mint{}\msupminus{}x G[t] dt for x \mmember{} I 15. \mlambda{}x.G[x] \mmember{} \{f:I {}\mrightarrow{}\mBbbR{}| \mforall{}x,y:\{a:\mBbbR{}| a \mmember{} I\} . ((x = y) {}\mRightarrow{} ((f x) = (f y)))\} 16. d(r\_\mint{}\msupminus{}x G[t] dt)/dx = \mlambda{}x.G[x] on I 17. \mforall{}f1,f2:\mBbbN{} {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{}. \mforall{}g1,g2:I {}\mrightarrow{}\mBbbR{}. (lim n\mrightarrow{}\minfty{}.f1[n;x] = \mlambda{}y.g1[y] for x \mmember{} I {}\mRightarrow{} lim n\mrightarrow{}\minfty{}.f2[n;x] = \mlambda{}y.g2[y] for x \mmember{} I {}\mRightarrow{} lim n\mrightarrow{}\minfty{}.f1[n;x] - f2[n;x] = \mlambda{}y.g1[y] - g2[y] for x \mmember{} I) 18. lim n\mrightarrow{}\minfty{}.f[n;x] - r\_\mint{}\msupminus{}x f'[n;t] dt = \mlambda{}y.F[y] - r\_\mint{}\msupminus{}y G[t] dt for x \mmember{} I \mvdash{} \mexists{}c:\mBbbR{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . (F[x] = (r\_\mint{}\msupminus{}x G[t] dt + c)) By Latex: ((Assert \mforall{}n:\mBbbN{}. (r\_\mint{}\msupminus{} f'[n;t] dt \mmember{} I {}\mrightarrow{}\mBbbR{}) BY (Auto THEN InstLemma `integrate\_wf` [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f'[n;x]\mkleeneclose{}]\mcdot{} THEN Auto THEN MemTypeCD THEN Reduce 0 THEN Auto)) THEN Assert \mkleeneopen{}\mforall{}n:\mBbbN{}. \mexists{}c:\mBbbR{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . ((f[n;x] - r\_\mint{}\msupminus{} f'[n;t] dt x) = c)\mkleeneclose{}\mcdot{} ) Home Index