Metamath Proof Explorer

Theorem dvntaylp

Description: The M -th derivative of the Taylor polynomial is the Taylor polynomial of the M -th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses dvntaylp.s 
|- ( ph -> S e. { RR , CC } )
dvntaylp.f 
|- ( ph -> F : A --> CC )
dvntaylp.a 
|- ( ph -> A C_ S )
dvntaylp.m 
|- ( ph -> M e. NN0 )
dvntaylp.n 
|- ( ph -> N e. NN0 )
dvntaylp.b 
|- ( ph -> B e. dom ( ( S Dn F ) ` ( N + M ) ) )
Assertion dvntaylp 
|- ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` M ) = ( N ( S Tayl ( ( S Dn F ) ` M ) ) B ) )

Proof

Step Hyp Ref Expression
1 dvntaylp.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvntaylp.f 
 |-  ( ph -> F : A --> CC )
3 dvntaylp.a 
 |-  ( ph -> A C_ S )
4 dvntaylp.m 
 |-  ( ph -> M e. NN0 )
5 dvntaylp.n 
 |-  ( ph -> N e. NN0 )
6 dvntaylp.b 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` ( N + M ) ) )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 4 7 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
9 eluzfz2b 
 |-  ( M e. ( ZZ>= ` 0 ) <-> M e. ( 0 ... M ) )
10 8 9 sylib 
 |-  ( ph -> M e. ( 0 ... M ) )
11 fveq2 
 |-  ( m = 0 -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` 0 ) )
12 fveq2 
 |-  ( m = 0 -> ( ( S Dn F ) ` m ) = ( ( S Dn F ) ` 0 ) )
13 12 oveq2d 
 |-  ( m = 0 -> ( S Tayl ( ( S Dn F ) ` m ) ) = ( S Tayl ( ( S Dn F ) ` 0 ) ) )
14 oveq2 
 |-  ( m = 0 -> ( M - m ) = ( M - 0 ) )
15 14 oveq2d 
 |-  ( m = 0 -> ( N + ( M - m ) ) = ( N + ( M - 0 ) ) )
16 eqidd 
 |-  ( m = 0 -> B = B )
17 13 15 16 oveq123d 
 |-  ( m = 0 -> ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) = ( ( N + ( M - 0 ) ) ( S Tayl ( ( S Dn F ) ` 0 ) ) B ) )
18 11 17 eqeq12d 
 |-  ( m = 0 -> ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) <-> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` 0 ) = ( ( N + ( M - 0 ) ) ( S Tayl ( ( S Dn F ) ` 0 ) ) B ) ) )
19 18 imbi2d 
 |-  ( m = 0 -> ( ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) ) <-> ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` 0 ) = ( ( N + ( M - 0 ) ) ( S Tayl ( ( S Dn F ) ` 0 ) ) B ) ) ) )
20 fveq2 
 |-  ( m = n -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) )
21 fveq2 
 |-  ( m = n -> ( ( S Dn F ) ` m ) = ( ( S Dn F ) ` n ) )
22 21 oveq2d 
 |-  ( m = n -> ( S Tayl ( ( S Dn F ) ` m ) ) = ( S Tayl ( ( S Dn F ) ` n ) ) )
23 oveq2 
 |-  ( m = n -> ( M - m ) = ( M - n ) )
24 23 oveq2d 
 |-  ( m = n -> ( N + ( M - m ) ) = ( N + ( M - n ) ) )
25 eqidd 
 |-  ( m = n -> B = B )
26 22 24 25 oveq123d 
 |-  ( m = n -> ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) )
27 20 26 eqeq12d 
 |-  ( m = n -> ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) <-> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) )
28 27 imbi2d 
 |-  ( m = n -> ( ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) ) <-> ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) ) )
29 fveq2 
 |-  ( m = ( n + 1 ) -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) )
30 fveq2 
 |-  ( m = ( n + 1 ) -> ( ( S Dn F ) ` m ) = ( ( S Dn F ) ` ( n + 1 ) ) )
31 30 oveq2d 
 |-  ( m = ( n + 1 ) -> ( S Tayl ( ( S Dn F ) ` m ) ) = ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) )
32 oveq2 
 |-  ( m = ( n + 1 ) -> ( M - m ) = ( M - ( n + 1 ) ) )
33 32 oveq2d 
 |-  ( m = ( n + 1 ) -> ( N + ( M - m ) ) = ( N + ( M - ( n + 1 ) ) ) )
34 eqidd 
 |-  ( m = ( n + 1 ) -> B = B )
35 31 33 34 oveq123d 
 |-  ( m = ( n + 1 ) -> ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) )
36 29 35 eqeq12d 
 |-  ( m = ( n + 1 ) -> ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) <-> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) ) )
37 36 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) ) <-> ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) ) ) )
38 fveq2 
 |-  ( m = M -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` M ) )
39 fveq2 
 |-  ( m = M -> ( ( S Dn F ) ` m ) = ( ( S Dn F ) ` M ) )
40 39 oveq2d 
 |-  ( m = M -> ( S Tayl ( ( S Dn F ) ` m ) ) = ( S Tayl ( ( S Dn F ) ` M ) ) )
41 oveq2 
 |-  ( m = M -> ( M - m ) = ( M - M ) )
42 41 oveq2d 
 |-  ( m = M -> ( N + ( M - m ) ) = ( N + ( M - M ) ) )
43 eqidd 
 |-  ( m = M -> B = B )
44 40 42 43 oveq123d 
 |-  ( m = M -> ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) = ( ( N + ( M - M ) ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) )
45 38 44 eqeq12d 
 |-  ( m = M -> ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) <-> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` M ) = ( ( N + ( M - M ) ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) ) )
46 45 imbi2d 
 |-  ( m = M -> ( ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` m ) = ( ( N + ( M - m ) ) ( S Tayl ( ( S Dn F ) ` m ) ) B ) ) <-> ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` M ) = ( ( N + ( M - M ) ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) ) ) )
47 ssidd 
 |-  ( ph -> CC C_ CC )
48 mapsspm 
 |-  ( CC ^m CC ) C_ ( CC ^pm CC )
49 5 4 nn0addcld 
 |-  ( ph -> ( N + M ) e. NN0 )
50 eqid 
 |-  ( ( N + M ) ( S Tayl F ) B ) = ( ( N + M ) ( S Tayl F ) B )
51 1 2 3 49 6 50 taylpf 
 |-  ( ph -> ( ( N + M ) ( S Tayl F ) B ) : CC --> CC )
52 cnex 
 |-  CC e. _V
53 52 52 elmap 
 |-  ( ( ( N + M ) ( S Tayl F ) B ) e. ( CC ^m CC ) <-> ( ( N + M ) ( S Tayl F ) B ) : CC --> CC )
54 51 53 sylibr 
 |-  ( ph -> ( ( N + M ) ( S Tayl F ) B ) e. ( CC ^m CC ) )
55 48 54 sseldi 
 |-  ( ph -> ( ( N + M ) ( S Tayl F ) B ) e. ( CC ^pm CC ) )
56 dvn0 
 |-  ( ( CC C_ CC /\ ( ( N + M ) ( S Tayl F ) B ) e. ( CC ^pm CC ) ) -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` 0 ) = ( ( N + M ) ( S Tayl F ) B ) )
57 47 55 56 syl2anc 
 |-  ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` 0 ) = ( ( N + M ) ( S Tayl F ) B ) )
58 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
59 1 58 syl 
 |-  ( ph -> S C_ CC )
60 52 a1i 
 |-  ( ph -> CC e. _V )
61 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
62 60 1 2 3 61 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
63 dvn0 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
64 59 62 63 syl2anc 
 |-  ( ph -> ( ( S Dn F ) ` 0 ) = F )
65 64 oveq2d 
 |-  ( ph -> ( S Tayl ( ( S Dn F ) ` 0 ) ) = ( S Tayl F ) )
66 4 nn0cnd 
 |-  ( ph -> M e. CC )
67 66 subid1d 
 |-  ( ph -> ( M - 0 ) = M )
68 67 oveq2d 
 |-  ( ph -> ( N + ( M - 0 ) ) = ( N + M ) )
69 eqidd 
 |-  ( ph -> B = B )
70 65 68 69 oveq123d 
 |-  ( ph -> ( ( N + ( M - 0 ) ) ( S Tayl ( ( S Dn F ) ` 0 ) ) B ) = ( ( N + M ) ( S Tayl F ) B ) )
71 57 70 eqtr4d 
 |-  ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` 0 ) = ( ( N + ( M - 0 ) ) ( S Tayl ( ( S Dn F ) ` 0 ) ) B ) )
72 71 a1i 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` 0 ) = ( ( N + ( M - 0 ) ) ( S Tayl ( ( S Dn F ) ` 0 ) ) B ) ) )
73 oveq2 
 |-  ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) -> ( CC _D ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) ) = ( CC _D ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) )
74 ssidd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> CC C_ CC )
75 55 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( N + M ) ( S Tayl F ) B ) e. ( CC ^pm CC ) )
76 elfzouz 
 |-  ( n e. ( 0 ..^ M ) -> n e. ( ZZ>= ` 0 ) )
77 76 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> n e. ( ZZ>= ` 0 ) )
78 77 7 eleqtrrdi 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> n e. NN0 )
79 dvnp1 
 |-  ( ( CC C_ CC /\ ( ( N + M ) ( S Tayl F ) B ) e. ( CC ^pm CC ) /\ n e. NN0 ) -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) ) )
80 74 75 78 79 syl3anc 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) ) )
81 1 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> S e. { RR , CC } )
82 62 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> F e. ( CC ^pm S ) )
83 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ n e. NN0 ) -> ( ( S Dn F ) ` n ) : dom ( ( S Dn F ) ` n ) --> CC )
84 81 82 78 83 syl3anc 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( S Dn F ) ` n ) : dom ( ( S Dn F ) ` n ) --> CC )
85 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ n e. NN0 ) -> dom ( ( S Dn F ) ` n ) C_ dom F )
86 81 82 78 85 syl3anc 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> dom ( ( S Dn F ) ` n ) C_ dom F )
87 2 fdmd 
 |-  ( ph -> dom F = A )
88 87 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> dom F = A )
89 86 88 sseqtrd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> dom ( ( S Dn F ) ` n ) C_ A )
90 3 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> A C_ S )
91 89 90 sstrd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> dom ( ( S Dn F ) ` n ) C_ S )
92 5 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> N e. NN0 )
93 fzofzp1 
 |-  ( n e. ( 0 ..^ M ) -> ( n + 1 ) e. ( 0 ... M ) )
94 93 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( n + 1 ) e. ( 0 ... M ) )
95 fznn0sub 
 |-  ( ( n + 1 ) e. ( 0 ... M ) -> ( M - ( n + 1 ) ) e. NN0 )
96 94 95 syl 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( M - ( n + 1 ) ) e. NN0 )
97 92 96 nn0addcld 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( N + ( M - ( n + 1 ) ) ) e. NN0 )
98 6 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> B e. dom ( ( S Dn F ) ` ( N + M ) ) )
99 elfzofz 
 |-  ( n e. ( 0 ..^ M ) -> n e. ( 0 ... M ) )
100 99 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> n e. ( 0 ... M ) )
101 fznn0sub 
 |-  ( n e. ( 0 ... M ) -> ( M - n ) e. NN0 )
102 100 101 syl 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( M - n ) e. NN0 )
103 92 102 nn0addcld 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( N + ( M - n ) ) e. NN0 )
104 dvnadd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( n e. NN0 /\ ( N + ( M - n ) ) e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` n ) ) ` ( N + ( M - n ) ) ) = ( ( S Dn F ) ` ( n + ( N + ( M - n ) ) ) ) )
105 81 82 78 103 104 syl22anc 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( S Dn ( ( S Dn F ) ` n ) ) ` ( N + ( M - n ) ) ) = ( ( S Dn F ) ` ( n + ( N + ( M - n ) ) ) ) )
106 5 nn0cnd 
 |-  ( ph -> N e. CC )
107 106 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> N e. CC )
108 96 nn0cnd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( M - ( n + 1 ) ) e. CC )
109 1cnd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> 1 e. CC )
110 107 108 109 addassd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( N + ( M - ( n + 1 ) ) ) + 1 ) = ( N + ( ( M - ( n + 1 ) ) + 1 ) ) )
111 66 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> M e. CC )
112 78 nn0cnd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> n e. CC )
113 111 112 109 nppcan2d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( M - ( n + 1 ) ) + 1 ) = ( M - n ) )
114 113 oveq2d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( N + ( ( M - ( n + 1 ) ) + 1 ) ) = ( N + ( M - n ) ) )
115 110 114 eqtrd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( N + ( M - ( n + 1 ) ) ) + 1 ) = ( N + ( M - n ) ) )
116 115 fveq2d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( S Dn ( ( S Dn F ) ` n ) ) ` ( ( N + ( M - ( n + 1 ) ) ) + 1 ) ) = ( ( S Dn ( ( S Dn F ) ` n ) ) ` ( N + ( M - n ) ) ) )
117 112 111 pncan3d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( n + ( M - n ) ) = M )
118 117 oveq2d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( N + ( n + ( M - n ) ) ) = ( N + M ) )
119 111 112 subcld 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( M - n ) e. CC )
120 107 112 119 add12d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( N + ( n + ( M - n ) ) ) = ( n + ( N + ( M - n ) ) ) )
121 118 120 eqtr3d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( N + M ) = ( n + ( N + ( M - n ) ) ) )
122 121 fveq2d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( S Dn F ) ` ( N + M ) ) = ( ( S Dn F ) ` ( n + ( N + ( M - n ) ) ) ) )
123 105 116 122 3eqtr4d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( S Dn ( ( S Dn F ) ` n ) ) ` ( ( N + ( M - ( n + 1 ) ) ) + 1 ) ) = ( ( S Dn F ) ` ( N + M ) ) )
124 123 dmeqd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> dom ( ( S Dn ( ( S Dn F ) ` n ) ) ` ( ( N + ( M - ( n + 1 ) ) ) + 1 ) ) = dom ( ( S Dn F ) ` ( N + M ) ) )
125 98 124 eleqtrrd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> B e. dom ( ( S Dn ( ( S Dn F ) ` n ) ) ` ( ( N + ( M - ( n + 1 ) ) ) + 1 ) ) )
126 81 84 91 97 125 dvtaylp 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( CC _D ( ( ( N + ( M - ( n + 1 ) ) ) + 1 ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( S _D ( ( S Dn F ) ` n ) ) ) B ) )
127 115 oveq1d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( ( N + ( M - ( n + 1 ) ) ) + 1 ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) )
128 127 oveq2d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( CC _D ( ( ( N + ( M - ( n + 1 ) ) ) + 1 ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) = ( CC _D ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) )
129 59 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> S C_ CC )
130 dvnp1 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ n e. NN0 ) -> ( ( S Dn F ) ` ( n + 1 ) ) = ( S _D ( ( S Dn F ) ` n ) ) )
131 129 82 78 130 syl3anc 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( S Dn F ) ` ( n + 1 ) ) = ( S _D ( ( S Dn F ) ` n ) ) )
132 131 oveq2d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) = ( S Tayl ( S _D ( ( S Dn F ) ` n ) ) ) )
133 132 eqcomd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( S Tayl ( S _D ( ( S Dn F ) ` n ) ) ) = ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) )
134 133 oveqd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( S _D ( ( S Dn F ) ` n ) ) ) B ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) )
135 126 128 134 3eqtr3rd 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) = ( CC _D ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) )
136 80 135 eqeq12d 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) <-> ( CC _D ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) ) = ( CC _D ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) ) )
137 73 136 syl5ibr 
 |-  ( ( ph /\ n e. ( 0 ..^ M ) ) -> ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) ) )
138 137 expcom 
 |-  ( n e. ( 0 ..^ M ) -> ( ph -> ( ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) ) ) )
139 138 a2d 
 |-  ( n e. ( 0 ..^ M ) -> ( ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` n ) = ( ( N + ( M - n ) ) ( S Tayl ( ( S Dn F ) ` n ) ) B ) ) -> ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` ( n + 1 ) ) = ( ( N + ( M - ( n + 1 ) ) ) ( S Tayl ( ( S Dn F ) ` ( n + 1 ) ) ) B ) ) ) )
140 19 28 37 46 72 139 fzind2 
 |-  ( M e. ( 0 ... M ) -> ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` M ) = ( ( N + ( M - M ) ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) ) )
141 10 140 mpcom 
 |-  ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` M ) = ( ( N + ( M - M ) ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) )
142 66 subidd 
 |-  ( ph -> ( M - M ) = 0 )
143 142 oveq2d 
 |-  ( ph -> ( N + ( M - M ) ) = ( N + 0 ) )
144 106 addid1d 
 |-  ( ph -> ( N + 0 ) = N )
145 143 144 eqtrd 
 |-  ( ph -> ( N + ( M - M ) ) = N )
146 145 oveq1d 
 |-  ( ph -> ( ( N + ( M - M ) ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) = ( N ( S Tayl ( ( S Dn F ) ` M ) ) B ) )
147 141 146 eqtrd 
 |-  ( ph -> ( ( CC Dn ( ( N + M ) ( S Tayl F ) B ) ) ` M ) = ( N ( S Tayl ( ( S Dn F ) ` M ) ) B ) )