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∈ℕ0→dx∈ℂxNdℂx=x∈ℂ⟼ifN=00N⁢xN−1

Proof

Step Hyp Ref Expression
1 elnn0 ⊢N∈ℕ0↔N∈ℕ∨N=0
2 dvexp ⊢N∈ℕ→dx∈ℂxNdℂx=x∈ℂ⟼N⁢xN−1
3 nnne0 ⊢N∈ℕ→N≠0
4 3 neneqd ⊢N∈ℕ→¬N=0
5 4 iffalsed ⊢N∈ℕ→ifN=00N⁢xN−1=N⁢xN−1
6 5 mpteq2dv ⊢N∈ℕ→x∈ℂ⟼ifN=00N⁢xN−1=x∈ℂ⟼N⁢xN−1
7 2 6 eqtr4d ⊢N∈ℕ→dx∈ℂxNdℂx=x∈ℂ⟼ifN=00N⁢xN−1
8 oveq2 ⊢N=0→xN=x0
9 exp0 ⊢x∈ℂ→x0=1
10 8 9 sylan9eq ⊢N=0∧x∈ℂ→xN=1
11 10 mpteq2dva ⊢N=0→x∈ℂ⟼xN=x∈ℂ⟼1
12 fconstmpt ⊢ℂ×1=x∈ℂ⟼1
13 11 12 eqtr4di ⊢N=0→x∈ℂ⟼xN=ℂ×1
14 13 oveq2d ⊢N=0→dx∈ℂxNdℂx=ℂDℂ×1
15 ax-1cn ⊢1∈ℂ
16 dvconst ⊢1∈ℂ→ℂDℂ×1=ℂ×0
17 15 16 ax-mp ⊢ℂDℂ×1=ℂ×0
18 14 17 eqtrdi ⊢N=0→dx∈ℂxNdℂx=ℂ×0
19 fconstmpt ⊢ℂ×0=x∈ℂ⟼0
20 18 19 eqtrdi ⊢N=0→dx∈ℂxNdℂx=x∈ℂ⟼0
21 iftrue ⊢N=0→ifN=00N⁢xN−1=0
22 21 mpteq2dv ⊢N=0→x∈ℂ⟼ifN=00N⁢xN−1=x∈ℂ⟼0
23 20 22 eqtr4d ⊢N=0→dx∈ℂxNdℂx=x∈ℂ⟼ifN=00N⁢xN−1
24 7 23 jaoi ⊢N∈ℕ∨N=0→dx∈ℂxNdℂx=x∈ℂ⟼ifN=00N⁢xN−1
25 1 24 sylbi ⊢N∈ℕ0→dx∈ℂxNdℂx=x∈ℂ⟼ifN=00N⁢xN−1