Metamath Proof Explorer

Theorem dvexp2

Description: Derivative of an exponential, possibly zero power. (Contributed by Stefan O'Rear, 13-Nov-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion dvexp2 
|- ( N e. NN0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 dvexp 
 |-  ( N e. NN -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
3 nnne0 
 |-  ( N e. NN -> N =/= 0 )
4 3 neneqd 
 |-  ( N e. NN -> -. N = 0 )
5 4 iffalsed 
 |-  ( N e. NN -> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) = ( N x. ( x ^ ( N - 1 ) ) ) )
6 5 mpteq2dv 
 |-  ( N e. NN -> ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
7 2 6 eqtr4d 
 |-  ( N e. NN -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
8 oveq2 
 |-  ( N = 0 -> ( x ^ N ) = ( x ^ 0 ) )
9 exp0 
 |-  ( x e. CC -> ( x ^ 0 ) = 1 )
10 8 9 sylan9eq 
 |-  ( ( N = 0 /\ x e. CC ) -> ( x ^ N ) = 1 )
11 10 mpteq2dva 
 |-  ( N = 0 -> ( x e. CC |-> ( x ^ N ) ) = ( x e. CC |-> 1 ) )
12 fconstmpt 
 |-  ( CC X. { 1 } ) = ( x e. CC |-> 1 )
13 11 12 eqtr4di 
 |-  ( N = 0 -> ( x e. CC |-> ( x ^ N ) ) = ( CC X. { 1 } ) )
14 13 oveq2d 
 |-  ( N = 0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( CC _D ( CC X. { 1 } ) ) )
15 ax-1cn 
 |-  1 e. CC
16 dvconst 
 |-  ( 1 e. CC -> ( CC _D ( CC X. { 1 } ) ) = ( CC X. { 0 } ) )
17 15 16 ax-mp 
 |-  ( CC _D ( CC X. { 1 } ) ) = ( CC X. { 0 } )
18 14 17 eqtrdi 
 |-  ( N = 0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( CC X. { 0 } ) )
19 fconstmpt 
 |-  ( CC X. { 0 } ) = ( x e. CC |-> 0 )
20 18 19 eqtrdi 
 |-  ( N = 0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> 0 ) )
21 iftrue 
 |-  ( N = 0 -> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) = 0 )
22 21 mpteq2dv 
 |-  ( N = 0 -> ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) = ( x e. CC |-> 0 ) )
23 20 22 eqtr4d 
 |-  ( N = 0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
24 7 23 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
25 1 24 sylbi 
 |-  ( N e. NN0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )