Step | Hyp | Ref
| Expression |
1 | | dvadd.bf |
. . . . . 6
⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾) |
2 | | eqid 2622 |
. . . . . . 7
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
3 | | dvadd.j |
. . . . . . 7
⊢ 𝐽 =
(TopOpen‘ℂfld) |
4 | | eqid 2622 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) |
5 | | dvaddbr.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
6 | | dvadd.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
7 | | dvadd.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
8 | 2, 3, 4, 5, 6, 7 | eldv 23662 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
9 | 1, 8 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
10 | 9 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋)) |
11 | | dvadd.bg |
. . . . . 6
⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿) |
12 | | eqid 2622 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
13 | | dvadd.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑌⟶ℂ) |
14 | | dvadd.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ 𝑆) |
15 | 2, 3, 12, 5, 13, 14 | eldv 23662 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
16 | 11, 15 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
17 | 16 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌)) |
18 | 10, 17 | elind 3798 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
19 | 3 | cnfldtopon 22586 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘ℂ) |
20 | | resttopon 20965 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐽
↾t 𝑆)
∈ (TopOn‘𝑆)) |
21 | 19, 5, 20 | sylancr 695 |
. . . . 5
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
22 | | topontop 20718 |
. . . . 5
⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾t 𝑆) ∈ Top) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Top) |
24 | | toponuni 20719 |
. . . . . 6
⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
25 | 21, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
26 | 7, 25 | sseqtrd 3641 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆)) |
27 | 14, 25 | sseqtrd 3641 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾t 𝑆)) |
28 | | eqid 2622 |
. . . . 5
⊢ ∪ (𝐽
↾t 𝑆) =
∪ (𝐽 ↾t 𝑆) |
29 | 28 | ntrin 20865 |
. . . 4
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽
↾t 𝑆)
∧ 𝑌 ⊆ ∪ (𝐽
↾t 𝑆))
→ ((int‘(𝐽
↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
30 | 23, 26, 27, 29 | syl3anc 1326 |
. . 3
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
31 | 18, 30 | eleqtrrd 2704 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌))) |
32 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ) |
33 | | inss1 3833 |
. . . . . . . . 9
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
34 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌)) |
35 | 34 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌)) |
36 | 33, 35 | sseldi 3601 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋) |
37 | 32, 36 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ) |
38 | 5, 6, 7 | dvbss 23665 |
. . . . . . . . . 10
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋) |
39 | | reldv 23634 |
. . . . . . . . . . 11
⊢ Rel
(𝑆 D 𝐹) |
40 | | releldm 5358 |
. . . . . . . . . . 11
⊢ ((Rel
(𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹)) |
41 | 39, 1, 40 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹)) |
42 | 38, 41 | sseldd 3604 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
43 | 6, 42 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
44 | 43 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
45 | 37, 44 | subcld 10392 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ) |
46 | 7, 5 | sstrd 3613 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
47 | 46 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ) |
48 | 47, 36 | sseldd 3604 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ) |
49 | 46, 42 | sseldd 3604 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
50 | 49 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ) |
51 | 48, 50 | subcld 10392 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ) |
52 | | eldifsni 4320 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶) |
53 | 52 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶) |
54 | 48, 50, 53 | subne0d 10401 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0) |
55 | 45, 51, 54 | divcld 10801 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
56 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ) |
57 | | inss2 3834 |
. . . . . . 7
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
58 | 57, 35 | sseldi 3601 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌) |
59 | 56, 58 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ) |
60 | 55, 59 | mulcld 10060 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ) |
61 | | ssdif 3745 |
. . . . . . . 8
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶})) |
62 | 57, 61 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶})) |
63 | 62 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶})) |
64 | 14, 5 | sstrd 3613 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
65 | 5, 13, 14 | dvbss 23665 |
. . . . . . . 8
⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌) |
66 | | reldv 23634 |
. . . . . . . . 9
⊢ Rel
(𝑆 D 𝐺) |
67 | | releldm 5358 |
. . . . . . . . 9
⊢ ((Rel
(𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺)) |
68 | 66, 11, 67 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺)) |
69 | 65, 68 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
70 | 13, 64, 69 | dvlem 23660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
71 | 63, 70 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
72 | 71, 44 | mulcld 10060 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ) |
73 | | ssid 3624 |
. . . . 5
⊢ ℂ
⊆ ℂ |
74 | 73 | a1i 11 |
. . . 4
⊢ (𝜑 → ℂ ⊆
ℂ) |
75 | | txtopon 21394 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐽 ∈
(TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ ×
ℂ))) |
76 | 19, 19, 75 | mp2an 708 |
. . . . . 6
⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ
× ℂ)) |
77 | 76 | toponunii 20721 |
. . . . . . 7
⊢ (ℂ
× ℂ) = ∪ (𝐽 ×t 𝐽) |
78 | 77 | restid 16094 |
. . . . . 6
⊢ ((𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ
× ℂ)) → ((𝐽 ×t 𝐽) ↾t (ℂ ×
ℂ)) = (𝐽
×t 𝐽)) |
79 | 76, 78 | ax-mp 5 |
. . . . 5
⊢ ((𝐽 ×t 𝐽) ↾t (ℂ
× ℂ)) = (𝐽
×t 𝐽) |
80 | 79 | eqcomi 2631 |
. . . 4
⊢ (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ ×
ℂ)) |
81 | 9 | simprd 479 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
82 | 6, 46, 42 | dvlem 23660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
83 | 82, 4 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ) |
84 | | ssdif 3745 |
. . . . . . . . 9
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶})) |
85 | 33, 84 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶})) |
86 | 46 | ssdifssd 3748 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ) |
87 | | eqid 2622 |
. . . . . . . 8
⊢ (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) |
88 | 33, 7 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆) |
89 | 88, 25 | sseqtrd 3641 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪
(𝐽 ↾t
𝑆)) |
90 | | difssd 3738 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∪ (𝐽
↾t 𝑆)
∖ 𝑋) ⊆ ∪ (𝐽
↾t 𝑆)) |
91 | 89, 90 | unssd 3789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪
(𝐽 ↾t
𝑆)) |
92 | | ssun1 3776 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) |
93 | 92 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) |
94 | 28 | ntrss 20859 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪
(𝐽 ↾t
𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
95 | 23, 91, 93, 94 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
96 | 95, 31 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
97 | 96, 42 | elind 3798 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
98 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋) |
99 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ↾t 𝑆) ↾t 𝑋) = ((𝐽 ↾t 𝑆) ↾t 𝑋) |
100 | 28, 99 | restntr 20986 |
. . . . . . . . . . . 12
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽
↾t 𝑆)
∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
101 | 23, 26, 98, 100 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
102 | 3 | cnfldtop 22587 |
. . . . . . . . . . . . . . 15
⊢ 𝐽 ∈ Top |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐽 ∈ Top) |
104 | | cnex 10017 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ V |
105 | | ssexg 4804 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
106 | 5, 104, 105 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ V) |
107 | | restabs 20969 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
108 | 103, 7, 106, 107 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
109 | 108 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑋)) = (int‘(𝐽 ↾t 𝑋))) |
110 | 109 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
111 | 101, 110 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
112 | 97, 111 | eleqtrd 2703 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
113 | | undif1 4043 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶}) |
114 | 42 | snssd 4340 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝐶} ⊆ 𝑋) |
115 | | ssequn2 3786 |
. . . . . . . . . . . . . 14
⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋) |
116 | 114, 115 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋) |
117 | 113, 116 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋) |
118 | 117 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑋)) |
119 | 118 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑋))) |
120 | | undif1 4043 |
. . . . . . . . . . 11
⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶}) |
121 | 42, 69 | elind 3798 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌)) |
122 | 121 | snssd 4340 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌)) |
123 | | ssequn2 3786 |
. . . . . . . . . . . 12
⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
124 | 122, 123 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
125 | 120, 124 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
126 | 119, 125 | fveq12d 6197 |
. . . . . . . . 9
⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
127 | 112, 126 | eleqtrrd 2704 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
128 | 83, 85, 86, 3, 87, 127 | limcres 23650 |
. . . . . . 7
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
129 | 85 | resmptd 5452 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))) |
130 | 129 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
131 | 128, 130 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
132 | 81, 131 | eleqtrd 2703 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
133 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌) |
134 | 133, 3 | dvcnp2 23683 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
135 | 5, 13, 14, 68, 134 | syl31anc 1329 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
136 | 3, 133 | cnplimc 23651 |
. . . . . . . . 9
⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
137 | 64, 69, 136 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
138 | 135, 137 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶))) |
139 | 138 | simprd 479 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)) |
140 | | difss 3737 |
. . . . . . . . . 10
⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) |
141 | 140, 57 | sstri 3612 |
. . . . . . . . 9
⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌 |
142 | 141 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌) |
143 | | eqid 2622 |
. . . . . . . 8
⊢ (𝐽 ↾t (𝑌 ∪ {𝐶})) = (𝐽 ↾t (𝑌 ∪ {𝐶})) |
144 | | difssd 3738 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∪ (𝐽
↾t 𝑆)
∖ 𝑌) ⊆ ∪ (𝐽
↾t 𝑆)) |
145 | 89, 144 | unssd 3789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪
(𝐽 ↾t
𝑆)) |
146 | | ssun1 3776 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) |
147 | 146 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) |
148 | 28 | ntrss 20859 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪
(𝐽 ↾t
𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
149 | 23, 145, 147, 148 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
150 | 149, 31 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
151 | 150, 69 | elind 3798 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
152 | 57 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌) |
153 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ↾t 𝑆) ↾t 𝑌) = ((𝐽 ↾t 𝑆) ↾t 𝑌) |
154 | 28, 153 | restntr 20986 |
. . . . . . . . . . . 12
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽
↾t 𝑆)
∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
155 | 23, 27, 152, 154 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
156 | | restabs 20969 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
157 | 103, 14, 106, 156 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
158 | 157 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑌)) = (int‘(𝐽 ↾t 𝑌))) |
159 | 158 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
160 | 155, 159 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
161 | 151, 160 | eleqtrd 2703 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
162 | 69 | snssd 4340 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝐶} ⊆ 𝑌) |
163 | | ssequn2 3786 |
. . . . . . . . . . . . 13
⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌) |
164 | 162, 163 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌) |
165 | 164 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 ↾t (𝑌 ∪ {𝐶})) = (𝐽 ↾t 𝑌)) |
166 | 165 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 → (int‘(𝐽 ↾t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑌))) |
167 | 166, 125 | fveq12d 6197 |
. . . . . . . . 9
⊢ (𝜑 → ((int‘(𝐽 ↾t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
168 | 161, 167 | eleqtrrd 2704 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
169 | 13, 142, 64, 3, 143, 168 | limcres 23650 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = (𝐺 limℂ 𝐶)) |
170 | 13, 142 | feqresmpt 6250 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧))) |
171 | 170 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
172 | 169, 171 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → (𝐺 limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
173 | 139, 172 | eleqtrd 2703 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
174 | 3 | mulcn 22670 |
. . . . . 6
⊢ ·
∈ ((𝐽
×t 𝐽) Cn
𝐽) |
175 | 5, 6, 7 | dvcl 23663 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ) |
176 | 1, 175 | mpdan 702 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℂ) |
177 | 13, 69 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ) |
178 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝐾 ∈ ℂ ∧ (𝐺‘𝐶) ∈ ℂ) → 〈𝐾, (𝐺‘𝐶)〉 ∈ (ℂ ×
ℂ)) |
179 | 176, 177,
178 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 〈𝐾, (𝐺‘𝐶)〉 ∈ (ℂ ×
ℂ)) |
180 | 77 | cncnpi 21082 |
. . . . . 6
⊢ ((
· ∈ ((𝐽
×t 𝐽) Cn
𝐽) ∧ 〈𝐾, (𝐺‘𝐶)〉 ∈ (ℂ × ℂ))
→ · ∈ (((𝐽
×t 𝐽) CnP
𝐽)‘〈𝐾, (𝐺‘𝐶)〉)) |
181 | 174, 179,
180 | sylancr 695 |
. . . . 5
⊢ (𝜑 → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, (𝐺‘𝐶)〉)) |
182 | 55, 59, 74, 74, 3, 80, 132, 173, 181 | limccnp2 23656 |
. . . 4
⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) limℂ 𝐶)) |
183 | 16 | simprd 479 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
184 | 70, 12 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ) |
185 | 64 | ssdifssd 3748 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ) |
186 | | eqid 2622 |
. . . . . . . 8
⊢ (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) |
187 | | undif1 4043 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶}) |
188 | 187, 164 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌) |
189 | 188 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑌)) |
190 | 189 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑌))) |
191 | 190, 125 | fveq12d 6197 |
. . . . . . . . 9
⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
192 | 161, 191 | eleqtrrd 2704 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
193 | 184, 62, 185, 3, 186, 192 | limcres 23650 |
. . . . . . 7
⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
194 | 62 | resmptd 5452 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
195 | 194 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
196 | 193, 195 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
197 | 183, 196 | eleqtrd 2703 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
198 | 88, 5 | sstrd 3613 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ) |
199 | | cncfmptc 22714 |
. . . . . . . 8
⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑧 ∈
(𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ)) |
200 | 43, 198, 74, 199 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ)) |
201 | | eqidd 2623 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶)) |
202 | 200, 121,
201 | cnmptlimc 23654 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
203 | 43 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ) |
204 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) = (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) |
205 | 203, 204 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ) |
206 | 205 | limcdif 23640 |
. . . . . . 7
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶)) |
207 | | resmpt 5449 |
. . . . . . . . 9
⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶))) |
208 | 140, 207 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶))) |
209 | 208 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
210 | 206, 209 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
211 | 202, 210 | eleqtrd 2703 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
212 | 5, 13, 14 | dvcl 23663 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ) |
213 | 11, 212 | mpdan 702 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℂ) |
214 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝐿 ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → 〈𝐿, (𝐹‘𝐶)〉 ∈ (ℂ ×
ℂ)) |
215 | 213, 43, 214 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 〈𝐿, (𝐹‘𝐶)〉 ∈ (ℂ ×
ℂ)) |
216 | 77 | cncnpi 21082 |
. . . . . 6
⊢ ((
· ∈ ((𝐽
×t 𝐽) Cn
𝐽) ∧ 〈𝐿, (𝐹‘𝐶)〉 ∈ (ℂ × ℂ))
→ · ∈ (((𝐽
×t 𝐽) CnP
𝐽)‘〈𝐿, (𝐹‘𝐶)〉)) |
217 | 174, 215,
216 | sylancr 695 |
. . . . 5
⊢ (𝜑 → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐿, (𝐹‘𝐶)〉)) |
218 | 71, 44, 74, 74, 3, 80, 197, 211, 217 | limccnp2 23656 |
. . . 4
⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) limℂ 𝐶)) |
219 | 3 | addcn 22668 |
. . . . 5
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
220 | 176, 177 | mulcld 10060 |
. . . . . 6
⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ) |
221 | 213, 43 | mulcld 10060 |
. . . . . 6
⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ) |
222 | | opelxpi 5148 |
. . . . . 6
⊢ (((𝐾 · (𝐺‘𝐶)) ∈ ℂ ∧ (𝐿 · (𝐹‘𝐶)) ∈ ℂ) → 〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉 ∈ (ℂ ×
ℂ)) |
223 | 220, 221,
222 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉 ∈ (ℂ ×
ℂ)) |
224 | 77 | cncnpi 21082 |
. . . . 5
⊢ (( +
∈ ((𝐽
×t 𝐽) Cn
𝐽) ∧ 〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉 ∈ (ℂ × ℂ))
→ + ∈ (((𝐽
×t 𝐽) CnP
𝐽)‘〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉)) |
225 | 219, 223,
224 | sylancr 695 |
. . . 4
⊢ (𝜑 → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉)) |
226 | 60, 72, 74, 74, 3, 80, 182, 218, 225 | limccnp2 23656 |
. . 3
⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) limℂ 𝐶)) |
227 | 42 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋) |
228 | 32, 227 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
229 | 37, 228 | subcld 10392 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ) |
230 | 229, 59 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ) |
231 | 69 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌) |
232 | 56, 231 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ) |
233 | 59, 232 | subcld 10392 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ) |
234 | 233, 228 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ) |
235 | 47, 227 | sseldd 3604 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ) |
236 | 48, 235 | subcld 10392 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ) |
237 | 230, 234,
236, 54 | divdird 10839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)))) |
238 | 37, 59 | mulcld 10060 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ) |
239 | 228, 59 | mulcld 10060 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ) |
240 | 228, 232 | mulcld 10060 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ) |
241 | 238, 239,
240 | npncand 10416 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
242 | 37, 228, 59 | subdird 10487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧)))) |
243 | 233, 228 | mulcomd 10061 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶)))) |
244 | 228, 59, 232 | subdid 10486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
245 | 243, 244 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
246 | 242, 245 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))) |
247 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑋⟶ℂ → 𝐹 Fn 𝑋) |
248 | 6, 247 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn 𝑋) |
249 | 248 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋) |
250 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝑌⟶ℂ → 𝐺 Fn 𝑌) |
251 | 13, 250 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 Fn 𝑌) |
252 | 251 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌) |
253 | | ssexg 4804 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ⊆ ℂ ∧ ℂ
∈ V) → 𝑋 ∈
V) |
254 | 46, 104, 253 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ V) |
255 | 254 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V) |
256 | | ssexg 4804 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ⊆ ℂ ∧ ℂ
∈ V) → 𝑌 ∈
V) |
257 | 64, 104, 256 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ V) |
258 | 257 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V) |
259 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌) |
260 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
261 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
262 | 249, 252,
255, 258, 259, 260, 261 | ofval 6906 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘𝑓 · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
263 | 35, 262 | mpdan 702 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘𝑓 · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
264 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶)) |
265 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶)) |
266 | 249, 252,
255, 258, 259, 264, 265 | ofval 6906 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘𝑓 · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶))) |
267 | 121, 266 | mpidan 704 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘𝑓 · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶))) |
268 | 263, 267 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
269 | 241, 246,
268 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶))) |
270 | 269 | oveq1d 6665 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
271 | 229, 59, 236, 54 | div23d 10838 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) |
272 | 233, 228,
236, 54 | div23d 10838 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) |
273 | 271, 272 | oveq12d 6668 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) |
274 | 237, 270,
273 | 3eqtr3d 2664 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) |
275 | 274 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))) |
276 | 275 | oveq1d 6665 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) limℂ 𝐶)) |
277 | 226, 276 | eleqtrrd 2704 |
. 2
⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
278 | | eqid 2622 |
. . 3
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
279 | | mulcl 10020 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
280 | 279 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
281 | 280, 6, 13, 254, 257, 259 | off 6912 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ) |
282 | 2, 3, 278, 5, 281, 88 | eldv 23662 |
. 2
⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘𝑓 · 𝐺)‘𝑧) − ((𝐹 ∘𝑓 · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
283 | 31, 277, 282 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘𝑓 · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶)))) |