Step | Hyp | Ref
| Expression |
1 | | dvfcn 24109 |
. . . 4
⊢ (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ |
2 | | ssidd 3843 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ℂ
⊆ ℂ) |
3 | | eldifsn 4550 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℂ ∖ {0})
↔ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
4 | | divcl 11039 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝐴 / 𝑥) ∈ ℂ) |
5 | 4 | 3expb 1110 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (𝐴 / 𝑥) ∈ ℂ) |
6 | 3, 5 | sylan2b 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝐴 / 𝑥) ∈
ℂ) |
7 | 6 | fmpttd 6649 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)):(ℂ ∖
{0})⟶ℂ) |
8 | | difssd 3961 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
∖ {0}) ⊆ ℂ) |
9 | 2, 7, 8 | dvbss 24102 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) ⊆ (ℂ ∖
{0})) |
10 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈ (ℂ
∖ {0})) |
11 | | eqid 2778 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
12 | 11 | cnfldtop 22995 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Top |
13 | 11 | cnfldhaus 22996 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈ Haus |
14 | | 0cn 10368 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
15 | 11 | cnfldtopon 22994 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
16 | 15 | toponunii 21128 |
. . . . . . . . . . . . 13
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
17 | 16 | sncld 21583 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Haus ∧ 0 ∈
ℂ) → {0} ∈
(Clsd‘(TopOpen‘ℂfld))) |
18 | 13, 14, 17 | mp2an 682 |
. . . . . . . . . . 11
⊢ {0}
∈ (Clsd‘(TopOpen‘ℂfld)) |
19 | 16 | cldopn 21243 |
. . . . . . . . . . 11
⊢ ({0}
∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld) |
21 | | isopn3i 21294 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘(ℂ ∖ {0}))
= (ℂ ∖ {0})) |
22 | 12, 20, 21 | mp2an 682 |
. . . . . . . . 9
⊢
((int‘(TopOpen‘ℂfld))‘(ℂ
∖ {0})) = (ℂ ∖ {0}) |
23 | 10, 22 | syl6eleqr 2870 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈
((int‘(TopOpen‘ℂfld))‘(ℂ ∖
{0}))) |
24 | | eldifi 3955 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈
ℂ) |
25 | 24 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈
ℂ) |
26 | 25 | sqvald 13324 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑦↑2) = (𝑦 · 𝑦)) |
27 | 26 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / (𝑦↑2)) = (𝐴 / (𝑦 · 𝑦))) |
28 | | simpl 476 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝐴 ∈
ℂ) |
29 | | eldifsni 4553 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ≠
0) |
30 | 29 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ≠
0) |
31 | 28, 25, 25, 30, 30 | divdiv1d 11182 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝐴 / 𝑦) / 𝑦) = (𝐴 / (𝑦 · 𝑦))) |
32 | 27, 31 | eqtr4d 2817 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / (𝑦↑2)) = ((𝐴 / 𝑦) / 𝑦)) |
33 | 32 | negeqd 10616 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) = -((𝐴 / 𝑦) / 𝑦)) |
34 | 28, 25, 30 | divcld 11151 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / 𝑦) ∈
ℂ) |
35 | 34, 25, 30 | divnegd 11164 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -((𝐴 / 𝑦) / 𝑦) = (-(𝐴 / 𝑦) / 𝑦)) |
36 | 33, 35 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) = (-(𝐴 / 𝑦) / 𝑦)) |
37 | 34 | negcld 10721 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / 𝑦) ∈
ℂ) |
38 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) |
39 | 38 | cdivcncf 23128 |
. . . . . . . . . . . 12
⊢ (-(𝐴 / 𝑦) ∈ ℂ → (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ)) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ)) |
41 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (-(𝐴 / 𝑦) / 𝑧) = (-(𝐴 / 𝑦) / 𝑦)) |
42 | 40, 10, 41 | cnmptlimc 24091 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (-(𝐴 / 𝑦) / 𝑦) ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) limℂ 𝑦)) |
43 | 36, 42 | eqeltrd 2859 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) limℂ 𝑦)) |
44 | | cncff 23104 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ) → (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
45 | 40, 44 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
46 | 45 | limcdif 24077 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) limℂ 𝑦) = (((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) limℂ
𝑦)) |
47 | | eldifi 3955 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) → 𝑧 ∈ (ℂ ∖
{0})) |
48 | 47 | adantl 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ∈ (ℂ
∖ {0})) |
49 | 48 | eldifad 3804 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ∈
ℂ) |
50 | 24 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑦 ∈
ℂ) |
51 | 49, 50 | subcld 10734 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 − 𝑦) ∈
ℂ) |
52 | 34 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝐴 / 𝑦) ∈
ℂ) |
53 | | eldifsni 4553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
54 | 48, 53 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ≠
0) |
55 | 52, 49, 54 | divcld 11151 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝐴 / 𝑦) / 𝑧) ∈ ℂ) |
56 | | mulneg12 10813 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 − 𝑦) ∈ ℂ ∧ ((𝐴 / 𝑦) / 𝑧) ∈ ℂ) → (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧))) |
57 | 51, 55, 56 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧))) |
58 | 50, 49, 55 | subdird 10832 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 − 𝑧) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑦 · ((𝐴 / 𝑦) / 𝑧)) − (𝑧 · ((𝐴 / 𝑦) / 𝑧)))) |
59 | 49, 50 | negsubdi2d 10750 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -(𝑧 − 𝑦) = (𝑦 − 𝑧)) |
60 | 59 | oveq1d 6937 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑦 − 𝑧) · ((𝐴 / 𝑦) / 𝑧))) |
61 | | oveq2 6930 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (𝐴 / 𝑥) = (𝐴 / 𝑧)) |
62 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)) |
63 | | ovex 6954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 / 𝑧) ∈ V |
64 | 61, 62, 63 | fvmpt 6542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝐴 / 𝑧)) |
65 | 48, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝐴 / 𝑧)) |
66 | | simpll 757 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝐴 ∈
ℂ) |
67 | 29 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑦 ≠
0) |
68 | 66, 50, 67 | divcan2d 11153 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑦 · (𝐴 / 𝑦)) = 𝐴) |
69 | 68 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 · (𝐴 / 𝑦)) / 𝑧) = (𝐴 / 𝑧)) |
70 | 50, 52, 49, 54 | divassd 11186 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 · (𝐴 / 𝑦)) / 𝑧) = (𝑦 · ((𝐴 / 𝑦) / 𝑧))) |
71 | 65, 69, 70 | 3eqtr2d 2820 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝑦 · ((𝐴 / 𝑦) / 𝑧))) |
72 | | oveq2 6930 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (𝐴 / 𝑥) = (𝐴 / 𝑦)) |
73 | | ovex 6954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 / 𝑦) ∈ V |
74 | 72, 62, 73 | fvmpt 6542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝐴 / 𝑦)) |
75 | 74 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝐴 / 𝑦)) |
76 | 52, 49, 54 | divcan2d 11153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 · ((𝐴 / 𝑦) / 𝑧)) = (𝐴 / 𝑦)) |
77 | 75, 76 | eqtr4d 2817 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝑧 · ((𝐴 / 𝑦) / 𝑧))) |
78 | 71, 77 | oveq12d 6940 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) = ((𝑦 · ((𝐴 / 𝑦) / 𝑧)) − (𝑧 · ((𝐴 / 𝑦) / 𝑧)))) |
79 | 58, 60, 78 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = (((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦))) |
80 | 52, 49, 54 | divnegd 11164 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -((𝐴 / 𝑦) / 𝑧) = (-(𝐴 / 𝑦) / 𝑧)) |
81 | 80 | oveq2d 6938 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧))) |
82 | 57, 79, 81 | 3eqtr3d 2822 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) = ((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧))) |
83 | 82 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦)) = (((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧)) / (𝑧 − 𝑦))) |
84 | 52 | negcld 10721 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -(𝐴 / 𝑦) ∈
ℂ) |
85 | 84, 49, 54 | divcld 11151 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝐴 / 𝑦) / 𝑧) ∈ ℂ) |
86 | | eldifsni 4553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) → 𝑧 ≠ 𝑦) |
87 | 86 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ≠ 𝑦) |
88 | 49, 50, 87 | subne0d 10743 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 − 𝑦) ≠ 0) |
89 | 85, 51, 88 | divcan3d 11156 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧)) / (𝑧 − 𝑦)) = (-(𝐴 / 𝑦) / 𝑧)) |
90 | 83, 89 | eqtrd 2814 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦)) = (-(𝐴 / 𝑦) / 𝑧)) |
91 | 90 | mpteq2dva 4979 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧))) |
92 | | difss 3960 |
. . . . . . . . . . . . 13
⊢ ((ℂ
∖ {0}) ∖ {𝑦})
⊆ (ℂ ∖ {0}) |
93 | | resmpt 5699 |
. . . . . . . . . . . . 13
⊢
(((ℂ ∖ {0}) ∖ {𝑦}) ⊆ (ℂ ∖ {0}) →
((𝑧 ∈ (ℂ ∖
{0}) ↦ (-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧)) |
95 | 91, 94 | syl6eqr 2832 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = ((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦}))) |
96 | 95 | oveq1d 6937 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦) = (((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) limℂ
𝑦)) |
97 | 46, 96 | eqtr4d 2817 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) limℂ 𝑦) = ((𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ ((((𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)) |
98 | 43, 97 | eleqtrd 2861 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)) |
99 | 15 | toponrestid 21133 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
100 | | eqid 2778 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ ((((𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) |
101 | | ssidd 3843 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ℂ ⊆ ℂ) |
102 | 7 | adantr 474 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥)):(ℂ ∖
{0})⟶ℂ) |
103 | | difssd 3961 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (ℂ ∖ {0}) ⊆ ℂ) |
104 | 99, 11, 100, 101, 102, 103 | eldv 24099 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) ↔ (𝑦 ∈
((int‘(TopOpen‘ℂfld))‘(ℂ ∖ {0}))
∧ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)))) |
105 | 23, 98, 104 | mpbir2and 703 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2))) |
106 | | vex 3401 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
107 | | negex 10620 |
. . . . . . . 8
⊢ -(𝐴 / (𝑦↑2)) ∈ V |
108 | 106, 107 | breldm 5574 |
. . . . . . 7
⊢ (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) → 𝑦 ∈ dom (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
109 | 105, 108 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈ dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
110 | 9, 109 | eqelssd 3841 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) = (ℂ ∖ {0})) |
111 | 110 | feq2d 6277 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ ↔
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))):(ℂ ∖
{0})⟶ℂ)) |
112 | 1, 111 | mpbii 225 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):(ℂ ∖
{0})⟶ℂ) |
113 | 112 | ffnd 6292 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))) Fn (ℂ ∖
{0})) |
114 | | negex 10620 |
. . . 4
⊢ -(𝐴 / (𝑥↑2)) ∈ V |
115 | 114 | rgenw 3106 |
. . 3
⊢
∀𝑥 ∈
(ℂ ∖ {0})-(𝐴 /
(𝑥↑2)) ∈
V |
116 | | eqid 2778 |
. . . 4
⊢ (𝑥 ∈ (ℂ ∖ {0})
↦ -(𝐴 / (𝑥↑2))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2))) |
117 | 116 | fnmpt 6266 |
. . 3
⊢
(∀𝑥 ∈
(ℂ ∖ {0})-(𝐴 /
(𝑥↑2)) ∈ V →
(𝑥 ∈ (ℂ ∖
{0}) ↦ -(𝐴 / (𝑥↑2))) Fn (ℂ ∖
{0})) |
118 | 115, 117 | mp1i 13 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0})
↦ -(𝐴 / (𝑥↑2))) Fn (ℂ ∖
{0})) |
119 | | ffun 6294 |
. . . . 5
⊢ ((ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ → Fun
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
120 | 1, 119 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ Fun (ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
121 | | funbrfv 6493 |
. . . 4
⊢ (Fun
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) → (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) → ((ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))‘𝑦) = -(𝐴 / (𝑦↑2)))) |
122 | 120, 105,
121 | sylc 65 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
123 | | oveq1 6929 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) |
124 | 123 | oveq2d 6938 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 / (𝑥↑2)) = (𝐴 / (𝑦↑2))) |
125 | 124 | negeqd 10616 |
. . . . 5
⊢ (𝑥 = 𝑦 → -(𝐴 / (𝑥↑2)) = -(𝐴 / (𝑦↑2))) |
126 | 125, 116,
107 | fvmpt 6542 |
. . . 4
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ -(𝐴 /
(𝑥↑2)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
127 | 126 | adantl 475 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ -(𝐴 /
(𝑥↑2)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
128 | 122, 127 | eqtr4d 2817 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))‘𝑦) = ((𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2)))‘𝑦)) |
129 | 113, 118,
128 | eqfnfvd 6577 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2)))) |