| Step | Hyp | Ref
| Expression |
| 1 | | dvfcn 25943 |
. . . 4
⊢ (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ |
| 2 | | ssidd 4007 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ℂ
⊆ ℂ) |
| 3 | | eldifsn 4786 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℂ ∖ {0})
↔ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
| 4 | | divcl 11928 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝐴 / 𝑥) ∈ ℂ) |
| 5 | 4 | 3expb 1121 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (𝐴 / 𝑥) ∈ ℂ) |
| 6 | 3, 5 | sylan2b 594 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝐴 / 𝑥) ∈
ℂ) |
| 7 | 6 | fmpttd 7135 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)):(ℂ ∖
{0})⟶ℂ) |
| 8 | | difssd 4137 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
∖ {0}) ⊆ ℂ) |
| 9 | 2, 7, 8 | dvbss 25936 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) ⊆ (ℂ ∖
{0})) |
| 10 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈ (ℂ
∖ {0})) |
| 11 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 12 | 11 | cnfldtop 24804 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Top |
| 13 | | cnn0opn 24808 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld) |
| 14 | | isopn3i 23090 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘(ℂ ∖ {0}))
= (ℂ ∖ {0})) |
| 15 | 12, 13, 14 | mp2an 692 |
. . . . . . . . 9
⊢
((int‘(TopOpen‘ℂfld))‘(ℂ
∖ {0})) = (ℂ ∖ {0}) |
| 16 | 10, 15 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈
((int‘(TopOpen‘ℂfld))‘(ℂ ∖
{0}))) |
| 17 | | eldifi 4131 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ∈
ℂ) |
| 18 | 17 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈
ℂ) |
| 19 | 18 | sqvald 14183 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑦↑2) = (𝑦 · 𝑦)) |
| 20 | 19 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / (𝑦↑2)) = (𝐴 / (𝑦 · 𝑦))) |
| 21 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝐴 ∈
ℂ) |
| 22 | | eldifsni 4790 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ 𝑦 ≠
0) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ≠
0) |
| 24 | 21, 18, 18, 23, 23 | divdiv1d 12074 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝐴 / 𝑦) / 𝑦) = (𝐴 / (𝑦 · 𝑦))) |
| 25 | 20, 24 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / (𝑦↑2)) = ((𝐴 / 𝑦) / 𝑦)) |
| 26 | 25 | negeqd 11502 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) = -((𝐴 / 𝑦) / 𝑦)) |
| 27 | 21, 18, 23 | divcld 12043 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝐴 / 𝑦) ∈
ℂ) |
| 28 | 27, 18, 23 | divnegd 12056 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -((𝐴 / 𝑦) / 𝑦) = (-(𝐴 / 𝑦) / 𝑦)) |
| 29 | 26, 28 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) = (-(𝐴 / 𝑦) / 𝑦)) |
| 30 | 27 | negcld 11607 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / 𝑦) ∈
ℂ) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) |
| 32 | 31 | cdivcncf 24947 |
. . . . . . . . . . . 12
⊢ (-(𝐴 / 𝑦) ∈ ℂ → (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ)) |
| 33 | 30, 32 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ)) |
| 34 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (-(𝐴 / 𝑦) / 𝑧) = (-(𝐴 / 𝑦) / 𝑦)) |
| 35 | 33, 10, 34 | cnmptlimc 25925 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (-(𝐴 / 𝑦) / 𝑦) ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) limℂ 𝑦)) |
| 36 | 29, 35 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) limℂ 𝑦)) |
| 37 | | cncff 24919 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) ∈ ((ℂ ∖ {0})–cn→ℂ) → (𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
| 38 | 33, 37 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
| 39 | 38 | limcdif 25911 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) limℂ 𝑦) = (((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) limℂ
𝑦)) |
| 40 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) → 𝑧 ∈ (ℂ ∖
{0})) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ∈ (ℂ
∖ {0})) |
| 42 | 41 | eldifad 3963 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ∈
ℂ) |
| 43 | 17 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑦 ∈
ℂ) |
| 44 | 42, 43 | subcld 11620 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 − 𝑦) ∈
ℂ) |
| 45 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝐴 / 𝑦) ∈
ℂ) |
| 46 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
| 47 | 41, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ≠
0) |
| 48 | 45, 42, 47 | divcld 12043 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝐴 / 𝑦) / 𝑧) ∈ ℂ) |
| 49 | | mulneg12 11701 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 − 𝑦) ∈ ℂ ∧ ((𝐴 / 𝑦) / 𝑧) ∈ ℂ) → (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧))) |
| 50 | 44, 48, 49 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧))) |
| 51 | 43, 42, 48 | subdird 11720 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 − 𝑧) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑦 · ((𝐴 / 𝑦) / 𝑧)) − (𝑧 · ((𝐴 / 𝑦) / 𝑧)))) |
| 52 | 42, 43 | negsubdi2d 11636 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -(𝑧 − 𝑦) = (𝑦 − 𝑧)) |
| 53 | 52 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = ((𝑦 − 𝑧) · ((𝐴 / 𝑦) / 𝑧))) |
| 54 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (𝐴 / 𝑥) = (𝐴 / 𝑧)) |
| 55 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)) |
| 56 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 / 𝑧) ∈ V |
| 57 | 54, 55, 56 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝐴 / 𝑧)) |
| 58 | 41, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝐴 / 𝑧)) |
| 59 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝐴 ∈
ℂ) |
| 60 | 22 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑦 ≠
0) |
| 61 | 59, 43, 60 | divcan2d 12045 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑦 · (𝐴 / 𝑦)) = 𝐴) |
| 62 | 61 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 · (𝐴 / 𝑦)) / 𝑧) = (𝐴 / 𝑧)) |
| 63 | 43, 45, 42, 47 | divassd 12078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑦 · (𝐴 / 𝑦)) / 𝑧) = (𝑦 · ((𝐴 / 𝑦) / 𝑧))) |
| 64 | 58, 62, 63 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) = (𝑦 · ((𝐴 / 𝑦) / 𝑧))) |
| 65 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (𝐴 / 𝑥) = (𝐴 / 𝑦)) |
| 66 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 / 𝑦) ∈ V |
| 67 | 65, 55, 66 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝐴 / 𝑦)) |
| 68 | 67 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝐴 / 𝑦)) |
| 69 | 45, 42, 47 | divcan2d 12045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 · ((𝐴 / 𝑦) / 𝑧)) = (𝐴 / 𝑦)) |
| 70 | 68, 69 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑦) = (𝑧 · ((𝐴 / 𝑦) / 𝑧))) |
| 71 | 64, 70 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) = ((𝑦 · ((𝐴 / 𝑦) / 𝑧)) − (𝑧 · ((𝐴 / 𝑦) / 𝑧)))) |
| 72 | 51, 53, 71 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝑧 − 𝑦) · ((𝐴 / 𝑦) / 𝑧)) = (((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦))) |
| 73 | 45, 42, 47 | divnegd 12056 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -((𝐴 / 𝑦) / 𝑧) = (-(𝐴 / 𝑦) / 𝑧)) |
| 74 | 73 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((𝑧 − 𝑦) · -((𝐴 / 𝑦) / 𝑧)) = ((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧))) |
| 75 | 50, 72, 74 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) = ((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧))) |
| 76 | 75 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦)) = (((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧)) / (𝑧 − 𝑦))) |
| 77 | 45 | negcld 11607 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ -(𝐴 / 𝑦) ∈
ℂ) |
| 78 | 77, 42, 47 | divcld 12043 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (-(𝐴 / 𝑦) / 𝑧) ∈ ℂ) |
| 79 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) → 𝑧 ≠ 𝑦) |
| 80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ 𝑧 ≠ 𝑦) |
| 81 | 42, 43, 80 | subne0d 11629 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (𝑧 − 𝑦) ≠ 0) |
| 82 | 78, 44, 81 | divcan3d 12048 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ (((𝑧 − 𝑦) · (-(𝐴 / 𝑦) / 𝑧)) / (𝑧 − 𝑦)) = (-(𝐴 / 𝑦) / 𝑧)) |
| 83 | 76, 82 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
∧ 𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦}))
→ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦)) = (-(𝐴 / 𝑦) / 𝑧)) |
| 84 | 83 | mpteq2dva 5242 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧))) |
| 85 | | difss 4136 |
. . . . . . . . . . . . 13
⊢ ((ℂ
∖ {0}) ∖ {𝑦})
⊆ (ℂ ∖ {0}) |
| 86 | | resmpt 6055 |
. . . . . . . . . . . . 13
⊢
(((ℂ ∖ {0}) ∖ {𝑦}) ⊆ (ℂ ∖ {0}) →
((𝑧 ∈ (ℂ ∖
{0}) ↦ (-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧))) |
| 87 | 85, 86 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ (-(𝐴 / 𝑦) / 𝑧)) |
| 88 | 84, 87 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = ((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦}))) |
| 89 | 88 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ ((ℂ
∖ {0}) ∖ {𝑦})
↦ ((((𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦) = (((𝑧 ∈ (ℂ ∖ {0}) ↦
(-(𝐴 / 𝑦) / 𝑧)) ↾ ((ℂ ∖ {0}) ∖
{𝑦})) limℂ
𝑦)) |
| 90 | 39, 89 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (-(𝐴 /
𝑦) / 𝑧)) limℂ 𝑦) = ((𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ ((((𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)) |
| 91 | 36, 90 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)) |
| 92 | 11 | cnfldtopon 24803 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 93 | 92 | toponrestid 22927 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 94 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) = (𝑧 ∈ ((ℂ ∖ {0}) ∖ {𝑦}) ↦ ((((𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) |
| 95 | | ssidd 4007 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ℂ ⊆ ℂ) |
| 96 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥)):(ℂ ∖
{0})⟶ℂ) |
| 97 | | difssd 4137 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (ℂ ∖ {0}) ⊆ ℂ) |
| 98 | 93, 11, 94, 95, 96, 97 | eldv 25933 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) ↔ (𝑦 ∈
((int‘(TopOpen‘ℂfld))‘(ℂ ∖ {0}))
∧ -(𝐴 / (𝑦↑2)) ∈ ((𝑧 ∈ ((ℂ ∖ {0})
∖ {𝑦}) ↦
((((𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))‘𝑧) − ((𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))‘𝑦)) / (𝑧 − 𝑦))) limℂ 𝑦)))) |
| 99 | 16, 91, 98 | mpbir2and 713 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2))) |
| 100 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 101 | | negex 11506 |
. . . . . . . 8
⊢ -(𝐴 / (𝑦↑2)) ∈ V |
| 102 | 100, 101 | breldm 5919 |
. . . . . . 7
⊢ (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) → 𝑦 ∈ dom (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
| 103 | 99, 102 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈ dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
| 104 | 9, 103 | eqelssd 4005 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) = (ℂ ∖ {0})) |
| 105 | 104 | feq2d 6722 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ ↔
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))):(ℂ ∖
{0})⟶ℂ)) |
| 106 | 1, 105 | mpbii 233 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):(ℂ ∖
{0})⟶ℂ) |
| 107 | 106 | ffnd 6737 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))) Fn (ℂ ∖
{0})) |
| 108 | | negex 11506 |
. . . 4
⊢ -(𝐴 / (𝑥↑2)) ∈ V |
| 109 | 108 | rgenw 3065 |
. . 3
⊢
∀𝑥 ∈
(ℂ ∖ {0})-(𝐴 /
(𝑥↑2)) ∈
V |
| 110 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ (ℂ ∖ {0})
↦ -(𝐴 / (𝑥↑2))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2))) |
| 111 | 110 | fnmpt 6708 |
. . 3
⊢
(∀𝑥 ∈
(ℂ ∖ {0})-(𝐴 /
(𝑥↑2)) ∈ V →
(𝑥 ∈ (ℂ ∖
{0}) ↦ -(𝐴 / (𝑥↑2))) Fn (ℂ ∖
{0})) |
| 112 | 109, 111 | mp1i 13 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0})
↦ -(𝐴 / (𝑥↑2))) Fn (ℂ ∖
{0})) |
| 113 | | ffun 6739 |
. . . . 5
⊢ ((ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))):dom (ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))⟶ℂ → Fun
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
| 114 | 1, 113 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ Fun (ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))) |
| 115 | | funbrfv 6957 |
. . . 4
⊢ (Fun
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝐴 / 𝑥))) → (𝑦(ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))-(𝐴 / (𝑦↑2)) → ((ℂ D (𝑥 ∈ (ℂ ∖ {0})
↦ (𝐴 / 𝑥)))‘𝑦) = -(𝐴 / (𝑦↑2)))) |
| 116 | 114, 99, 115 | sylc 65 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
| 117 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) |
| 118 | 117 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 / (𝑥↑2)) = (𝐴 / (𝑦↑2))) |
| 119 | 118 | negeqd 11502 |
. . . . 5
⊢ (𝑥 = 𝑦 → -(𝐴 / (𝑥↑2)) = -(𝐴 / (𝑦↑2))) |
| 120 | 119, 110,
101 | fvmpt 7016 |
. . . 4
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ -(𝐴 /
(𝑥↑2)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
| 121 | 120 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((𝑥 ∈ (ℂ
∖ {0}) ↦ -(𝐴 /
(𝑥↑2)))‘𝑦) = -(𝐴 / (𝑦↑2))) |
| 122 | 116, 121 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ ((ℂ D (𝑥
∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)))‘𝑦) = ((𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2)))‘𝑦)) |
| 123 | 107, 112,
122 | eqfnfvd 7054 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝐴 /
𝑥))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ -(𝐴 / (𝑥↑2)))) |