Metamath Proof Explorer

Theorem dvnadd

Description: The N -th derivative of the M -th derivative of F is the same as the M + N -th derivative of F . (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnadd 
|- ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( n = 0 -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn ( ( S Dn F ) ` M ) ) ` 0 ) )
2 oveq2 
 |-  ( n = 0 -> ( M + n ) = ( M + 0 ) )
3 2 fveq2d 
 |-  ( n = 0 -> ( ( S Dn F ) ` ( M + n ) ) = ( ( S Dn F ) ` ( M + 0 ) ) )
4 1 3 eqeq12d 
 |-  ( n = 0 -> ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) <-> ( ( S Dn ( ( S Dn F ) ` M ) ) ` 0 ) = ( ( S Dn F ) ` ( M + 0 ) ) ) )
5 4 imbi2d 
 |-  ( n = 0 -> ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) ) <-> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` 0 ) = ( ( S Dn F ) ` ( M + 0 ) ) ) ) )
6 fveq2 
 |-  ( n = k -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) )
7 oveq2 
 |-  ( n = k -> ( M + n ) = ( M + k ) )
8 7 fveq2d 
 |-  ( n = k -> ( ( S Dn F ) ` ( M + n ) ) = ( ( S Dn F ) ` ( M + k ) ) )
9 6 8 eqeq12d 
 |-  ( n = k -> ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) <-> ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) = ( ( S Dn F ) ` ( M + k ) ) ) )
10 9 imbi2d 
 |-  ( n = k -> ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) ) <-> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) = ( ( S Dn F ) ` ( M + k ) ) ) ) )
11 fveq2 
 |-  ( n = ( k + 1 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) )
12 oveq2 
 |-  ( n = ( k + 1 ) -> ( M + n ) = ( M + ( k + 1 ) ) )
13 12 fveq2d 
 |-  ( n = ( k + 1 ) -> ( ( S Dn F ) ` ( M + n ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) )
14 11 13 eqeq12d 
 |-  ( n = ( k + 1 ) -> ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) <-> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) ) )
15 14 imbi2d 
 |-  ( n = ( k + 1 ) -> ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) ) <-> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) ) ) )
16 fveq2 
 |-  ( n = N -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) )
17 oveq2 
 |-  ( n = N -> ( M + n ) = ( M + N ) )
18 17 fveq2d 
 |-  ( n = N -> ( ( S Dn F ) ` ( M + n ) ) = ( ( S Dn F ) ` ( M + N ) ) )
19 16 18 eqeq12d 
 |-  ( n = N -> ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) <-> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) ) )
20 19 imbi2d 
 |-  ( n = N -> ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` n ) = ( ( S Dn F ) ` ( M + n ) ) ) <-> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) ) ) )
21 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
22 21 ad2antrr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> S C_ CC )
23 ssidd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> CC C_ CC )
24 cnex 
 |-  CC e. _V
25 elpm2g 
 |-  ( ( CC e. _V /\ S e. { RR , CC } ) -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
26 24 25 mpan 
 |-  ( S e. { RR , CC } -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
27 26 simplbda 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> dom F C_ S )
28 24 a1i 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> CC e. _V )
29 simpl 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> S e. { RR , CC } )
30 pmss12g 
 |-  ( ( ( CC C_ CC /\ dom F C_ S ) /\ ( CC e. _V /\ S e. { RR , CC } ) ) -> ( CC ^pm dom F ) C_ ( CC ^pm S ) )
31 23 27 28 29 30 syl22anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( CC ^pm dom F ) C_ ( CC ^pm S ) )
32 31 adantr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( CC ^pm dom F ) C_ ( CC ^pm S ) )
33 dvnff 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) : NN0 --> ( CC ^pm dom F ) )
34 33 ffvelrnda 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn F ) ` M ) e. ( CC ^pm dom F ) )
35 32 34 sseldd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn F ) ` M ) e. ( CC ^pm S ) )
36 dvn0 
 |-  ( ( S C_ CC /\ ( ( S Dn F ) ` M ) e. ( CC ^pm S ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` 0 ) = ( ( S Dn F ) ` M ) )
37 22 35 36 syl2anc 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` 0 ) = ( ( S Dn F ) ` M ) )
38 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
39 38 adantl 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> M e. CC )
40 39 addid1d 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( M + 0 ) = M )
41 40 fveq2d 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn F ) ` ( M + 0 ) ) = ( ( S Dn F ) ` M ) )
42 37 41 eqtr4d 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` 0 ) = ( ( S Dn F ) ` ( M + 0 ) ) )
43 oveq2 
 |-  ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) = ( ( S Dn F ) ` ( M + k ) ) -> ( S _D ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) ) = ( S _D ( ( S Dn F ) ` ( M + k ) ) ) )
44 22 adantr 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> S C_ CC )
45 35 adantr 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( S Dn F ) ` M ) e. ( CC ^pm S ) )
46 simpr 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> k e. NN0 )
47 dvnp1 
 |-  ( ( S C_ CC /\ ( ( S Dn F ) ` M ) e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( S _D ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) ) )
48 44 45 46 47 syl3anc 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( S _D ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) ) )
49 39 adantr 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> M e. CC )
50 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
51 50 adantl 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> k e. CC )
52 1cnd 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> 1 e. CC )
53 49 51 52 addassd 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( M + k ) + 1 ) = ( M + ( k + 1 ) ) )
54 53 fveq2d 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( S Dn F ) ` ( ( M + k ) + 1 ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) )
55 simpllr 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> F e. ( CC ^pm S ) )
56 nn0addcl 
 |-  ( ( M e. NN0 /\ k e. NN0 ) -> ( M + k ) e. NN0 )
57 56 adantll 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( M + k ) e. NN0 )
58 dvnp1 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ ( M + k ) e. NN0 ) -> ( ( S Dn F ) ` ( ( M + k ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( M + k ) ) ) )
59 44 55 57 58 syl3anc 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( S Dn F ) ` ( ( M + k ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( M + k ) ) ) )
60 54 59 eqtr3d 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) = ( S _D ( ( S Dn F ) ` ( M + k ) ) ) )
61 48 60 eqeq12d 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) <-> ( S _D ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) ) = ( S _D ( ( S Dn F ) ` ( M + k ) ) ) ) )
62 43 61 syl5ibr 
 |-  ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) = ( ( S Dn F ) ` ( M + k ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) ) )
63 62 expcom 
 |-  ( k e. NN0 -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) = ( ( S Dn F ) ` ( M + k ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) ) ) )
64 63 a2d 
 |-  ( k e. NN0 -> ( ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) = ( ( S Dn F ) ` ( M + k ) ) ) -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( k + 1 ) ) = ( ( S Dn F ) ` ( M + ( k + 1 ) ) ) ) ) )
65 5 10 15 20 42 64 nn0ind 
 |-  ( N e. NN0 -> ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) ) )
66 65 com12 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ M e. NN0 ) -> ( N e. NN0 -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) ) )
67 66 impr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) )