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 ) )