Metamath Proof Explorer

Theorem taylfvallem1

Description: Lemma for taylfval . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses taylfval.s 
|- ( ph -> S e. { RR , CC } )
taylfval.f 
|- ( ph -> F : A --> CC )
taylfval.a 
|- ( ph -> A C_ S )
taylfval.n 
|- ( ph -> ( N e. NN0 \/ N = +oo ) )
taylfval.b 
|- ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
Assertion taylfvallem1 
|- ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) e. CC )

Proof

Step Hyp Ref Expression
1 taylfval.s 
 |-  ( ph -> S e. { RR , CC } )
2 taylfval.f 
 |-  ( ph -> F : A --> CC )
3 taylfval.a 
 |-  ( ph -> A C_ S )
4 taylfval.n 
 |-  ( ph -> ( N e. NN0 \/ N = +oo ) )
5 taylfval.b 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
6 1 ad2antrr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> S e. { RR , CC } )
7 cnex 
 |-  CC e. _V
8 7 a1i 
 |-  ( ph -> CC e. _V )
9 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
10 8 1 2 3 9 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
11 10 ad2antrr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> F e. ( CC ^pm S ) )
12 simpr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. ( ( 0 [,] N ) i^i ZZ ) )
13 12 elin2d 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. ZZ )
14 12 elin1d 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. ( 0 [,] N ) )
15 0xr 
 |-  0 e. RR*
16 nn0re 
 |-  ( N e. NN0 -> N e. RR )
17 16 rexrd 
 |-  ( N e. NN0 -> N e. RR* )
18 id 
 |-  ( N = +oo -> N = +oo )
19 pnfxr 
 |-  +oo e. RR*
20 18 19 eqeltrdi 
 |-  ( N = +oo -> N e. RR* )
21 17 20 jaoi 
 |-  ( ( N e. NN0 \/ N = +oo ) -> N e. RR* )
22 4 21 syl 
 |-  ( ph -> N e. RR* )
23 22 ad2antrr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> N e. RR* )
24 elicc1 
 |-  ( ( 0 e. RR* /\ N e. RR* ) -> ( k e. ( 0 [,] N ) <-> ( k e. RR* /\ 0 <_ k /\ k <_ N ) ) )
25 15 23 24 sylancr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( k e. ( 0 [,] N ) <-> ( k e. RR* /\ 0 <_ k /\ k <_ N ) ) )
26 14 25 mpbid 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( k e. RR* /\ 0 <_ k /\ k <_ N ) )
27 26 simp2d 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> 0 <_ k )
28 elnn0z 
 |-  ( k e. NN0 <-> ( k e. ZZ /\ 0 <_ k ) )
29 13 27 28 sylanbrc 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. NN0 )
30 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
31 6 11 29 30 syl3anc 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
32 5 adantlr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
33 31 32 ffvelrnd 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( S Dn F ) ` k ) ` B ) e. CC )
34 29 faccld 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ! ` k ) e. NN )
35 34 nncnd 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ! ` k ) e. CC )
36 34 nnne0d 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ! ` k ) =/= 0 )
37 33 35 36 divcld 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
38 simplr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> X e. CC )
39 2 ad2antrr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> F : A --> CC )
40 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> dom ( ( S Dn F ) ` k ) C_ dom F )
41 6 11 29 40 syl3anc 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> dom ( ( S Dn F ) ` k ) C_ dom F )
42 39 41 fssdmd 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> dom ( ( S Dn F ) ` k ) C_ A )
43 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
44 1 43 syl 
 |-  ( ph -> S C_ CC )
45 3 44 sstrd 
 |-  ( ph -> A C_ CC )
46 45 ad2antrr 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> A C_ CC )
47 42 46 sstrd 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> dom ( ( S Dn F ) ` k ) C_ CC )
48 47 32 sseldd 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. CC )
49 38 48 subcld 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( X - B ) e. CC )
50 49 29 expcld 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( X - B ) ^ k ) e. CC )
51 37 50 mulcld 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) e. CC )