Metamath Proof Explorer

Theorem dvn1

Description: One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 0p1e1 
 |-  ( 0 + 1 ) = 1
2 1 fveq2i 
 |-  ( ( S Dn F ) ` ( 0 + 1 ) ) = ( ( S Dn F ) ` 1 )
3 0nn0 
 |-  0 e. NN0
4 dvnp1 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ 0 e. NN0 ) -> ( ( S Dn F ) ` ( 0 + 1 ) ) = ( S _D ( ( S Dn F ) ` 0 ) ) )
5 3 4 mp3an3 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` ( 0 + 1 ) ) = ( S _D ( ( S Dn F ) ` 0 ) ) )
6 dvn0 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
7 6 oveq2d 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( S _D ( ( S Dn F ) ` 0 ) ) = ( S _D F ) )
8 5 7 eqtrd 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` ( 0 + 1 ) ) = ( S _D F ) )
9 2 8 eqtr3id 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 1 ) = ( S _D F ) )