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 ( ๐‘ โˆˆ โ„•0 โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 โŠข ( ๐‘ โˆˆ โ„•0 โ†” ( ๐‘ โˆˆ โ„• โˆจ ๐‘ = 0 ) )
2 dvexp โŠข ( ๐‘ โˆˆ โ„• โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
3 nnne0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0 )
4 3 neneqd โŠข ( ๐‘ โˆˆ โ„• โ†’ ยฌ ๐‘ = 0 )
5 4 iffalsed โŠข ( ๐‘ โˆˆ โ„• โ†’ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) = ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) )
6 5 mpteq2dv โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
7 2 6 eqtr4d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )
8 oveq2 โŠข ( ๐‘ = 0 โ†’ ( ๐‘ฅ โ†‘ ๐‘ ) = ( ๐‘ฅ โ†‘ 0 ) )
9 exp0 โŠข ( ๐‘ฅ โˆˆ โ„‚ โ†’ ( ๐‘ฅ โ†‘ 0 ) = 1 )
10 8 9 sylan9eq โŠข ( ( ๐‘ = 0 โˆง ๐‘ฅ โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ โ†‘ ๐‘ ) = 1 )
11 10 mpteq2dva โŠข ( ๐‘ = 0 โ†’ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ 1 ) )
12 fconstmpt โŠข ( โ„‚ ร— { 1 } ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ 1 )
13 11 12 eqtr4di โŠข ( ๐‘ = 0 โ†’ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) = ( โ„‚ ร— { 1 } ) )
14 13 oveq2d โŠข ( ๐‘ = 0 โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( โ„‚ D ( โ„‚ ร— { 1 } ) ) )
15 ax-1cn โŠข 1 โˆˆ โ„‚
16 dvconst โŠข ( 1 โˆˆ โ„‚ โ†’ ( โ„‚ D ( โ„‚ ร— { 1 } ) ) = ( โ„‚ ร— { 0 } ) )
17 15 16 ax-mp โŠข ( โ„‚ D ( โ„‚ ร— { 1 } ) ) = ( โ„‚ ร— { 0 } )
18 14 17 eqtrdi โŠข ( ๐‘ = 0 โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( โ„‚ ร— { 0 } ) )
19 fconstmpt โŠข ( โ„‚ ร— { 0 } ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ 0 )
20 18 19 eqtrdi โŠข ( ๐‘ = 0 โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ 0 ) )
21 iftrue โŠข ( ๐‘ = 0 โ†’ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) = 0 )
22 21 mpteq2dv โŠข ( ๐‘ = 0 โ†’ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ 0 ) )
23 20 22 eqtr4d โŠข ( ๐‘ = 0 โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )
24 7 23 jaoi โŠข ( ( ๐‘ โˆˆ โ„• โˆจ ๐‘ = 0 ) โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )
25 1 24 sylbi โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( โ„‚ D ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โ†‘ ๐‘ ) ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ if ( ๐‘ = 0 , 0 , ( ๐‘ ยท ( ๐‘ฅ โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) )