Metamath Proof Explorer

Theorem taylplem1

Description: Lemma for taylpfval and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 taylpfval.s 
 |-  ( ph -> S e. { RR , CC } )
2 taylpfval.f 
 |-  ( ph -> F : A --> CC )
3 taylpfval.a 
 |-  ( ph -> A C_ S )
4 taylpfval.n 
 |-  ( ph -> N e. NN0 )
5 taylpfval.b 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` N ) )
6 0z 
 |-  0 e. ZZ
7 4 nn0zd 
 |-  ( ph -> N e. ZZ )
8 fzval2 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 ... N ) = ( ( 0 [,] N ) i^i ZZ ) )
9 6 7 8 sylancr 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 [,] N ) i^i ZZ ) )
10 9 eleq2d 
 |-  ( ph -> ( k e. ( 0 ... N ) <-> k e. ( ( 0 [,] N ) i^i ZZ ) ) )
11 10 biimpar 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. ( 0 ... N ) )
12 cnex 
 |-  CC e. _V
13 12 a1i 
 |-  ( ph -> CC e. _V )
14 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
15 13 1 2 3 14 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
16 1 15 jca 
 |-  ( ph -> ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) )
17 dvn2bss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` k ) )
18 17 3expa 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ k e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` k ) )
19 16 18 sylan 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` k ) )
20 5 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` N ) )
21 19 20 sseldd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` k ) )
22 11 21 syldan 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )