Metamath Proof Explorer

Theorem dvef

Description: Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014) (Proof shortened by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion dvef ( ℂ D exp ) = exp

Proof

Step Hyp Ref Expression
1 dvfcn ⊢ ( ℂ D exp ) : dom ( ℂ D exp ) ⟶ ℂ
2 dvbsss ⊢ dom ( ℂ D exp ) ⊆ ℂ
3 subcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑧 − 𝑥 ) ∈ ℂ )
4 3 ancoms ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑧 − 𝑥 ) ∈ ℂ )
5 efadd ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑧 − 𝑥 ) ∈ ℂ ) → ( exp ‘ ( 𝑥 + ( 𝑧 − 𝑥 ) ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑧 − 𝑥 ) ) ) )
6 4 5 syldan ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ ( 𝑥 + ( 𝑧 − 𝑥 ) ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑧 − 𝑥 ) ) ) )
7 pncan3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 + ( 𝑧 − 𝑥 ) ) = 𝑧 )
8 7 fveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ ( 𝑥 + ( 𝑧 − 𝑥 ) ) ) = ( exp ‘ 𝑧 ) )
9 6 8 eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑧 − 𝑥 ) ) ) = ( exp ‘ 𝑧 ) )
10 9 mpteq2dva ⊢ ( 𝑥 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑧 ) ) )
11 cnex ⊢ ℂ ∈ V
12 11 a1i ⊢ ( 𝑥 ∈ ℂ → ℂ ∈ V )
13 fvexd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ 𝑥 ) ∈ V )
14 fvexd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ ( 𝑧 − 𝑥 ) ) ∈ V )
15 fconstmpt ⊢ ( ℂ × { ( exp ‘ 𝑥 ) } ) = ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑥 ) )
16 15 a1i ⊢ ( 𝑥 ∈ ℂ → ( ℂ × { ( exp ‘ 𝑥 ) } ) = ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
17 eqidd ⊢ ( 𝑥 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) )
18 12 13 14 16 17 offval2 ⊢ ( 𝑥 ∈ ℂ → ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) )
19 eff ⊢ exp : ℂ ⟶ ℂ
20 19 a1i ⊢ ( 𝑥 ∈ ℂ → exp : ℂ ⟶ ℂ )
21 20 feqmptd ⊢ ( 𝑥 ∈ ℂ → exp = ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑧 ) ) )
22 10 18 21 3eqtr4d ⊢ ( 𝑥 ∈ ℂ → ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) = exp )
23 22 oveq2d ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) ) = ( ℂ D exp ) )
24 efcl ⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
25 fconstg ⊢ ( ( exp ‘ 𝑥 ) ∈ ℂ → ( ℂ × { ( exp ‘ 𝑥 ) } ) : ℂ ⟶ { ( exp ‘ 𝑥 ) } )
26 24 25 syl ⊢ ( 𝑥 ∈ ℂ → ( ℂ × { ( exp ‘ 𝑥 ) } ) : ℂ ⟶ { ( exp ‘ 𝑥 ) } )
27 24 snssd ⊢ ( 𝑥 ∈ ℂ → { ( exp ‘ 𝑥 ) } ⊆ ℂ )
28 26 27 fssd ⊢ ( 𝑥 ∈ ℂ → ( ℂ × { ( exp ‘ 𝑥 ) } ) : ℂ ⟶ ℂ )
29 ssidd ⊢ ( 𝑥 ∈ ℂ → ℂ ⊆ ℂ )
30 efcl ⊢ ( ( 𝑧 − 𝑥 ) ∈ ℂ → ( exp ‘ ( 𝑧 − 𝑥 ) ) ∈ ℂ )
31 4 30 syl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ ( 𝑧 − 𝑥 ) ) ∈ ℂ )
32 31 fmpttd ⊢ ( 𝑥 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) : ℂ ⟶ ℂ )
33 c0ex ⊢ 0 ∈ V
34 33 snid ⊢ 0 ∈ { 0 }
35 opelxpi ⊢ ( ( 𝑥 ∈ ℂ ∧ 0 ∈ { 0 } ) → ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ × { 0 } ) )
36 34 35 mpan2 ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ × { 0 } ) )
37 dvconst ⊢ ( ( exp ‘ 𝑥 ) ∈ ℂ → ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) = ( ℂ × { 0 } ) )
38 24 37 syl ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) = ( ℂ × { 0 } ) )
39 36 38 eleqtrrd ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) )
40 df-br ⊢ ( 𝑥 ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) 0 ↔ ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) )
41 39 40 sylibr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) 0 )
42 20 4 cofmpt ⊢ ( 𝑥 ∈ ℂ → ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) )
43 42 oveq2d ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) ) = ( ℂ D ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) )
44 4 fmpttd ⊢ ( 𝑥 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) : ℂ ⟶ ℂ )
45 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 − 𝑥 ) = ( 𝑥 − 𝑥 ) )
46 eqid ⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) )
47 ovex ⊢ ( 𝑥 − 𝑥 ) ∈ V
48 45 46 47 fvmpt ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ‘ 𝑥 ) = ( 𝑥 − 𝑥 ) )
49 subid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 𝑥 ) = 0 )
50 48 49 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ‘ 𝑥 ) = 0 )
51 dveflem ⊢ 0 ( ℂ D exp ) 1
52 50 51 eqbrtrdi ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ‘ 𝑥 ) ( ℂ D exp ) 1 )
53 1ex ⊢ 1 ∈ V
54 53 snid ⊢ 1 ∈ { 1 }
55 opelxpi ⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ { 1 } ) → ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ × { 1 } ) )
56 54 55 mpan2 ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ × { 1 } ) )
57 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
58 57 a1i ⊢ ( 𝑥 ∈ ℂ → ℂ ∈ { ℝ , ℂ } )
59 simpr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
60 1cnd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 1 ∈ ℂ )
61 58 dvmptid ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ 𝑧 ) ) = ( 𝑧 ∈ ℂ ↦ 1 ) )
62 simpl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝑥 ∈ ℂ )
63 0cnd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 0 ∈ ℂ )
64 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
65 58 64 dvmptc ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑧 ∈ ℂ ↦ 0 ) )
66 58 59 60 61 62 63 65 dvmptsub ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 1 − 0 ) ) )
67 1m0e1 ⊢ ( 1 − 0 ) = 1
68 67 mpteq2i ⊢ ( 𝑧 ∈ ℂ ↦ ( 1 − 0 ) ) = ( 𝑧 ∈ ℂ ↦ 1 )
69 fconstmpt ⊢ ( ℂ × { 1 } ) = ( 𝑧 ∈ ℂ ↦ 1 )
70 68 69 eqtr4i ⊢ ( 𝑧 ∈ ℂ ↦ ( 1 − 0 ) ) = ( ℂ × { 1 } )
71 66 70 eqtrdi ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) = ( ℂ × { 1 } ) )
72 56 71 eleqtrrd ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) )
73 df-br ⊢ ( 𝑥 ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) 1 ↔ ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) )
74 72 73 sylibr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) 1 )
75 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
76 20 29 44 29 29 29 52 74 75 dvcobr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) ) ( 1 · 1 ) )
77 1t1e1 ⊢ ( 1 · 1 ) = 1
78 76 77 breqtrdi ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) ) 1 )
79 43 78 breqdi ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) 1 )
80 28 29 32 29 29 41 79 75 dvmulbr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) ) ( ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) + ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) ) )
81 32 64 ffvelcdmd ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ∈ ℂ )
82 81 mul02d ⊢ ( 𝑥 ∈ ℂ → ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) = 0 )
83 fvex ⊢ ( exp ‘ 𝑥 ) ∈ V
84 83 fvconst2 ⊢ ( 𝑥 ∈ ℂ → ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
85 84 oveq2d ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) = ( 1 · ( exp ‘ 𝑥 ) ) )
86 24 mullidd ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( exp ‘ 𝑥 ) ) = ( exp ‘ 𝑥 ) )
87 85 86 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) = ( exp ‘ 𝑥 ) )
88 82 87 oveq12d ⊢ ( 𝑥 ∈ ℂ → ( ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) + ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) ) = ( 0 + ( exp ‘ 𝑥 ) ) )
89 24 addlidd ⊢ ( 𝑥 ∈ ℂ → ( 0 + ( exp ‘ 𝑥 ) ) = ( exp ‘ 𝑥 ) )
90 88 89 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) + ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) ) = ( exp ‘ 𝑥 ) )
91 80 90 breqtrd ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) ) ( exp ‘ 𝑥 ) )
92 23 91 breqdi ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D exp ) ( exp ‘ 𝑥 ) )
93 vex ⊢ 𝑥 ∈ V
94 93 83 breldm ⊢ ( 𝑥 ( ℂ D exp ) ( exp ‘ 𝑥 ) → 𝑥 ∈ dom ( ℂ D exp ) )
95 92 94 syl ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ dom ( ℂ D exp ) )
96 95 ssriv ⊢ ℂ ⊆ dom ( ℂ D exp )
97 2 96 eqssi ⊢ dom ( ℂ D exp ) = ℂ
98 97 feq2i ⊢ ( ( ℂ D exp ) : dom ( ℂ D exp ) ⟶ ℂ ↔ ( ℂ D exp ) : ℂ ⟶ ℂ )
99 1 98 mpbi ⊢ ( ℂ D exp ) : ℂ ⟶ ℂ
100 99 a1i ⊢ ( ⊤ → ( ℂ D exp ) : ℂ ⟶ ℂ )
101 100 feqmptd ⊢ ( ⊤ → ( ℂ D exp ) = ( 𝑥 ∈ ℂ ↦ ( ( ℂ D exp ) ‘ 𝑥 ) ) )
102 ffun ⊢ ( ( ℂ D exp ) : dom ( ℂ D exp ) ⟶ ℂ → Fun ( ℂ D exp ) )
103 1 102 ax-mp ⊢ Fun ( ℂ D exp )
104 funbrfv ⊢ ( Fun ( ℂ D exp ) → ( 𝑥 ( ℂ D exp ) ( exp ‘ 𝑥 ) → ( ( ℂ D exp ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) ) )
105 103 92 104 mpsyl ⊢ ( 𝑥 ∈ ℂ → ( ( ℂ D exp ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
106 105 mpteq2ia ⊢ ( 𝑥 ∈ ℂ ↦ ( ( ℂ D exp ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) )
107 101 106 eqtrdi ⊢ ( ⊤ → ( ℂ D exp ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
108 19 a1i ⊢ ( ⊤ → exp : ℂ ⟶ ℂ )
109 108 feqmptd ⊢ ( ⊤ → exp = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
110 107 109 eqtr4d ⊢ ( ⊤ → ( ℂ D exp ) = exp )
111 110 mptru ⊢ ( ℂ D exp ) = exp