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 0cnd ⊢ ( 𝑥 ∈ ℂ → 0 ∈ ℂ )
34 1cnd ⊢ ( 𝑥 ∈ ℂ → 1 ∈ ℂ )
35 c0ex ⊢ 0 ∈ V
36 35 snid ⊢ 0 ∈ { 0 }
37 opelxpi ⊢ ( ( 𝑥 ∈ ℂ ∧ 0 ∈ { 0 } ) → ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ × { 0 } ) )
38 36 37 mpan2 ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ × { 0 } ) )
39 dvconst ⊢ ( ( exp ‘ 𝑥 ) ∈ ℂ → ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) = ( ℂ × { 0 } ) )
40 24 39 syl ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) = ( ℂ × { 0 } ) )
41 38 40 eleqtrrd ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) )
42 df-br ⊢ ( 𝑥 ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) 0 ↔ ⟨ 𝑥 , 0 ⟩ ∈ ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) )
43 41 42 sylibr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( ℂ × { ( exp ‘ 𝑥 ) } ) ) 0 )
44 20 4 cofmpt ⊢ ( 𝑥 ∈ ℂ → ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) )
45 44 oveq2d ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) ) = ( ℂ D ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) )
46 4 fmpttd ⊢ ( 𝑥 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) : ℂ ⟶ ℂ )
47 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 − 𝑥 ) = ( 𝑥 − 𝑥 ) )
48 eqid ⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) )
49 ovex ⊢ ( 𝑥 − 𝑥 ) ∈ V
50 47 48 49 fvmpt ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ‘ 𝑥 ) = ( 𝑥 − 𝑥 ) )
51 subid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 𝑥 ) = 0 )
52 50 51 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ‘ 𝑥 ) = 0 )
53 dveflem ⊢ 0 ( ℂ D exp ) 1
54 52 53 eqbrtrdi ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ‘ 𝑥 ) ( ℂ D exp ) 1 )
55 1ex ⊢ 1 ∈ V
56 55 snid ⊢ 1 ∈ { 1 }
57 opelxpi ⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ { 1 } ) → ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ × { 1 } ) )
58 56 57 mpan2 ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ × { 1 } ) )
59 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
60 59 a1i ⊢ ( 𝑥 ∈ ℂ → ℂ ∈ { ℝ , ℂ } )
61 simpr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
62 1cnd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 1 ∈ ℂ )
63 60 dvmptid ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ 𝑧 ) ) = ( 𝑧 ∈ ℂ ↦ 1 ) )
64 simpl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝑥 ∈ ℂ )
65 0cnd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 0 ∈ ℂ )
66 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
67 60 66 dvmptc ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑧 ∈ ℂ ↦ 0 ) )
68 60 61 62 63 64 65 67 dvmptsub ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 1 − 0 ) ) )
69 1m0e1 ⊢ ( 1 − 0 ) = 1
70 69 mpteq2i ⊢ ( 𝑧 ∈ ℂ ↦ ( 1 − 0 ) ) = ( 𝑧 ∈ ℂ ↦ 1 )
71 fconstmpt ⊢ ( ℂ × { 1 } ) = ( 𝑧 ∈ ℂ ↦ 1 )
72 70 71 eqtr4i ⊢ ( 𝑧 ∈ ℂ ↦ ( 1 − 0 ) ) = ( ℂ × { 1 } )
73 68 72 eqtrdi ⊢ ( 𝑥 ∈ ℂ → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) = ( ℂ × { 1 } ) )
74 58 73 eleqtrrd ⊢ ( 𝑥 ∈ ℂ → ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) )
75 df-br ⊢ ( 𝑥 ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) 1 ↔ ⟨ 𝑥 , 1 ⟩ ∈ ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) )
76 74 75 sylibr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) 1 )
77 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
78 20 29 46 29 29 29 34 34 54 76 77 dvcobr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) ) ( 1 · 1 ) )
79 1t1e1 ⊢ ( 1 · 1 ) = 1
80 78 79 breqtrdi ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( exp ∘ ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝑥 ) ) ) ) 1 )
81 45 80 breqdi ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) 1 )
82 28 29 32 29 29 33 34 43 81 77 dvmulbr ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) ) ( ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) + ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) ) )
83 32 66 ffvelrnd ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ∈ ℂ )
84 83 mul02d ⊢ ( 𝑥 ∈ ℂ → ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) = 0 )
85 fvex ⊢ ( exp ‘ 𝑥 ) ∈ V
86 85 fvconst2 ⊢ ( 𝑥 ∈ ℂ → ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
87 86 oveq2d ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) = ( 1 · ( exp ‘ 𝑥 ) ) )
88 24 mulid2d ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( exp ‘ 𝑥 ) ) = ( exp ‘ 𝑥 ) )
89 87 88 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) = ( exp ‘ 𝑥 ) )
90 84 89 oveq12d ⊢ ( 𝑥 ∈ ℂ → ( ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) + ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) ) = ( 0 + ( exp ‘ 𝑥 ) ) )
91 24 addid2d ⊢ ( 𝑥 ∈ ℂ → ( 0 + ( exp ‘ 𝑥 ) ) = ( exp ‘ 𝑥 ) )
92 90 91 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( ( 0 · ( ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ‘ 𝑥 ) ) + ( 1 · ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ‘ 𝑥 ) ) ) = ( exp ‘ 𝑥 ) )
93 82 92 breqtrd ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D ( ( ℂ × { ( exp ‘ 𝑥 ) } ) ∘f · ( 𝑧 ∈ ℂ ↦ ( exp ‘ ( 𝑧 − 𝑥 ) ) ) ) ) ( exp ‘ 𝑥 ) )
94 23 93 breqdi ⊢ ( 𝑥 ∈ ℂ → 𝑥 ( ℂ D exp ) ( exp ‘ 𝑥 ) )
95 vex ⊢ 𝑥 ∈ V
96 95 85 breldm ⊢ ( 𝑥 ( ℂ D exp ) ( exp ‘ 𝑥 ) → 𝑥 ∈ dom ( ℂ D exp ) )
97 94 96 syl ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ dom ( ℂ D exp ) )
98 97 ssriv ⊢ ℂ ⊆ dom ( ℂ D exp )
99 2 98 eqssi ⊢ dom ( ℂ D exp ) = ℂ
100 99 feq2i ⊢ ( ( ℂ D exp ) : dom ( ℂ D exp ) ⟶ ℂ ↔ ( ℂ D exp ) : ℂ ⟶ ℂ )
101 1 100 mpbi ⊢ ( ℂ D exp ) : ℂ ⟶ ℂ
102 101 a1i ⊢ ( ⊤ → ( ℂ D exp ) : ℂ ⟶ ℂ )
103 102 feqmptd ⊢ ( ⊤ → ( ℂ D exp ) = ( 𝑥 ∈ ℂ ↦ ( ( ℂ D exp ) ‘ 𝑥 ) ) )
104 ffun ⊢ ( ( ℂ D exp ) : dom ( ℂ D exp ) ⟶ ℂ → Fun ( ℂ D exp ) )
105 1 104 ax-mp ⊢ Fun ( ℂ D exp )
106 funbrfv ⊢ ( Fun ( ℂ D exp ) → ( 𝑥 ( ℂ D exp ) ( exp ‘ 𝑥 ) → ( ( ℂ D exp ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) ) )
107 105 94 106 mpsyl ⊢ ( 𝑥 ∈ ℂ → ( ( ℂ D exp ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
108 107 mpteq2ia ⊢ ( 𝑥 ∈ ℂ ↦ ( ( ℂ D exp ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) )
109 103 108 eqtrdi ⊢ ( ⊤ → ( ℂ D exp ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
110 19 a1i ⊢ ( ⊤ → exp : ℂ ⟶ ℂ )
111 110 feqmptd ⊢ ( ⊤ → exp = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
112 109 111 eqtr4d ⊢ ( ⊤ → ( ℂ D exp ) = exp )
113 112 mptru ⊢ ( ℂ D exp ) = exp