Step | Hyp | Ref
| Expression |
1 | | dvfcn 25757 |
. . . . . . 7
⊢ (ℂ
D exp):dom (ℂ D exp)⟶ℂ |
2 | | dvbsss 25751 |
. . . . . . . . 9
⊢ dom
(ℂ D exp) ⊆ ℂ |
3 | | subcl 11466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) |
4 | 3 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) |
5 | | efadd 16044 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (𝑧 − 𝑥) ∈ ℂ) → (exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) |
6 | 4, 5 | syldan 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) |
7 | | pncan3 11475 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 + (𝑧 − 𝑥)) = 𝑧) |
8 | 7 | fveq2d 6895 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = (exp‘𝑧)) |
9 | 6, 8 | eqtr3d 2773 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥))) = (exp‘𝑧)) |
10 | 9 | mpteq2dva 5248 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ (exp‘𝑧))) |
11 | | cnex 11197 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ℂ
∈ V) |
13 | | fvexd 6906 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘𝑥) ∈
V) |
14 | | fvexd 6906 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈ V) |
15 | | fconstmpt 5738 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥)) |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥))) |
17 | | eqidd 2732 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) |
18 | 12, 13, 14, 16, 17 | offval2 7694 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧 − 𝑥))))) |
19 | | eff 16032 |
. . . . . . . . . . . . . . . 16
⊢
exp:ℂ⟶ℂ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
exp:ℂ⟶ℂ) |
21 | 20 | feqmptd 6960 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → exp =
(𝑧 ∈ ℂ ↦
(exp‘𝑧))) |
22 | 10, 18, 21 | 3eqtr4d 2781 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = exp) |
23 | 22 | oveq2d 7428 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (ℂ
D ((ℂ × {(exp‘𝑥)}) ∘f · (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) = (ℂ D
exp)) |
24 | | efcl 16033 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
25 | | fconstg 6778 |
. . . . . . . . . . . . . . . 16
⊢
((exp‘𝑥)
∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) |
27 | 24 | snssd 4812 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
{(exp‘𝑥)} ⊆
ℂ) |
28 | 26, 27 | fssd 6735 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶ℂ) |
29 | | ssidd 4005 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ℂ
⊆ ℂ) |
30 | | efcl 16033 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 − 𝑥) ∈ ℂ → (exp‘(𝑧 − 𝑥)) ∈ ℂ) |
31 | 4, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈
ℂ) |
32 | 31 | fmpttd 7116 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))):ℂ⟶ℂ) |
33 | | c0ex 11215 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
34 | 33 | snid 4664 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
{0} |
35 | | opelxpi 5713 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
{0}) → 〈𝑥,
0〉 ∈ (ℂ × {0})) |
36 | 34, 35 | mpan2 688 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ × {0})) |
37 | | dvconst 25766 |
. . . . . . . . . . . . . . . . 17
⊢
((exp‘𝑥)
∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) |
38 | 24, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (ℂ
D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) |
39 | 36, 38 | eleqtrrd 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) |
40 | | df-br 5149 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0 ↔
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) |
41 | 39, 40 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0) |
42 | 20, 4 | cofmpt 7132 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (exp
∘ (𝑧 ∈ ℂ
↦ (𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) |
43 | 42 | oveq2d 7428 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
D (exp ∘ (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) = (ℂ D (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) |
44 | 4 | fmpttd 7116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)):ℂ⟶ℂ) |
45 | | oveq1 7419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 − 𝑥) = (𝑥 − 𝑥)) |
46 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) |
47 | | ovex 7445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 − 𝑥) ∈ V |
48 | 45, 46, 47 | fvmpt 6998 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = (𝑥 − 𝑥)) |
49 | | subid 11486 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (𝑥 − 𝑥) = 0) |
50 | 48, 49 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = 0) |
51 | | dveflem 25831 |
. . . . . . . . . . . . . . . . . 18
⊢ 0(ℂ
D exp)1 |
52 | 50, 51 | eqbrtrdi 5187 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥)(ℂ D exp)1) |
53 | | 1ex 11217 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
V |
54 | 53 | snid 4664 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
{1} |
55 | | opelxpi 5713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
{1}) → 〈𝑥,
1〉 ∈ (ℂ × {1})) |
56 | 54, 55 | mpan2 688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ × {1})) |
57 | | cnelprrecn 11209 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℂ
∈ {ℝ, ℂ} |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
59 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) |
60 | | 1cnd 11216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) |
61 | 58 | dvmptid 25809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑧)) = (𝑧 ∈ ℂ ↦ 1)) |
62 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑥 ∈
ℂ) |
63 | | 0cnd 11214 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 0 ∈
ℂ) |
64 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
65 | 58, 64 | dvmptc 25810 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑥)) = (𝑧 ∈ ℂ ↦ 0)) |
66 | 58, 59, 60, 61, 62, 63, 65 | dvmptsub 25819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (1 −
0))) |
67 | | 1m0e1 12340 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 0) = 1 |
68 | 67 | mpteq2i 5253 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (𝑧 ∈
ℂ ↦ 1) |
69 | | fconstmpt 5738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) |
70 | 68, 69 | eqtr4i 2762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (ℂ × {1}) |
71 | 66, 70 | eqtrdi 2787 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (ℂ ×
{1})) |
72 | 56, 71 | eleqtrrd 2835 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ D (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) |
73 | | df-br 5149 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1 ↔ 〈𝑥, 1〉 ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))) |
74 | 72, 73 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1) |
75 | | eqid 2731 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
76 | 20, 29, 44, 29, 29, 29, 52, 74, 75 | dvcobr 25797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))(1 · 1)) |
77 | | 1t1e1 12381 |
. . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 |
78 | 76, 77 | breqtrdi 5189 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))1) |
79 | 43, 78 | breqdi 5163 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))1) |
80 | 28, 29, 32, 29, 29, 41, 79, 75 | dvmulbr 25789 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) + (1 · ((ℂ ×
{(exp‘𝑥)})‘𝑥)))) |
81 | 32, 64 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥)))‘𝑥) ∈ ℂ) |
82 | 81 | mul02d 11419 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) = 0) |
83 | | fvex 6904 |
. . . . . . . . . . . . . . . . . 18
⊢
(exp‘𝑥) ∈
V |
84 | 83 | fvconst2 7207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})‘𝑥) = (exp‘𝑥)) |
85 | 84 | oveq2d 7428 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (1 · (exp‘𝑥))) |
86 | 24 | mullidd 11239 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· (exp‘𝑥)) =
(exp‘𝑥)) |
87 | 85, 86 | eqtrd 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (exp‘𝑥)) |
88 | 82, 87 | oveq12d 7430 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (0 + (exp‘𝑥))) |
89 | 24 | addlidd 11422 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (0 +
(exp‘𝑥)) =
(exp‘𝑥)) |
90 | 88, 89 | eqtrd 2771 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (exp‘𝑥)) |
91 | 80, 90 | breqtrd 5174 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))(exp‘𝑥)) |
92 | 23, 91 | breqdi 5163 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D exp)(exp‘𝑥)) |
93 | | vex 3477 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
94 | 93, 83 | breldm 5908 |
. . . . . . . . . . 11
⊢ (𝑥(ℂ D exp)(exp‘𝑥) → 𝑥 ∈ dom (ℂ D exp)) |
95 | 92, 94 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → 𝑥 ∈ dom (ℂ D
exp)) |
96 | 95 | ssriv 3986 |
. . . . . . . . 9
⊢ ℂ
⊆ dom (ℂ D exp) |
97 | 2, 96 | eqssi 3998 |
. . . . . . . 8
⊢ dom
(ℂ D exp) = ℂ |
98 | 97 | feq2i 6709 |
. . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ ↔ (ℂ D
exp):ℂ⟶ℂ) |
99 | 1, 98 | mpbi 229 |
. . . . . 6
⊢ (ℂ
D exp):ℂ⟶ℂ |
100 | 99 | a1i 11 |
. . . . 5
⊢ (⊤
→ (ℂ D exp):ℂ⟶ℂ) |
101 | 100 | feqmptd 6960 |
. . . 4
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ ((ℂ D exp)‘𝑥))) |
102 | | ffun 6720 |
. . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ → Fun (ℂ D
exp)) |
103 | 1, 102 | ax-mp 5 |
. . . . . 6
⊢ Fun
(ℂ D exp) |
104 | | funbrfv 6942 |
. . . . . 6
⊢ (Fun
(ℂ D exp) → (𝑥(ℂ D exp)(exp‘𝑥) → ((ℂ D exp)‘𝑥) = (exp‘𝑥))) |
105 | 103, 92, 104 | mpsyl 68 |
. . . . 5
⊢ (𝑥 ∈ ℂ → ((ℂ
D exp)‘𝑥) =
(exp‘𝑥)) |
106 | 105 | mpteq2ia 5251 |
. . . 4
⊢ (𝑥 ∈ ℂ ↦
((ℂ D exp)‘𝑥))
= (𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
107 | 101, 106 | eqtrdi 2787 |
. . 3
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ (exp‘𝑥))) |
108 | 19 | a1i 11 |
. . . 4
⊢ (⊤
→ exp:ℂ⟶ℂ) |
109 | 108 | feqmptd 6960 |
. . 3
⊢ (⊤
→ exp = (𝑥 ∈
ℂ ↦ (exp‘𝑥))) |
110 | 107, 109 | eqtr4d 2774 |
. 2
⊢ (⊤
→ (ℂ D exp) = exp) |
111 | 110 | mptru 1547 |
1
⊢ (ℂ
D exp) = exp |