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