Metamath Proof Explorer

Theorem dvexp

Description: Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion dvexp ( 𝑁 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 1 ) )
2 1 mpteq2dv ⊢ ( 𝑛 = 1 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 1 ) ) )
3 2 oveq2d ⊢ ( 𝑛 = 1 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 1 ) ) ) )
4 id ⊢ ( 𝑛 = 1 → 𝑛 = 1 )
5 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 − 1 ) = ( 1 − 1 ) )
6 5 oveq2d ⊢ ( 𝑛 = 1 → ( 𝑥 ↑ ( 𝑛 − 1 ) ) = ( 𝑥 ↑ ( 1 − 1 ) ) )
7 4 6 oveq12d ⊢ ( 𝑛 = 1 → ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) = ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) )
8 7 mpteq2dv ⊢ ( 𝑛 = 1 → ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) ) )
9 3 8 eqeq12d ⊢ ( 𝑛 = 1 → ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 1 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) ) ) )
10 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑘 ) )
11 10 mpteq2dv ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) )
12 11 oveq2d ⊢ ( 𝑛 = 𝑘 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) )
13 id ⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 )
14 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 − 1 ) = ( 𝑘 − 1 ) )
15 14 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ↑ ( 𝑛 − 1 ) ) = ( 𝑥 ↑ ( 𝑘 − 1 ) ) )
16 13 15 oveq12d ⊢ ( 𝑛 = 𝑘 → ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) )
17 16 mpteq2dv ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) )
18 12 17 eqeq12d ⊢ ( 𝑛 = 𝑘 → ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) )
19 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ ( 𝑘 + 1 ) ) )
20 19 mpteq2dv ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) )
21 20 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ) )
22 id ⊢ ( 𝑛 = ( 𝑘 + 1 ) → 𝑛 = ( 𝑘 + 1 ) )
23 oveq1 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 − 1 ) = ( ( 𝑘 + 1 ) − 1 ) )
24 23 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑥 ↑ ( 𝑛 − 1 ) ) = ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) )
25 22 24 oveq12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) = ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) )
26 25 mpteq2dv ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) )
27 21 26 eqeq12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) ) )
28 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑁 ) )
29 28 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) )
30 29 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ) )
31 id ⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
32 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 1 ) = ( 𝑁 − 1 ) )
33 32 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ↑ ( 𝑛 − 1 ) ) = ( 𝑥 ↑ ( 𝑁 − 1 ) ) )
34 31 33 oveq12d ⊢ ( 𝑛 = 𝑁 → ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) )
35 34 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )
36 30 35 eqeq12d ⊢ ( 𝑛 = 𝑁 → ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑛 · ( 𝑥 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) ) )
37 exp1 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 1 ) = 𝑥 )
38 37 mpteq2ia ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 1 ) ) = ( 𝑥 ∈ ℂ ↦ 𝑥 )
39 mptresid ⊢ ( I ↾ ℂ ) = ( 𝑥 ∈ ℂ ↦ 𝑥 )
40 38 39 eqtr4i ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 1 ) ) = ( I ↾ ℂ )
41 40 oveq2i ⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 1 ) ) ) = ( ℂ D ( I ↾ ℂ ) )
42 1m1e0 ⊢ ( 1 − 1 ) = 0
43 42 oveq2i ⊢ ( 𝑥 ↑ ( 1 − 1 ) ) = ( 𝑥 ↑ 0 )
44 exp0 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 0 ) = 1 )
45 43 44 eqtrid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ ( 1 − 1 ) ) = 1 )
46 45 oveq2d ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) = ( 1 · 1 ) )
47 1t1e1 ⊢ ( 1 · 1 ) = 1
48 46 47 eqtrdi ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) = 1 )
49 48 mpteq2ia ⊢ ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ 1 )
50 fconstmpt ⊢ ( ℂ × { 1 } ) = ( 𝑥 ∈ ℂ ↦ 1 )
51 49 50 eqtr4i ⊢ ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) ) = ( ℂ × { 1 } )
52 dvid ⊢ ( ℂ D ( I ↾ ℂ ) ) = ( ℂ × { 1 } )
53 51 52 eqtr4i ⊢ ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) ) = ( ℂ D ( I ↾ ℂ ) )
54 41 53 eqtr4i ⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 1 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ ( 1 − 1 ) ) ) )
55 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
56 55 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → 𝑘 ∈ ℂ )
57 ax-1cn ⊢ 1 ∈ ℂ
58 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
59 56 57 58 sylancl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
60 59 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) = ( 𝑥 ↑ 𝑘 ) )
61 60 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) = ( ( 𝑘 + 1 ) · ( 𝑥 ↑ 𝑘 ) ) )
62 57 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
63 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
64 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
65 expcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
66 63 64 65 syl2anr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
67 56 62 66 adddird ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 + 1 ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) + ( 1 · ( 𝑥 ↑ 𝑘 ) ) ) )
68 66 mullidd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 1 · ( 𝑥 ↑ 𝑘 ) ) = ( 𝑥 ↑ 𝑘 ) )
69 68 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) + ( 1 · ( 𝑥 ↑ 𝑘 ) ) ) = ( ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) + ( 𝑥 ↑ 𝑘 ) ) )
70 61 67 69 3eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) = ( ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) + ( 𝑥 ↑ 𝑘 ) ) )
71 70 mpteq2dva ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) + ( 𝑥 ↑ 𝑘 ) ) ) )
72 cnex ⊢ ℂ ∈ V
73 72 a1i ⊢ ( 𝑘 ∈ ℕ → ℂ ∈ V )
74 56 66 mulcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
75 nnm1nn0 ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
76 expcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑘 − 1 ) ∈ ℕ0 ) → ( 𝑥 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
77 63 75 76 syl2anr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
78 56 77 mulcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
79 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
80 eqidd ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) )
81 39 a1i ⊢ ( 𝑘 ∈ ℕ → ( I ↾ ℂ ) = ( 𝑥 ∈ ℂ ↦ 𝑥 ) )
82 73 78 79 80 81 offval2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ∘f · ( I ↾ ℂ ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) · 𝑥 ) ) )
83 56 77 79 mulassd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) · 𝑥 ) = ( 𝑘 · ( ( 𝑥 ↑ ( 𝑘 − 1 ) ) · 𝑥 ) ) )
84 expm1t ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ↑ 𝑘 ) = ( ( 𝑥 ↑ ( 𝑘 − 1 ) ) · 𝑥 ) )
85 84 ancoms ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 𝑘 ) = ( ( 𝑥 ↑ ( 𝑘 − 1 ) ) · 𝑥 ) )
86 85 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) = ( 𝑘 · ( ( 𝑥 ↑ ( 𝑘 − 1 ) ) · 𝑥 ) ) )
87 83 86 eqtr4d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) · 𝑥 ) = ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) )
88 87 mpteq2dva ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) ) )
89 82 88 eqtrd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ∘f · ( I ↾ ℂ ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) ) )
90 52 50 eqtri ⊢ ( ℂ D ( I ↾ ℂ ) ) = ( 𝑥 ∈ ℂ ↦ 1 )
91 90 a1i ⊢ ( 𝑘 ∈ ℕ → ( ℂ D ( I ↾ ℂ ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
92 eqidd ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) )
93 73 62 66 91 92 offval2 ⊢ ( 𝑘 ∈ ℕ → ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ 𝑘 ) ) ) )
94 68 mpteq2dva ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) )
95 93 94 eqtrd ⊢ ( 𝑘 ∈ ℕ → ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) )
96 73 74 66 89 95 offval2 ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 · ( 𝑥 ↑ 𝑘 ) ) + ( 𝑥 ↑ 𝑘 ) ) ) )
97 71 96 eqtr4d ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) )
98 oveq1 ⊢ ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) → ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ∘f · ( I ↾ ℂ ) ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ∘f · ( I ↾ ℂ ) ) )
99 98 oveq1d ⊢ ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) → ( ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) )
100 99 eqcomd ⊢ ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) = ( ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) )
101 97 100 sylan9eq ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = ( ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) )
102 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
103 102 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ℂ ∈ { ℝ , ℂ } )
104 66 fmpttd ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) : ℂ ⟶ ℂ )
105 104 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) : ℂ ⟶ ℂ )
106 f1oi ⊢ ( I ↾ ℂ ) : ℂ –1-1-onto→ ℂ
107 f1of ⊢ ( ( I ↾ ℂ ) : ℂ –1-1-onto→ ℂ → ( I ↾ ℂ ) : ℂ ⟶ ℂ )
108 106 107 mp1i ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( I ↾ ℂ ) : ℂ ⟶ ℂ )
109 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) )
110 109 dmeqd ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = dom ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) )
111 78 fmpttd ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) : ℂ ⟶ ℂ )
112 111 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) : ℂ ⟶ ℂ )
113 112 fdmd ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → dom ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) = ℂ )
114 110 113 eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ℂ )
115 1ex ⊢ 1 ∈ V
116 115 fconst ⊢ ( ℂ × { 1 } ) : ℂ ⟶ { 1 }
117 52 feq1i ⊢ ( ( ℂ D ( I ↾ ℂ ) ) : ℂ ⟶ { 1 } ↔ ( ℂ × { 1 } ) : ℂ ⟶ { 1 } )
118 116 117 mpbir ⊢ ( ℂ D ( I ↾ ℂ ) ) : ℂ ⟶ { 1 }
119 118 fdmi ⊢ dom ( ℂ D ( I ↾ ℂ ) ) = ℂ
120 119 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → dom ( ℂ D ( I ↾ ℂ ) ) = ℂ )
121 103 105 108 114 120 dvmulf ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( ℂ D ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∘f · ( I ↾ ℂ ) ) ) = ( ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ∘f · ( I ↾ ℂ ) ) ∘f + ( ( ℂ D ( I ↾ ℂ ) ) ∘f · ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) ) )
122 73 66 79 92 81 offval2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∘f · ( I ↾ ℂ ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 𝑘 ) · 𝑥 ) ) )
123 expp1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ↑ ( 𝑘 + 1 ) ) = ( ( 𝑥 ↑ 𝑘 ) · 𝑥 ) )
124 63 64 123 syl2anr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ ( 𝑘 + 1 ) ) = ( ( 𝑥 ↑ 𝑘 ) · 𝑥 ) )
125 124 mpteq2dva ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 𝑘 ) · 𝑥 ) ) )
126 122 125 eqtr4d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∘f · ( I ↾ ℂ ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) )
127 126 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( ℂ D ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∘f · ( I ↾ ℂ ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ) )
128 127 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( ℂ D ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∘f · ( I ↾ ℂ ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ) )
129 101 121 128 3eqtr2rd ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) )
130 129 ex ⊢ ( 𝑘 ∈ ℕ → ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑘 · ( 𝑥 ↑ ( 𝑘 − 1 ) ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑘 + 1 ) · ( 𝑥 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) ) )
131 9 18 27 36 54 130 nnind ⊢ ( 𝑁 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )