Step | Hyp | Ref
| Expression |
1 | | dvfcn 24224 |
. . . . . . 7
⊢ (ℂ
D exp):dom (ℂ D exp)⟶ℂ |
2 | | dvbsss 24218 |
. . . . . . . . 9
⊢ dom
(ℂ D exp) ⊆ ℂ |
3 | | subcl 10691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) |
4 | 3 | ancoms 451 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) |
5 | | efadd 15313 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (𝑧 − 𝑥) ∈ ℂ) → (exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) |
6 | 4, 5 | syldan 583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) |
7 | | pncan3 10700 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 + (𝑧 − 𝑥)) = 𝑧) |
8 | 7 | fveq2d 6508 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = (exp‘𝑧)) |
9 | 6, 8 | eqtr3d 2818 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥))) = (exp‘𝑧)) |
10 | 9 | mpteq2dva 5027 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ (exp‘𝑧))) |
11 | | cnex 10422 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ℂ
∈ V) |
13 | | fvexd 6519 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘𝑥) ∈
V) |
14 | | fvexd 6519 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈ V) |
15 | | fconstmpt 5468 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥)) |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥))) |
17 | | eqidd 2781 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) |
18 | 12, 13, 14, 16, 17 | offval2 7250 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧 − 𝑥))))) |
19 | | eff 15301 |
. . . . . . . . . . . . . . . 16
⊢
exp:ℂ⟶ℂ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
exp:ℂ⟶ℂ) |
21 | 20 | feqmptd 6568 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → exp =
(𝑧 ∈ ℂ ↦
(exp‘𝑧))) |
22 | 10, 18, 21 | 3eqtr4d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = exp) |
23 | 22 | oveq2d 6998 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (ℂ
D ((ℂ × {(exp‘𝑥)}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) = (ℂ D
exp)) |
24 | | efcl 15302 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
25 | | fconstg 6400 |
. . . . . . . . . . . . . . . 16
⊢
((exp‘𝑥)
∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) |
27 | 24 | snssd 4621 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
{(exp‘𝑥)} ⊆
ℂ) |
28 | 26, 27 | fssd 6363 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶ℂ) |
29 | | ssidd 3882 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ℂ
⊆ ℂ) |
30 | | efcl 15302 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 − 𝑥) ∈ ℂ → (exp‘(𝑧 − 𝑥)) ∈ ℂ) |
31 | 4, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈
ℂ) |
32 | 31 | fmpttd 6708 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))):ℂ⟶ℂ) |
33 | | 0cnd 10438 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 0 ∈
ℂ) |
34 | | 1cnd 10440 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 1 ∈
ℂ) |
35 | | c0ex 10439 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
36 | 35 | snid 4478 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
{0} |
37 | | opelxpi 5448 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
{0}) → 〈𝑥,
0〉 ∈ (ℂ × {0})) |
38 | 36, 37 | mpan2 679 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ × {0})) |
39 | | dvconst 24232 |
. . . . . . . . . . . . . . . . 17
⊢
((exp‘𝑥)
∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) |
40 | 24, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (ℂ
D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) |
41 | 38, 40 | eleqtrrd 2871 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) |
42 | | df-br 4935 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0 ↔
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) |
43 | 41, 42 | sylibr 226 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0) |
44 | 20, 4 | cofmpt 6723 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (exp
∘ (𝑧 ∈ ℂ
↦ (𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) |
45 | 44 | oveq2d 6998 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
D (exp ∘ (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) = (ℂ D (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) |
46 | 4 | fmpttd 6708 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)):ℂ⟶ℂ) |
47 | | oveq1 6989 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 − 𝑥) = (𝑥 − 𝑥)) |
48 | | eqid 2780 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) |
49 | | ovex 7014 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 − 𝑥) ∈ V |
50 | 47, 48, 49 | fvmpt 6601 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = (𝑥 − 𝑥)) |
51 | | subid 10712 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (𝑥 − 𝑥) = 0) |
52 | 50, 51 | eqtrd 2816 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = 0) |
53 | | dveflem 24294 |
. . . . . . . . . . . . . . . . . 18
⊢ 0(ℂ
D exp)1 |
54 | 52, 53 | syl6eqbr 4973 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥)(ℂ D exp)1) |
55 | | 1ex 10441 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
V |
56 | 55 | snid 4478 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
{1} |
57 | | opelxpi 5448 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
{1}) → 〈𝑥,
1〉 ∈ (ℂ × {1})) |
58 | 56, 57 | mpan2 679 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ × {1})) |
59 | | cnelprrecn 10434 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℂ
∈ {ℝ, ℂ} |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
61 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) |
62 | | 1cnd 10440 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) |
63 | 60 | dvmptid 24272 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑧)) = (𝑧 ∈ ℂ ↦ 1)) |
64 | | simpl 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑥 ∈
ℂ) |
65 | | 0cnd 10438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 0 ∈
ℂ) |
66 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
67 | 60, 66 | dvmptc 24273 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑥)) = (𝑧 ∈ ℂ ↦ 0)) |
68 | 60, 61, 62, 63, 64, 65, 67 | dvmptsub 24282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (1 −
0))) |
69 | | 1m0e1 11574 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 0) = 1 |
70 | 69 | mpteq2i 5024 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (𝑧 ∈
ℂ ↦ 1) |
71 | | fconstmpt 5468 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) |
72 | 70, 71 | eqtr4i 2807 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (ℂ × {1}) |
73 | 68, 72 | syl6eq 2832 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (ℂ ×
{1})) |
74 | 58, 73 | eleqtrrd 2871 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ D (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) |
75 | | df-br 4935 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1 ↔ 〈𝑥, 1〉 ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))) |
76 | 74, 75 | sylibr 226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1) |
77 | | eqid 2780 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
78 | 20, 29, 46, 29, 29, 29, 34, 34, 54, 76, 77 | dvcobr 24261 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))(1 · 1)) |
79 | | 1t1e1 11615 |
. . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 |
80 | 78, 79 | syl6breq 4975 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))1) |
81 | 45, 80 | breqdi 4949 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))1) |
82 | 28, 29, 32, 29, 29, 33, 34, 43, 81, 77 | dvmulbr 24254 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) + (1 · ((ℂ ×
{(exp‘𝑥)})‘𝑥)))) |
83 | 32, 66 | ffvelrnd 6683 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥)))‘𝑥) ∈ ℂ) |
84 | 83 | mul02d 10644 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) = 0) |
85 | | fvex 6517 |
. . . . . . . . . . . . . . . . . 18
⊢
(exp‘𝑥) ∈
V |
86 | 85 | fvconst2 6799 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})‘𝑥) = (exp‘𝑥)) |
87 | 86 | oveq2d 6998 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (1 · (exp‘𝑥))) |
88 | 24 | mulid2d 10464 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· (exp‘𝑥)) =
(exp‘𝑥)) |
89 | 87, 88 | eqtrd 2816 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (exp‘𝑥)) |
90 | 84, 89 | oveq12d 7000 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (0 + (exp‘𝑥))) |
91 | 24 | addid2d 10647 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (0 +
(exp‘𝑥)) =
(exp‘𝑥)) |
92 | 90, 91 | eqtrd 2816 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (exp‘𝑥)) |
93 | 82, 92 | breqtrd 4960 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))(exp‘𝑥)) |
94 | 23, 93 | breqdi 4949 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D exp)(exp‘𝑥)) |
95 | | vex 3420 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
96 | 95, 85 | breldm 5631 |
. . . . . . . . . . 11
⊢ (𝑥(ℂ D exp)(exp‘𝑥) → 𝑥 ∈ dom (ℂ D exp)) |
97 | 94, 96 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → 𝑥 ∈ dom (ℂ D
exp)) |
98 | 97 | ssriv 3864 |
. . . . . . . . 9
⊢ ℂ
⊆ dom (ℂ D exp) |
99 | 2, 98 | eqssi 3876 |
. . . . . . . 8
⊢ dom
(ℂ D exp) = ℂ |
100 | 99 | feq2i 6341 |
. . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ ↔ (ℂ D
exp):ℂ⟶ℂ) |
101 | 1, 100 | mpbi 222 |
. . . . . 6
⊢ (ℂ
D exp):ℂ⟶ℂ |
102 | 101 | a1i 11 |
. . . . 5
⊢ (⊤
→ (ℂ D exp):ℂ⟶ℂ) |
103 | 102 | feqmptd 6568 |
. . . 4
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ ((ℂ D exp)‘𝑥))) |
104 | | ffun 6352 |
. . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ → Fun (ℂ D
exp)) |
105 | 1, 104 | ax-mp 5 |
. . . . . 6
⊢ Fun
(ℂ D exp) |
106 | | funbrfv 6551 |
. . . . . 6
⊢ (Fun
(ℂ D exp) → (𝑥(ℂ D exp)(exp‘𝑥) → ((ℂ D exp)‘𝑥) = (exp‘𝑥))) |
107 | 105, 94, 106 | mpsyl 68 |
. . . . 5
⊢ (𝑥 ∈ ℂ → ((ℂ
D exp)‘𝑥) =
(exp‘𝑥)) |
108 | 107 | mpteq2ia 5023 |
. . . 4
⊢ (𝑥 ∈ ℂ ↦
((ℂ D exp)‘𝑥))
= (𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
109 | 103, 108 | syl6eq 2832 |
. . 3
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ (exp‘𝑥))) |
110 | 19 | a1i 11 |
. . . 4
⊢ (⊤
→ exp:ℂ⟶ℂ) |
111 | 110 | feqmptd 6568 |
. . 3
⊢ (⊤
→ exp = (𝑥 ∈
ℂ ↦ (exp‘𝑥))) |
112 | 109, 111 | eqtr4d 2819 |
. 2
⊢ (⊤
→ (ℂ D exp) = exp) |
113 | 112 | mptru 1515 |
1
⊢ (ℂ
D exp) = exp |