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 ) )