Metamath Proof Explorer

Theorem etransclem2

Description: Derivative of G . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem2.xf 
|- F/_ x F
etransclem2.f 
|- ( ph -> F : RR --> CC )
etransclem2.dvnf 
|- ( ( ph /\ i e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
etransclem2.g 
|- G = ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) )
Assertion etransclem2 
|- ( ph -> ( RR _D G ) = ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` ( i + 1 ) ) ` x ) ) )

Proof

Step Hyp Ref Expression
1 etransclem2.xf 
 |-  F/_ x F
2 etransclem2.f 
 |-  ( ph -> F : RR --> CC )
3 etransclem2.dvnf 
 |-  ( ( ph /\ i e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
4 etransclem2.g 
 |-  G = ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) )
5 4 oveq2i 
 |-  ( RR _D G ) = ( RR _D ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) ) )
6 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
7 6 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
8 reelprrecn 
 |-  RR e. { RR , CC }
9 8 a1i 
 |-  ( ph -> RR e. { RR , CC } )
10 reopn 
 |-  RR e. ( topGen ` ran (,) )
11 10 a1i 
 |-  ( ph -> RR e. ( topGen ` ran (,) ) )
12 fzfid 
 |-  ( ph -> ( 0 ... R ) e. Fin )
13 fzelp1 
 |-  ( i e. ( 0 ... R ) -> i e. ( 0 ... ( R + 1 ) ) )
14 13 3 sylan2 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
15 14 3adant3 
 |-  ( ( ph /\ i e. ( 0 ... R ) /\ x e. RR ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
16 simp3 
 |-  ( ( ph /\ i e. ( 0 ... R ) /\ x e. RR ) -> x e. RR )
17 15 16 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ... R ) /\ x e. RR ) -> ( ( ( RR Dn F ) ` i ) ` x ) e. CC )
18 fzp1elp1 
 |-  ( i e. ( 0 ... R ) -> ( i + 1 ) e. ( 0 ... ( R + 1 ) ) )
19 ovex 
 |-  ( i + 1 ) e. _V
20 eleq1 
 |-  ( j = ( i + 1 ) -> ( j e. ( 0 ... ( R + 1 ) ) <-> ( i + 1 ) e. ( 0 ... ( R + 1 ) ) ) )
21 20 anbi2d 
 |-  ( j = ( i + 1 ) -> ( ( ph /\ j e. ( 0 ... ( R + 1 ) ) ) <-> ( ph /\ ( i + 1 ) e. ( 0 ... ( R + 1 ) ) ) ) )
22 fveq2 
 |-  ( j = ( i + 1 ) -> ( ( RR Dn F ) ` j ) = ( ( RR Dn F ) ` ( i + 1 ) ) )
23 22 feq1d 
 |-  ( j = ( i + 1 ) -> ( ( ( RR Dn F ) ` j ) : RR --> CC <-> ( ( RR Dn F ) ` ( i + 1 ) ) : RR --> CC ) )
24 21 23 imbi12d 
 |-  ( j = ( i + 1 ) -> ( ( ( ph /\ j e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` j ) : RR --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` ( i + 1 ) ) : RR --> CC ) ) )
25 eleq1 
 |-  ( i = j -> ( i e. ( 0 ... ( R + 1 ) ) <-> j e. ( 0 ... ( R + 1 ) ) ) )
26 25 anbi2d 
 |-  ( i = j -> ( ( ph /\ i e. ( 0 ... ( R + 1 ) ) ) <-> ( ph /\ j e. ( 0 ... ( R + 1 ) ) ) ) )
27 fveq2 
 |-  ( i = j -> ( ( RR Dn F ) ` i ) = ( ( RR Dn F ) ` j ) )
28 27 feq1d 
 |-  ( i = j -> ( ( ( RR Dn F ) ` i ) : RR --> CC <-> ( ( RR Dn F ) ` j ) : RR --> CC ) )
29 26 28 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC ) <-> ( ( ph /\ j e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` j ) : RR --> CC ) ) )
30 29 3 chvarvv 
 |-  ( ( ph /\ j e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` j ) : RR --> CC )
31 19 24 30 vtocl 
 |-  ( ( ph /\ ( i + 1 ) e. ( 0 ... ( R + 1 ) ) ) -> ( ( RR Dn F ) ` ( i + 1 ) ) : RR --> CC )
32 18 31 sylan2 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` ( i + 1 ) ) : RR --> CC )
33 32 3adant3 
 |-  ( ( ph /\ i e. ( 0 ... R ) /\ x e. RR ) -> ( ( RR Dn F ) ` ( i + 1 ) ) : RR --> CC )
34 33 16 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ... R ) /\ x e. RR ) -> ( ( ( RR Dn F ) ` ( i + 1 ) ) ` x ) e. CC )
35 14 ffnd 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` i ) Fn RR )
36 nfcv 
 |-  F/_ x RR
37 nfcv 
 |-  F/_ x Dn
38 36 37 1 nfov 
 |-  F/_ x ( RR Dn F )
39 nfcv 
 |-  F/_ x i
40 38 39 nffv 
 |-  F/_ x ( ( RR Dn F ) ` i )
41 40 dffn5f 
 |-  ( ( ( RR Dn F ) ` i ) Fn RR <-> ( ( RR Dn F ) ` i ) = ( x e. RR |-> ( ( ( RR Dn F ) ` i ) ` x ) ) )
42 35 41 sylib 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` i ) = ( x e. RR |-> ( ( ( RR Dn F ) ` i ) ` x ) ) )
43 42 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( x e. RR |-> ( ( ( RR Dn F ) ` i ) ` x ) ) = ( ( RR Dn F ) ` i ) )
44 43 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( RR _D ( x e. RR |-> ( ( ( RR Dn F ) ` i ) ` x ) ) ) = ( RR _D ( ( RR Dn F ) ` i ) ) )
45 ax-resscn 
 |-  RR C_ CC
46 45 a1i 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> RR C_ CC )
47 ffdm 
 |-  ( F : RR --> CC -> ( F : dom F --> CC /\ dom F C_ RR ) )
48 2 47 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ RR ) )
49 cnex 
 |-  CC e. _V
50 49 a1i 
 |-  ( ph -> CC e. _V )
51 reex 
 |-  RR e. _V
52 elpm2g 
 |-  ( ( CC e. _V /\ RR e. _V ) -> ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) ) )
53 50 51 52 sylancl 
 |-  ( ph -> ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) ) )
54 48 53 mpbird 
 |-  ( ph -> F e. ( CC ^pm RR ) )
55 54 adantr 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> F e. ( CC ^pm RR ) )
56 elfznn0 
 |-  ( i e. ( 0 ... R ) -> i e. NN0 )
57 56 adantl 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> i e. NN0 )
58 dvnp1 
 |-  ( ( RR C_ CC /\ F e. ( CC ^pm RR ) /\ i e. NN0 ) -> ( ( RR Dn F ) ` ( i + 1 ) ) = ( RR _D ( ( RR Dn F ) ` i ) ) )
59 46 55 57 58 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` ( i + 1 ) ) = ( RR _D ( ( RR Dn F ) ` i ) ) )
60 32 ffnd 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` ( i + 1 ) ) Fn RR )
61 nfcv 
 |-  F/_ x ( i + 1 )
62 38 61 nffv 
 |-  F/_ x ( ( RR Dn F ) ` ( i + 1 ) )
63 62 dffn5f 
 |-  ( ( ( RR Dn F ) ` ( i + 1 ) ) Fn RR <-> ( ( RR Dn F ) ` ( i + 1 ) ) = ( x e. RR |-> ( ( ( RR Dn F ) ` ( i + 1 ) ) ` x ) ) )
64 60 63 sylib 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` ( i + 1 ) ) = ( x e. RR |-> ( ( ( RR Dn F ) ` ( i + 1 ) ) ` x ) ) )
65 44 59 64 3eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( RR _D ( x e. RR |-> ( ( ( RR Dn F ) ` i ) ` x ) ) ) = ( x e. RR |-> ( ( ( RR Dn F ) ` ( i + 1 ) ) ` x ) ) )
66 7 6 9 11 12 17 34 65 dvmptfsum 
 |-  ( ph -> ( RR _D ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) ) ) = ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` ( i + 1 ) ) ` x ) ) )
67 5 66 syl5eq 
 |-  ( ph -> ( RR _D G ) = ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` ( i + 1 ) ) ` x ) ) )