Step | Hyp | Ref
| Expression |
1 | | dvfcn 23478 |
. . . . . . 7
⊢ (ℂ
D exp):dom (ℂ D exp)⟶ℂ |
2 | | dvbsss 23472 |
. . . . . . . . 9
⊢ dom
(ℂ D exp) ⊆ ℂ |
3 | | efcl 14652 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
4 | | fconstg 6005 |
. . . . . . . . . . . . . . . 16
⊢
((exp‘𝑥)
∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) |
6 | 3 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
{(exp‘𝑥)} ⊆
ℂ) |
7 | 5, 6 | fssd 5970 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶ℂ) |
8 | | ssid 3587 |
. . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ |
9 | 8 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ℂ
⊆ ℂ) |
10 | | subcl 10159 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) |
11 | 10 | ancoms 468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) |
12 | | efcl 14652 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 − 𝑥) ∈ ℂ → (exp‘(𝑧 − 𝑥)) ∈ ℂ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈
ℂ) |
14 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))) |
15 | 13, 14 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))):ℂ⟶ℂ) |
16 | | 0cn 9911 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℂ |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 0 ∈
ℂ) |
18 | | ax-1cn 9873 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 1 ∈
ℂ) |
20 | 16 | elexi 3186 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
21 | 20 | snid 4155 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
{0} |
22 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
{0}) → 〈𝑥,
0〉 ∈ (ℂ × {0})) |
23 | 21, 22 | mpan2 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ × {0})) |
24 | | dvconst 23486 |
. . . . . . . . . . . . . . . . 17
⊢
((exp‘𝑥)
∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) |
25 | 3, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (ℂ
D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) |
26 | 23, 25 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) |
27 | | df-br 4584 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0 ↔
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) |
28 | 26, 27 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0) |
29 | | eff 14651 |
. . . . . . . . . . . . . . . . . 18
⊢
exp:ℂ⟶ℂ |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
exp:ℂ⟶ℂ) |
31 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) |
32 | 11, 31 | fmptd 6292 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)):ℂ⟶ℂ) |
33 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 − 𝑥) = (𝑥 − 𝑥)) |
34 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 − 𝑥) ∈ V |
35 | 33, 31, 34 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = (𝑥 − 𝑥)) |
36 | | subid 10179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (𝑥 − 𝑥) = 0) |
37 | 35, 36 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = 0) |
38 | | dveflem 23546 |
. . . . . . . . . . . . . . . . . 18
⊢ 0(ℂ
D exp)1 |
39 | 37, 38 | syl6eqbr 4622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥)(ℂ D exp)1) |
40 | 18 | elexi 3186 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
V |
41 | 40 | snid 4155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
{1} |
42 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
{1}) → 〈𝑥,
1〉 ∈ (ℂ × {1})) |
43 | 41, 42 | mpan2 703 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ × {1})) |
44 | | cnelprrecn 9908 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℂ
∈ {ℝ, ℂ} |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
46 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) |
47 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) |
48 | 45 | dvmptid 23526 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑧)) = (𝑧 ∈ ℂ ↦ 1)) |
49 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑥 ∈
ℂ) |
50 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 0 ∈
ℂ) |
51 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
52 | 45, 51 | dvmptc 23527 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑥)) = (𝑧 ∈ ℂ ↦ 0)) |
53 | 45, 46, 47, 48, 49, 50, 52 | dvmptsub 23536 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (1 −
0))) |
54 | | 1m0e1 11008 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 0) = 1 |
55 | 54 | mpteq2i 4669 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (𝑧 ∈
ℂ ↦ 1) |
56 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) |
57 | 55, 56 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (ℂ × {1}) |
58 | 53, 57 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (ℂ ×
{1})) |
59 | 43, 58 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ D (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) |
60 | | df-br 4584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1 ↔ 〈𝑥, 1〉 ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))) |
61 | 59, 60 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1) |
62 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
63 | 30, 9, 32, 9, 9, 9,
19, 19, 39, 61, 62 | dvcobr 23515 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))(1 · 1)) |
64 | | 1t1e1 11052 |
. . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 |
65 | 63, 64 | syl6breq 4624 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))1) |
66 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))) |
67 | 30 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → exp =
(𝑦 ∈ ℂ ↦
(exp‘𝑦))) |
68 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑧 − 𝑥) → (exp‘𝑦) = (exp‘(𝑧 − 𝑥))) |
69 | 11, 66, 67, 68 | fmptco 6303 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (exp
∘ (𝑧 ∈ ℂ
↦ (𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) |
70 | 69 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (ℂ
D (exp ∘ (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) = (ℂ D (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) |
71 | 70 | breqd 4594 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))1 ↔ 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))1)) |
72 | 65, 71 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))1) |
73 | 7, 9, 15, 9, 9, 17, 19, 28, 72, 62 | dvmulbr 23508 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) + (1 · ((ℂ ×
{(exp‘𝑥)})‘𝑥)))) |
74 | 15, 51 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥)))‘𝑥) ∈ ℂ) |
75 | 74 | mul02d 10113 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) = 0) |
76 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢
(exp‘𝑥) ∈
V |
77 | 76 | fvconst2 6374 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})‘𝑥) = (exp‘𝑥)) |
78 | 77 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (1 · (exp‘𝑥))) |
79 | 3 | mulid2d 9937 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· (exp‘𝑥)) =
(exp‘𝑥)) |
80 | 78, 79 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (exp‘𝑥)) |
81 | 75, 80 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (0 + (exp‘𝑥))) |
82 | 3 | addid2d 10116 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (0 +
(exp‘𝑥)) =
(exp‘𝑥)) |
83 | 81, 82 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (exp‘𝑥)) |
84 | 73, 83 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))(exp‘𝑥)) |
85 | | cnex 9896 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → ℂ
∈ V) |
87 | 76 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘𝑥) ∈
V) |
88 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(exp‘(𝑧
− 𝑥)) ∈
V |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈ V) |
90 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥)) |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥))) |
92 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) |
93 | 86, 87, 89, 91, 92 | offval2 6812 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧 − 𝑥))))) |
94 | 30 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → exp =
(𝑧 ∈ ℂ ↦
(exp‘𝑧))) |
95 | | efadd 14663 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ (𝑧 − 𝑥) ∈ ℂ) → (exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) |
96 | 11, 95 | syldan 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) |
97 | | pncan3 10168 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 + (𝑧 − 𝑥)) = 𝑧) |
98 | 97 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = (exp‘𝑧)) |
99 | 96, 98 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥))) = (exp‘𝑧)) |
100 | 99 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ (exp‘𝑧))) |
101 | 94, 100 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → exp =
(𝑧 ∈ ℂ ↦
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥))))) |
102 | 93, 101 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = exp) |
103 | 102 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (ℂ
D ((ℂ × {(exp‘𝑥)}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) = (ℂ D
exp)) |
104 | 103 | breqd 4594 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))(exp‘𝑥) ↔ 𝑥(ℂ D exp)(exp‘𝑥))) |
105 | 84, 104 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D exp)(exp‘𝑥)) |
106 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
107 | 106, 76 | breldm 5251 |
. . . . . . . . . . 11
⊢ (𝑥(ℂ D exp)(exp‘𝑥) → 𝑥 ∈ dom (ℂ D exp)) |
108 | 105, 107 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → 𝑥 ∈ dom (ℂ D
exp)) |
109 | 108 | ssriv 3572 |
. . . . . . . . 9
⊢ ℂ
⊆ dom (ℂ D exp) |
110 | 2, 109 | eqssi 3584 |
. . . . . . . 8
⊢ dom
(ℂ D exp) = ℂ |
111 | 110 | feq2i 5950 |
. . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ ↔ (ℂ D
exp):ℂ⟶ℂ) |
112 | 1, 111 | mpbi 219 |
. . . . . 6
⊢ (ℂ
D exp):ℂ⟶ℂ |
113 | 112 | a1i 11 |
. . . . 5
⊢ (⊤
→ (ℂ D exp):ℂ⟶ℂ) |
114 | 113 | feqmptd 6159 |
. . . 4
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ ((ℂ D exp)‘𝑥))) |
115 | | ffun 5961 |
. . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ → Fun (ℂ D
exp)) |
116 | 1, 115 | ax-mp 5 |
. . . . . 6
⊢ Fun
(ℂ D exp) |
117 | | funbrfv 6144 |
. . . . . 6
⊢ (Fun
(ℂ D exp) → (𝑥(ℂ D exp)(exp‘𝑥) → ((ℂ D exp)‘𝑥) = (exp‘𝑥))) |
118 | 116, 105,
117 | mpsyl 66 |
. . . . 5
⊢ (𝑥 ∈ ℂ → ((ℂ
D exp)‘𝑥) =
(exp‘𝑥)) |
119 | 118 | mpteq2ia 4668 |
. . . 4
⊢ (𝑥 ∈ ℂ ↦
((ℂ D exp)‘𝑥))
= (𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
120 | 114, 119 | syl6eq 2660 |
. . 3
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ (exp‘𝑥))) |
121 | 29 | a1i 11 |
. . . 4
⊢ (⊤
→ exp:ℂ⟶ℂ) |
122 | 121 | feqmptd 6159 |
. . 3
⊢ (⊤
→ exp = (𝑥 ∈
ℂ ↦ (exp‘𝑥))) |
123 | 120, 122 | eqtr4d 2647 |
. 2
⊢ (⊤
→ (ℂ D exp) = exp) |
124 | 123 | trud 1484 |
1
⊢ (ℂ
D exp) = exp |