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


1. Interval
2. iproper(I)
3. : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. I ⟶ℝ
6. 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. : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝa ∈ I} .  ((x y)  (G[x] G[y]))
14. lim n→∞.r_∫-f'[n;t] dt = λx.r_∫-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_∫-G[t] dt)/dx = λx.G[x] on I
17. : ℝ
18. rfun-eq(I;λx.F[x];λx.(r_∫-G[t] dt c))
19. d(r_∫-G[t] dt c)/dx = λx.G[x] r0 on I
⊢ d(F[x])/dx = λx.G[x] on I
BY
((Assert λx.((r_∫- G[t] dt x) c) ∈ I ⟶ℝ BY
          Auto)
   THEN RepUR ``integrate`` -1
   THEN DerivativeFunctionality (-2)
   THEN Auto) }

1
1. Interval
2. iproper(I)
3. : ℕ ⟶ I ⟶ℝ
4. f' : ℕ ⟶ I ⟶ℝ
5. I ⟶ℝ
6. 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. : ℝ
12. r ∈ I
13. ∀x,y:{a:ℝa ∈ I} .  ((x y)  (G[x] G[y]))
14. lim n→∞.r_∫-f'[n;t] dt = λx.r_∫-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_∫-G[t] dt)/dx = λx.G[x] on I
17. : ℝ
18. rfun-eq(I;λx.F[x];λx.(r_∫-G[t] dt c))
19. d(r_∫-G[t] dt c)/dx = λx.G[x] r0 on I
20. λx.(r_∫-G[t] dt c) ∈ I ⟶ℝ
21. {x:ℝx ∈ I} 
⊢ (r_∫-G[t] dt c) F[x]


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.  c  :  \mBbbR{}
18.  rfun-eq(I;\mlambda{}x.F[x];\mlambda{}x.(r\_\mint{}\msupminus{}x  G[t]  dt  +  c))
19.  d(r\_\mint{}\msupminus{}x  G[t]  dt  +  c)/dx  =  \mlambda{}x.G[x]  +  r0  on  I
\mvdash{}  d(F[x])/dx  =  \mlambda{}x.G[x]  on  I


By


Latex:
((Assert  \mlambda{}x.((r\_\mint{}\msupminus{}  G[t]  dt  x)  +  c)  \mmember{}  I  {}\mrightarrow{}\mBbbR{}  BY
                Auto)
  THEN  RepUR  ``integrate``  -1
  THEN  DerivativeFunctionality  (-2)
  THEN  Auto)




Home Index