Step | Hyp | Ref
| Expression |
1 | | dvfcn 23478 |
. . . 4
⊢ (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ |
2 | | ssid 3587 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ℂ
⊆ ℂ) |
4 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℂ ∖ {0})
↔ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
5 | | divcl 10570 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝐴 / 𝑥) ∈ ℂ) |
6 | 5 | 3expb 1258 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (𝐴 / 𝑥) ∈ ℂ) |
7 | 4, 6 | sylan2b 491 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝐴 / 𝑥) ∈
ℂ) |
8 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)) |
9 | 7, 8 | fmptd 6292 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)):(ℂ ∖
{0})⟶ℂ) |
10 | | difssd 3700 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
∖ {0}) ⊆ ℂ) |
11 | 3, 9, 10 | dvbss 23471 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) ⊆ (ℂ ∖
{0})) |
12 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈ (ℂ
∖ {0})) |
13 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
14 | 13 | cnfldtop 22397 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈ Top |
15 | 13 | cnfldhaus 22398 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈ Haus |
16 | | 0cn 9911 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
17 | 13 | cnfldtopon 22396 |
. . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
18 | 17 | toponunii 20547 |
. . . . . . . . . . . . . . 15
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
19 | 18 | sncld 20985 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ Haus ∧ 0 ∈
ℂ) → {0} ∈
(Clsd‘(TopOpen‘ℂfld))) |
20 | 15, 16, 19 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ {0}
∈ (Clsd‘(TopOpen‘ℂfld)) |
21 | 18 | cldopn 20645 |
. . . . . . . . . . . . 13
⊢ ({0}
∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld)) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld) |
23 | | isopn3i 20696 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘(ℂ ∖ {0}))
= (ℂ ∖ {0})) |
24 | 14, 22, 23 | mp2an 704 |
. . . . . . . . . . 11
⊢
((int‘(TopOpen‘ℂfld))‘(ℂ
∖ {0})) = (ℂ ∖ {0}) |
25 | 12, 24 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈
((int‘(TopOpen‘ℂfld))‘(ℂ ∖
{0}))) |
26 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈
ℂ) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈
ℂ) |
28 | 27 | sqvald 12867 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑦↑2) = (𝑦 · 𝑦)) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / (𝑦↑2)) = (𝐴 / (𝑦 · 𝑦))) |
30 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝐴 ∈
ℂ) |
31 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ≠
0) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ≠
0) |
33 | 30, 27, 27, 32, 32 | divdiv1d 10711 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝐴 / 𝑦) / 𝑦) = (𝐴 / (𝑦 · 𝑦))) |
34 | 29, 33 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / (𝑦↑2)) = ((𝐴 / 𝑦) / 𝑦)) |
35 | 34 | negeqd 10154 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) = -((𝐴 / 𝑦) / 𝑦)) |
36 | 30, 27, 32 | divcld 10680 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / 𝑦) ∈
ℂ) |
37 | 36, 27, 32 | divnegd 10693 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -((𝐴 / 𝑦) / 𝑦) = (-(𝐴 / 𝑦) / 𝑦)) |
38 | 35, 37 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) = (-(𝐴 / 𝑦) / 𝑦)) |
39 | 36 | negcld 10258 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / 𝑦) ∈
ℂ) |
40 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) |
41 | 40 | cdivcncf 22528 |
. . . . . . . . . . . . . 14
⊢ (-(𝐴 / 𝑦) ∈ ℂ → (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ)) |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ)) |
43 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (-(𝐴 / 𝑦) / 𝑧) = (-(𝐴 / 𝑦) / 𝑦)) |
44 | 42, 12, 43 | cnmptlimc 23460 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (-(𝐴 / 𝑦) / 𝑦) ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) limℂ 𝑦)) |
45 | 38, 44 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) limℂ 𝑦)) |
46 | | cncff 22504 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ) → (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
47 | 42, 46 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
48 | 47 | limcdif 23446 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) limℂ 𝑦) = (((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) limℂ
𝑦)) |
49 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) → 𝑧 ∈ (ℂ ∖
{0})) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ∈ (ℂ
∖ {0})) |
51 | 50 | eldifad 3552 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ∈
ℂ) |
52 | 26 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑦 ∈
ℂ) |
53 | 51, 52 | subcld 10271 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 − 𝑦) ∈
ℂ) |
54 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝐴 / 𝑦) ∈
ℂ) |
55 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ≠
0) |
57 | 54, 51, 56 | divcld 10680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝐴 / 𝑦) / 𝑧) ∈ ℂ) |
58 | | mulneg12 10347 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 − 𝑦) ∈ ℂ ∧ ((𝐴 / 𝑦) / 𝑧) ∈ ℂ) → (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧))) |
59 | 53, 57, 58 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧))) |
60 | 52, 51, 57 | subdird 10366 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 − 𝑧) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑦 · ((𝐴 / 𝑦) / 𝑧)) − (𝑧 · ((𝐴 / 𝑦) / 𝑧)))) |
61 | 51, 52 | negsubdi2d 10287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -(𝑧 − 𝑦) = (𝑦 − 𝑧)) |
62 | 61 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑦 − 𝑧) · ((𝐴 / 𝑦) / 𝑧))) |
63 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (𝐴 / 𝑥) = (𝐴 / 𝑧)) |
64 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 / 𝑧) ∈ V |
65 | 63, 8, 64 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝐴 / 𝑧)) |
66 | 50, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝐴 / 𝑧)) |
67 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝐴 ∈
ℂ) |
68 | 31 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑦 ≠
0) |
69 | 67, 52, 68 | divcan2d 10682 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑦 · (𝐴 / 𝑦)) = 𝐴) |
70 | 69 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 · (𝐴 / 𝑦)) / 𝑧) = (𝐴 / 𝑧)) |
71 | 52, 54, 51, 56 | divassd 10715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 · (𝐴 / 𝑦)) / 𝑧) = (𝑦 · ((𝐴 / 𝑦) / 𝑧))) |
72 | 66, 70, 71 | 3eqtr2d 2650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝑦 · ((𝐴 / 𝑦) / 𝑧))) |
73 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝐴 / 𝑥) = (𝐴 / 𝑦)) |
74 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 / 𝑦) ∈ V |
75 | 73, 8, 74 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝐴 / 𝑦)) |
76 | 75 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝐴 / 𝑦)) |
77 | 54, 51, 56 | divcan2d 10682 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 · ((𝐴 / 𝑦) / 𝑧)) = (𝐴 / 𝑦)) |
78 | 76, 77 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝑧 · ((𝐴 / 𝑦) / 𝑧))) |
79 | 72, 78 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) = ((𝑦 · ((𝐴 / 𝑦) / 𝑧)) − (𝑧 · ((𝐴 / 𝑦) / 𝑧)))) |
80 | 60, 62, 79 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = (((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦))) |
81 | 54, 51, 56 | divnegd 10693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -((𝐴 / 𝑦) / 𝑧) = (-(𝐴 / 𝑦) / 𝑧)) |
82 | 81 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧))) |
83 | 59, 80, 82 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) = ((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧))) |
84 | 83 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦)) = (((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧)) / (𝑧 − 𝑦))) |
85 | 54 | negcld 10258 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -(𝐴 / 𝑦) ∈
ℂ) |
86 | 85, 51, 56 | divcld 10680 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝐴 / 𝑦) / 𝑧) ∈ ℂ) |
87 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) → 𝑧 ≠ 𝑦) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ≠ 𝑦) |
89 | 51, 52, 88 | subne0d 10280 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 − 𝑦) ≠ 0) |
90 | 86, 53, 89 | divcan3d 10685 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧)) / (𝑧 − 𝑦)) = (-(𝐴 / 𝑦) / 𝑧)) |
91 | 84, 90 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦)) = (-(𝐴 / 𝑦) / 𝑧)) |
92 | 91 | mpteq2dva 4672 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧))) |
93 | | difss 3699 |
. . . . . . . . . . . . . . 15
⊢ ((ℂ
∖ {0}) ∖ {𝑦})
⊆ (ℂ ∖ {0}) |
94 | | resmpt 5369 |
. . . . . . . . . . . . . . 15
⊢
(((ℂ ∖ {0}) ∖ {𝑦}) ⊆ (ℂ ∖ {0}) →
((𝑧 ∈ (ℂ ∖
{0}) ↦ (-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧))) |
95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧)) |
96 | 92, 95 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = ((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦}))) |
97 | 96 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦) = (((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) limℂ
𝑦)) |
98 | 48, 97 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) limℂ 𝑦) = ((𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ ((((𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)) |
99 | 45, 98 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)) |
100 | 18 | restid 15917 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
101 | 14, 100 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
102 | 101 | eqcomi 2619 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
103 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ ((((𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) |
104 | 2 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ℂ ⊆ ℂ) |
105 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥)):(ℂ ∖
{0})⟶ℂ) |
106 | | difssd 3700 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (ℂ ∖ {0}) ⊆ ℂ) |
107 | 102, 13, 103, 104, 105, 106 | eldv 23468 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) ↔ (𝑦 ∈
((int‘(TopOpen‘ℂfld))‘(ℂ ∖ {0}))
∧ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)))) |
108 | 25, 99, 107 | mpbir2and 959 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2))) |
109 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
110 | | negex 10158 |
. . . . . . . . . 10
⊢ -(𝐴 / (𝑦↑2)) ∈ V |
111 | 109, 110 | breldm 5251 |
. . . . . . . . 9
⊢ (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) → 𝑦 ∈ dom (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
112 | 108, 111 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈ dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
113 | 112 | ex 449 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈ dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))))) |
114 | 113 | ssrdv 3574 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
∖ {0}) ⊆ dom (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
115 | 11, 114 | eqssd 3585 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) = (ℂ ∖ {0})) |
116 | 115 | feq2d 5944 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ ↔
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))):(ℂ ∖
{0})⟶ℂ)) |
117 | 1, 116 | mpbii 222 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):(ℂ ∖
{0})⟶ℂ) |
118 | | ffn 5958 |
. . 3
⊢ ((ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):(ℂ ∖
{0})⟶ℂ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) Fn (ℂ ∖
{0})) |
119 | 117, 118 | syl 17 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))) Fn (ℂ ∖
{0})) |
120 | | negex 10158 |
. . . 4
⊢ -(𝐴 / (𝑥↑2)) ∈ V |
121 | 120 | rgenw 2908 |
. . 3
⊢
∀𝑥 ∈
(ℂ ∖ {0})-(𝐴 /
(𝑥↑2)) ∈
V |
122 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ (ℂ ∖ {0})
↦ -(𝐴 / (𝑥↑2))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2))) |
123 | 122 | fnmpt 5933 |
. . 3
⊢
(∀𝑥 ∈
(ℂ ∖ {0})-(𝐴 /
(𝑥↑2)) ∈ V →
(𝑥 ∈ (ℂ ∖
{0}) ↦ -(𝐴 / (𝑥↑2))) Fn (ℂ ∖
{0})) |
124 | 121, 123 | mp1i 13 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0})
↦ -(𝐴 / (𝑥↑2))) Fn (ℂ ∖
{0})) |
125 | | ffun 5961 |
. . . . 5
⊢ ((ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ → Fun
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
126 | 1, 125 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ Fun (ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
127 | | funbrfv 6144 |
. . . 4
⊢ (Fun
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) → (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) → ((ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))‘𝑦) = -(𝐴 / (𝑦↑2)))) |
128 | 126, 108,
127 | sylc 63 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
129 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) |
130 | 129 | oveq2d 6565 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 / (𝑥↑2)) = (𝐴 / (𝑦↑2))) |
131 | 130 | negeqd 10154 |
. . . . 5
⊢ (𝑥 = 𝑦 → -(𝐴 / (𝑥↑2)) = -(𝐴 / (𝑦↑2))) |
132 | 131, 122,
110 | fvmpt 6191 |
. . . 4
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ -(𝐴 /
(𝑥↑2)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
133 | 132 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ -(𝐴 /
(𝑥↑2)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
134 | 128, 133 | eqtr4d 2647 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))‘𝑦) = ((𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2)))‘𝑦)) |
135 | 119, 124,
134 | eqfnfvd 6222 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2)))) |