Step | Hyp | Ref
| Expression |
1 | | dvadd.bf |
. . . . . 6
⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾) |
2 | | eqid 2610 |
. . . . . . 7
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
3 | | dvadd.j |
. . . . . . 7
⊢ 𝐽 =
(TopOpen‘ℂfld) |
4 | | eqid 2610 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) |
5 | | dvaddbr.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
6 | | dvadd.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
7 | | dvadd.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
8 | 2, 3, 4, 5, 6, 7 | eldv 23468 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
9 | 1, 8 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
10 | 9 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋)) |
11 | | dvadd.bg |
. . . . . 6
⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿) |
12 | | eqid 2610 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
13 | | dvadd.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑌⟶ℂ) |
14 | | dvadd.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ 𝑆) |
15 | 2, 3, 12, 5, 13, 14 | eldv 23468 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
16 | 11, 15 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
17 | 16 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌)) |
18 | 10, 17 | elind 3760 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
19 | 3 | cnfldtopon 22396 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘ℂ) |
20 | | resttopon 20775 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐽
↾t 𝑆)
∈ (TopOn‘𝑆)) |
21 | 19, 5, 20 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
22 | | topontop 20541 |
. . . . 5
⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾t 𝑆) ∈ Top) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Top) |
24 | | toponuni 20542 |
. . . . . 6
⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
25 | 21, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
26 | 7, 25 | sseqtrd 3604 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆)) |
27 | 14, 25 | sseqtrd 3604 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾t 𝑆)) |
28 | | eqid 2610 |
. . . . 5
⊢ ∪ (𝐽
↾t 𝑆) =
∪ (𝐽 ↾t 𝑆) |
29 | 28 | ntrin 20675 |
. . . 4
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽
↾t 𝑆)
∧ 𝑌 ⊆ ∪ (𝐽
↾t 𝑆))
→ ((int‘(𝐽
↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
30 | 23, 26, 27, 29 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
31 | 18, 30 | eleqtrrd 2691 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌))) |
32 | | inss1 3795 |
. . . . . . 7
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
33 | | ssdif 3707 |
. . . . . . 7
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶})) |
34 | 32, 33 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶})) |
35 | 34 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∖ {𝐶})) |
36 | 7, 5 | sstrd 3578 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
37 | 28 | ntrss2 20671 |
. . . . . . . 8
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽
↾t 𝑆))
→ ((int‘(𝐽
↾t 𝑆))‘𝑋) ⊆ 𝑋) |
38 | 23, 26, 37 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘𝑋) ⊆ 𝑋) |
39 | 38, 10 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
40 | 6, 36, 39 | dvlem 23466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
41 | 35, 40 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
42 | | inss2 3796 |
. . . . . . 7
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
43 | | ssdif 3707 |
. . . . . . 7
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶})) |
44 | 42, 43 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶})) |
45 | 44 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶})) |
46 | 14, 5 | sstrd 3578 |
. . . . . 6
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
47 | 28 | ntrss2 20671 |
. . . . . . . 8
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽
↾t 𝑆))
→ ((int‘(𝐽
↾t 𝑆))‘𝑌) ⊆ 𝑌) |
48 | 23, 27, 47 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘𝑌) ⊆ 𝑌) |
49 | 48, 17 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
50 | 13, 46, 49 | dvlem 23466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
51 | 45, 50 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
52 | | ssid 3587 |
. . . . 5
⊢ ℂ
⊆ ℂ |
53 | 52 | a1i 11 |
. . . 4
⊢ (𝜑 → ℂ ⊆
ℂ) |
54 | | txtopon 21204 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐽 ∈
(TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ ×
ℂ))) |
55 | 19, 19, 54 | mp2an 704 |
. . . . . 6
⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ
× ℂ)) |
56 | 55 | toponunii 20547 |
. . . . . . 7
⊢ (ℂ
× ℂ) = ∪ (𝐽 ×t 𝐽) |
57 | 56 | restid 15917 |
. . . . . 6
⊢ ((𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ
× ℂ)) → ((𝐽 ×t 𝐽) ↾t (ℂ ×
ℂ)) = (𝐽
×t 𝐽)) |
58 | 55, 57 | ax-mp 5 |
. . . . 5
⊢ ((𝐽 ×t 𝐽) ↾t (ℂ
× ℂ)) = (𝐽
×t 𝐽) |
59 | 58 | eqcomi 2619 |
. . . 4
⊢ (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ ×
ℂ)) |
60 | 9 | simprd 478 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
61 | 40, 4 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ) |
62 | 36 | ssdifssd 3710 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ) |
63 | | eqid 2610 |
. . . . . . 7
⊢ (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) |
64 | 32, 7 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆) |
65 | 64, 25 | sseqtrd 3604 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪
(𝐽 ↾t
𝑆)) |
66 | | difssd 3700 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∪ (𝐽
↾t 𝑆)
∖ 𝑋) ⊆ ∪ (𝐽
↾t 𝑆)) |
67 | 65, 66 | unssd 3751 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪
(𝐽 ↾t
𝑆)) |
68 | | ssun1 3738 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) |
70 | 28 | ntrss 20669 |
. . . . . . . . . . . 12
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪
(𝐽 ↾t
𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
71 | 23, 67, 69, 70 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
72 | 71, 31 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
73 | 72, 39 | elind 3760 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
74 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋) |
75 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ((𝐽 ↾t 𝑆) ↾t 𝑋) = ((𝐽 ↾t 𝑆) ↾t 𝑋) |
76 | 28, 75 | restntr 20796 |
. . . . . . . . . . 11
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽
↾t 𝑆)
∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
77 | 23, 26, 74, 76 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
78 | 3 | cnfldtop 22397 |
. . . . . . . . . . . . . 14
⊢ 𝐽 ∈ Top |
79 | 78 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Top) |
80 | | cnex 9896 |
. . . . . . . . . . . . . 14
⊢ ℂ
∈ V |
81 | | ssexg 4732 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
82 | 5, 80, 81 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ V) |
83 | | restabs 20779 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
84 | 79, 7, 82, 83 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
85 | 84 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑋)) = (int‘(𝐽 ↾t 𝑋))) |
86 | 85 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
87 | 77, 86 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
88 | 73, 87 | eleqtrd 2690 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
89 | | undif1 3995 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶}) |
90 | 39 | snssd 4281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐶} ⊆ 𝑋) |
91 | | ssequn2 3748 |
. . . . . . . . . . . . 13
⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋) |
92 | 90, 91 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋) |
93 | 89, 92 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋) |
94 | 93 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑋)) |
95 | 94 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑋))) |
96 | | undif1 3995 |
. . . . . . . . . 10
⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶}) |
97 | 39, 49 | elind 3760 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌)) |
98 | 97 | snssd 4281 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌)) |
99 | | ssequn2 3748 |
. . . . . . . . . . 11
⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
100 | 98, 99 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
101 | 96, 100 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
102 | 95, 101 | fveq12d 6109 |
. . . . . . . 8
⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
103 | 88, 102 | eleqtrrd 2691 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
104 | 61, 34, 62, 3, 63, 103 | limcres 23456 |
. . . . . 6
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
105 | 34 | resmptd 5371 |
. . . . . . 7
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))) |
106 | 105 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
107 | 104, 106 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
108 | 60, 107 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
109 | 16 | simprd 478 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
110 | 50, 12 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ) |
111 | 46 | ssdifssd 3710 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ) |
112 | | eqid 2610 |
. . . . . . 7
⊢ (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) |
113 | | difssd 3700 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∪ (𝐽
↾t 𝑆)
∖ 𝑌) ⊆ ∪ (𝐽
↾t 𝑆)) |
114 | 65, 113 | unssd 3751 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪
(𝐽 ↾t
𝑆)) |
115 | | ssun1 3738 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) |
116 | 115 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) |
117 | 28 | ntrss 20669 |
. . . . . . . . . . . 12
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪
(𝐽 ↾t
𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
118 | 23, 114, 116, 117 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
119 | 118, 31 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
120 | 119, 49 | elind 3760 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
121 | 42 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌) |
122 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ((𝐽 ↾t 𝑆) ↾t 𝑌) = ((𝐽 ↾t 𝑆) ↾t 𝑌) |
123 | 28, 122 | restntr 20796 |
. . . . . . . . . . 11
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽
↾t 𝑆)
∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
124 | 23, 27, 121, 123 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
125 | | restabs 20779 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
126 | 79, 14, 82, 125 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
127 | 126 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑌)) = (int‘(𝐽 ↾t 𝑌))) |
128 | 127 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
129 | 124, 128 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
130 | 120, 129 | eleqtrd 2690 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
131 | | undif1 3995 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶}) |
132 | 49 | snssd 4281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐶} ⊆ 𝑌) |
133 | | ssequn2 3748 |
. . . . . . . . . . . . 13
⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌) |
134 | 132, 133 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌) |
135 | 131, 134 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌) |
136 | 135 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑌)) |
137 | 136 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑌))) |
138 | 137, 101 | fveq12d 6109 |
. . . . . . . 8
⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
139 | 130, 138 | eleqtrrd 2691 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
140 | 110, 44, 111, 3, 112, 139 | limcres 23456 |
. . . . . 6
⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
141 | 44 | resmptd 5371 |
. . . . . . 7
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
142 | 141 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
143 | 140, 142 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
144 | 109, 143 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
145 | 3 | addcn 22476 |
. . . . 5
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
146 | 5, 6, 7 | dvcl 23469 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ) |
147 | 1, 146 | mpdan 699 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℂ) |
148 | 5, 13, 14 | dvcl 23469 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ) |
149 | 11, 148 | mpdan 699 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ℂ) |
150 | | opelxpi 5072 |
. . . . . 6
⊢ ((𝐾 ∈ ℂ ∧ 𝐿 ∈ ℂ) →
〈𝐾, 𝐿〉 ∈ (ℂ ×
ℂ)) |
151 | 147, 149,
150 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ (ℂ ×
ℂ)) |
152 | 56 | cncnpi 20892 |
. . . . 5
⊢ (( +
∈ ((𝐽
×t 𝐽) Cn
𝐽) ∧ 〈𝐾, 𝐿〉 ∈ (ℂ × ℂ))
→ + ∈ (((𝐽
×t 𝐽) CnP
𝐽)‘〈𝐾, 𝐿〉)) |
153 | 145, 151,
152 | sylancr 694 |
. . . 4
⊢ (𝜑 → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, 𝐿〉)) |
154 | 41, 51, 53, 53, 3, 59, 108, 144, 153 | limccnp2 23462 |
. . 3
⊢ (𝜑 → (𝐾 + 𝐿) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
155 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌)) |
156 | 155 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌)) |
157 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑋⟶ℂ → 𝐹 Fn 𝑋) |
158 | 6, 157 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn 𝑋) |
159 | 158 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋) |
160 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝑌⟶ℂ → 𝐺 Fn 𝑌) |
161 | 13, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 Fn 𝑌) |
162 | 161 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌) |
163 | | ssexg 4732 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ⊆ ℂ ∧ ℂ
∈ V) → 𝑋 ∈
V) |
164 | 36, 80, 163 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ V) |
165 | 164 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V) |
166 | | ssexg 4732 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ⊆ ℂ ∧ ℂ
∈ V) → 𝑌 ∈
V) |
167 | 46, 80, 166 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ V) |
168 | 167 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V) |
169 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌) |
170 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
171 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
172 | 159, 162,
165, 168, 169, 170, 171 | ofval 6804 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘𝑓 + 𝐺)‘𝑧) = ((𝐹‘𝑧) + (𝐺‘𝑧))) |
173 | 156, 172 | mpdan 699 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘𝑓 + 𝐺)‘𝑧) = ((𝐹‘𝑧) + (𝐺‘𝑧))) |
174 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶)) |
175 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶)) |
176 | 159, 162,
165, 168, 169, 174, 175 | ofval 6804 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘𝑓 + 𝐺)‘𝐶) = ((𝐹‘𝐶) + (𝐺‘𝐶))) |
177 | 97, 176 | mpidan 701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘𝑓 + 𝐺)‘𝐶) = ((𝐹‘𝐶) + (𝐺‘𝐶))) |
178 | 173, 177 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) = (((𝐹‘𝑧) + (𝐺‘𝑧)) − ((𝐹‘𝐶) + (𝐺‘𝐶)))) |
179 | | difss 3699 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) |
180 | 179, 32 | sstri 3577 |
. . . . . . . . . . 11
⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑋 |
181 | 180 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ 𝑋) |
182 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ) |
183 | 6, 181, 182 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ) |
184 | 179, 42 | sstri 3577 |
. . . . . . . . . . 11
⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌 |
185 | 184 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ 𝑌) |
186 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝐺:𝑌⟶ℂ ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) ∈ ℂ) |
187 | 13, 185, 186 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ) |
188 | 6, 39 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
189 | 188 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
190 | 13, 49 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ) |
191 | 190 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ) |
192 | 183, 187,
189, 191 | addsub4d 10318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) + (𝐺‘𝑧)) − ((𝐹‘𝐶) + (𝐺‘𝐶))) = (((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶)))) |
193 | 178, 192 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) = (((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶)))) |
194 | 193 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶))) / (𝑧 − 𝐶))) |
195 | 183, 189 | subcld 10271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ) |
196 | 187, 191 | subcld 10271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ) |
197 | 180, 36 | syl5ss 3579 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ ℂ) |
198 | 197 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ) |
199 | 36, 39 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
200 | 199 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ) |
201 | 198, 200 | subcld 10271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ) |
202 | | eldifsni 4261 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶) |
203 | 202 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶) |
204 | 198, 200,
203 | subne0d 10280 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0) |
205 | 195, 196,
201, 204 | divdird 10718 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) + ((𝐺‘𝑧) − (𝐺‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
206 | 194, 205 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
207 | 206 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))))) |
208 | 207 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) limℂ 𝐶)) |
209 | 154, 208 | eleqtrrd 2691 |
. 2
⊢ (𝜑 → (𝐾 + 𝐿) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
210 | | eqid 2610 |
. . 3
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
211 | | addcl 9897 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
212 | 211 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) |
213 | 212, 6, 13, 164, 167, 169 | off 6810 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):(𝑋 ∩ 𝑌)⟶ℂ) |
214 | 2, 3, 210, 5, 213, 64 | eldv 23468 |
. 2
⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿) ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ (𝐾 + 𝐿) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 + 𝐺)‘𝑧) − ((𝐹 ∘𝑓 + 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
215 | 31, 209, 214 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 + 𝐺))(𝐾 + 𝐿)) |