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 ∈ ℂ x N d ℂ x = x ∈ ℂ ⟼ if N = 0 0 N ⁢ x N − 1

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 dvexp ⊢ N ∈ ℕ → dx ∈ ℂ x N d ℂ x = x ∈ ℂ ⟼ N ⁢ x N − 1
3 nnne0 ⊢ N ∈ ℕ → N ≠ 0
4 3 neneqd ⊢ N ∈ ℕ → ¬ N = 0
5 4 iffalsed ⊢ N ∈ ℕ → if N = 0 0 N ⁢ x N − 1 = N ⁢ x N − 1
6 5 mpteq2dv ⊢ N ∈ ℕ → x ∈ ℂ ⟼ if N = 0 0 N ⁢ x N − 1 = x ∈ ℂ ⟼ N ⁢ x N − 1
7 2 6 eqtr4d ⊢ N ∈ ℕ → dx ∈ ℂ x N d ℂ x = x ∈ ℂ ⟼ if N = 0 0 N ⁢ x N − 1
8 oveq2 ⊢ N = 0 → x N = x 0
9 exp0 ⊢ x ∈ ℂ → x 0 = 1
10 8 9 sylan9eq ⊢ N = 0 ∧ x ∈ ℂ → x N = 1
11 10 mpteq2dva ⊢ N = 0 → x ∈ ℂ ⟼ x N = x ∈ ℂ ⟼ 1
12 fconstmpt ⊢ ℂ × 1 = x ∈ ℂ ⟼ 1
13 11 12 eqtr4di ⊢ N = 0 → x ∈ ℂ ⟼ x N = ℂ × 1
14 13 oveq2d ⊢ N = 0 → dx ∈ ℂ x N d ℂ 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 ∈ ℂ x N d ℂ x = ℂ × 0
19 fconstmpt ⊢ ℂ × 0 = x ∈ ℂ ⟼ 0
20 18 19 eqtrdi ⊢ N = 0 → dx ∈ ℂ x N d ℂ x = x ∈ ℂ ⟼ 0
21 iftrue ⊢ N = 0 → if N = 0 0 N ⁢ x N − 1 = 0
22 21 mpteq2dv ⊢ N = 0 → x ∈ ℂ ⟼ if N = 0 0 N ⁢ x N − 1 = x ∈ ℂ ⟼ 0
23 20 22 eqtr4d ⊢ N = 0 → dx ∈ ℂ x N d ℂ x = x ∈ ℂ ⟼ if N = 0 0 N ⁢ x N − 1
24 7 23 jaoi ⊢ N ∈ ℕ ∨ N = 0 → dx ∈ ℂ x N d ℂ x = x ∈ ℂ ⟼ if N = 0 0 N ⁢ x N − 1
25 1 24 sylbi ⊢ N ∈ ℕ 0 → dx ∈ ℂ x N d ℂ x = x ∈ ℂ ⟼ if N = 0 0 N ⁢ x N − 1