Metamath Proof Explorer


Theorem taylth

Description: Taylor's theorem. The Taylor polynomial of a N -times differentiable function is such that the error term goes to zero faster than ( x - B ) ^ N . This is Metamath 100 proof #35. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses taylth.f
|- ( ph -> F : A --> RR )
taylth.a
|- ( ph -> A C_ RR )
taylth.d
|- ( ph -> dom ( ( RR Dn F ) ` N ) = A )
taylth.n
|- ( ph -> N e. NN )
taylth.b
|- ( ph -> B e. A )
taylth.t
|- T = ( N ( RR Tayl F ) B )
taylth.r
|- R = ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) )
Assertion taylth
|- ( ph -> 0 e. ( R limCC B ) )

Proof

Step Hyp Ref Expression
1 taylth.f
 |-  ( ph -> F : A --> RR )
2 taylth.a
 |-  ( ph -> A C_ RR )
3 taylth.d
 |-  ( ph -> dom ( ( RR Dn F ) ` N ) = A )
4 taylth.n
 |-  ( ph -> N e. NN )
5 taylth.b
 |-  ( ph -> B e. A )
6 taylth.t
 |-  T = ( N ( RR Tayl F ) B )
7 taylth.r
 |-  R = ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) )
8 reelprrecn
 |-  RR e. { RR , CC }
9 8 a1i
 |-  ( ph -> RR e. { RR , CC } )
10 ax-resscn
 |-  RR C_ CC
11 fss
 |-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
12 1 10 11 sylancl
 |-  ( ph -> F : A --> CC )
13 1 adantr
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> F : A --> RR )
14 2 adantr
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> A C_ RR )
15 3 adantr
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> dom ( ( RR Dn F ) ` N ) = A )
16 4 adantr
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> N e. NN )
17 5 adantr
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> B e. A )
18 simprl
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> m e. ( 1 ..^ N ) )
19 simprr
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) )
20 fveq2
 |-  ( y = x -> ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - m ) ) ` x ) )
21 fveq2
 |-  ( y = x -> ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) )
22 20 21 oveq12d
 |-  ( y = x -> ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) = ( ( ( ( RR Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) )
23 oveq1
 |-  ( y = x -> ( y - B ) = ( x - B ) )
24 23 oveq1d
 |-  ( y = x -> ( ( y - B ) ^ m ) = ( ( x - B ) ^ m ) )
25 22 24 oveq12d
 |-  ( y = x -> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) = ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) )
26 25 cbvmptv
 |-  ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) )
27 26 oveq1i
 |-  ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B )
28 19 27 eleqtrdi
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) )
29 13 14 15 16 17 6 18 28 taylthlem2
 |-  ( ( ph /\ ( m e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - m ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` y ) ) / ( ( y - B ) ^ m ) ) ) limCC B ) ) ) -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( m + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( m + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( m + 1 ) ) ) ) limCC B ) )
30 9 12 2 3 4 5 6 7 29 taylthlem1
 |-  ( ph -> 0 e. ( R limCC B ) )