Metamath Proof Explorer

Theorem dvn0

Description: Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvn0 
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. _V |-> ( S _D x ) ) = ( x e. _V |-> ( S _D x ) )
2 1 dvnfval 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) = seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) )
3 2 fveq1d 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` 0 ) )
4 0z 
 |-  0 e. ZZ
5 simpr 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> F e. ( CC ^pm S ) )
6 0nn0 
 |-  0 e. NN0
7 fvconst2g 
 |-  ( ( F e. ( CC ^pm S ) /\ 0 e. NN0 ) -> ( ( NN0 X. { F } ) ` 0 ) = F )
8 5 6 7 sylancl 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( NN0 X. { F } ) ` 0 ) = F )
9 4 8 seq1i 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` 0 ) = F )
10 3 9 eqtrd 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )