Metamath Proof Explorer

Theorem dvn2bss

Description: An N-times differentiable point is an M-times differentiable point, if M <_ N . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Assertion dvn2bss 
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` M ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> S e. { RR , CC } )
2 simp2 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> F e. ( CC ^pm S ) )
3 elfznn0 
 |-  ( M e. ( 0 ... N ) -> M e. NN0 )
4 3 3ad2ant3 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> M e. NN0 )
5 elfzuz3 
 |-  ( M e. ( 0 ... N ) -> N e. ( ZZ>= ` M ) )
6 5 3ad2ant3 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> N e. ( ZZ>= ` M ) )
7 uznn0sub 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )
8 6 7 syl 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( N - M ) e. NN0 )
9 dvnadd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( M e. NN0 /\ ( N - M ) e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = ( ( S Dn F ) ` ( M + ( N - M ) ) ) )
10 1 2 4 8 9 syl22anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = ( ( S Dn F ) ` ( M + ( N - M ) ) ) )
11 4 nn0cnd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> M e. CC )
12 elfzuz2 
 |-  ( M e. ( 0 ... N ) -> N e. ( ZZ>= ` 0 ) )
13 12 3ad2ant3 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> N e. ( ZZ>= ` 0 ) )
14 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
15 13 14 eleqtrrdi 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> N e. NN0 )
16 15 nn0cnd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> N e. CC )
17 11 16 pncan3d 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( M + ( N - M ) ) = N )
18 17 fveq2d 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( ( S Dn F ) ` ( M + ( N - M ) ) ) = ( ( S Dn F ) ` N ) )
19 10 18 eqtrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = ( ( S Dn F ) ` N ) )
20 19 dmeqd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = dom ( ( S Dn F ) ` N ) )
21 cnex 
 |-  CC e. _V
22 21 a1i 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> CC e. _V )
23 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. NN0 ) -> ( ( S Dn F ) ` M ) : dom ( ( S Dn F ) ` M ) --> CC )
24 3 23 syl3an3 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( ( S Dn F ) ` M ) : dom ( ( S Dn F ) ` M ) --> CC )
25 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. NN0 ) -> dom ( ( S Dn F ) ` M ) C_ dom F )
26 3 25 syl3an3 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` M ) C_ dom F )
27 elpmi 
 |-  ( F e. ( CC ^pm S ) -> ( F : dom F --> CC /\ dom F C_ S ) )
28 27 3ad2ant2 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( F : dom F --> CC /\ dom F C_ S ) )
29 28 simprd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom F C_ S )
30 26 29 sstrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` M ) C_ S )
31 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( ( ( S Dn F ) ` M ) : dom ( ( S Dn F ) ` M ) --> CC /\ dom ( ( S Dn F ) ` M ) C_ S ) ) -> ( ( S Dn F ) ` M ) e. ( CC ^pm S ) )
32 22 1 24 30 31 syl22anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> ( ( S Dn F ) ` M ) e. ( CC ^pm S ) )
33 dvnbss 
 |-  ( ( S e. { RR , CC } /\ ( ( S Dn F ) ` M ) e. ( CC ^pm S ) /\ ( N - M ) e. NN0 ) -> dom ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) C_ dom ( ( S Dn F ) ` M ) )
34 1 32 8 33 syl3anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) C_ dom ( ( S Dn F ) ` M ) )
35 20 34 eqsstrrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` M ) )