Step | Hyp | Ref
| Expression |
1 | | dvadd.bf |
. . . . . 6
⊢ (𝜑 → 𝐶(𝑆 D 𝐹)𝐾) |
2 | | eqid 2724 |
. . . . . . 7
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
3 | | dvadd.j |
. . . . . . 7
⊢ 𝐽 =
(TopOpen‘ℂfld) |
4 | | eqid 2724 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) |
5 | | dvaddbr.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
6 | | dvadd.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
7 | | dvadd.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
8 | 2, 3, 4, 5, 6, 7 | eldv 25749 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
9 | 1, 8 | mpbid 231 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
10 | 9 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋)) |
11 | | dvadd.bg |
. . . . . 6
⊢ (𝜑 → 𝐶(𝑆 D 𝐺)𝐿) |
12 | | eqid 2724 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
13 | | dvadd.g |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑌⟶ℂ) |
14 | | dvadd.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ 𝑆) |
15 | 2, 3, 12, 5, 13, 14 | eldv 25749 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
16 | 11, 15 | mpbid 231 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶))) |
17 | 16 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌)) |
18 | 10, 17 | elind 4186 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
19 | 3 | cnfldtopon 24621 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘ℂ) |
20 | | resttopon 22987 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐽
↾t 𝑆)
∈ (TopOn‘𝑆)) |
21 | 19, 5, 20 | sylancr 586 |
. . . . 5
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
22 | | topontop 22737 |
. . . . 5
⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → (𝐽 ↾t 𝑆) ∈ Top) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Top) |
24 | | toponuni 22738 |
. . . . . 6
⊢ ((𝐽 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
25 | 21, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
26 | 7, 25 | sseqtrd 4014 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐽 ↾t 𝑆)) |
27 | 14, 25 | sseqtrd 4014 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ∪ (𝐽 ↾t 𝑆)) |
28 | | eqid 2724 |
. . . . 5
⊢ ∪ (𝐽
↾t 𝑆) =
∪ (𝐽 ↾t 𝑆) |
29 | 28 | ntrin 22887 |
. . . 4
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽
↾t 𝑆)
∧ 𝑌 ⊆ ∪ (𝐽
↾t 𝑆))
→ ((int‘(𝐽
↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
30 | 23, 26, 27, 29 | syl3anc 1368 |
. . 3
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
31 | 18, 30 | eleqtrrd 2828 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌))) |
32 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹:𝑋⟶ℂ) |
33 | | inss1 4220 |
. . . . . . . . 9
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
34 | | eldifi 4118 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ∈ (𝑋 ∩ 𝑌)) |
35 | 34 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑋 ∩ 𝑌)) |
36 | 33, 35 | sselid 3972 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑋) |
37 | 32, 36 | ffvelcdmd 7077 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝑧) ∈ ℂ) |
38 | 5, 6, 7 | dvbss 25752 |
. . . . . . . . . 10
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋) |
39 | | reldv 25721 |
. . . . . . . . . . 11
⊢ Rel
(𝑆 D 𝐹) |
40 | | releldm 5933 |
. . . . . . . . . . 11
⊢ ((Rel
(𝑆 D 𝐹) ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐶 ∈ dom (𝑆 D 𝐹)) |
41 | 39, 1, 40 | sylancr 586 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐹)) |
42 | 38, 41 | sseldd 3975 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
43 | 6, 42 | ffvelcdmd 7077 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
45 | 37, 44 | subcld 11568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ) |
46 | 7, 5 | sstrd 3984 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
47 | 46 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ⊆ ℂ) |
48 | 47, 36 | sseldd 3975 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ ℂ) |
49 | 46, 42 | sseldd 3975 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
50 | 49 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ) |
51 | 48, 50 | subcld 11568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ) |
52 | | eldifsni 4785 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) → 𝑧 ≠ 𝐶) |
53 | 52 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ≠ 𝐶) |
54 | 48, 50, 53 | subne0d 11577 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ≠ 0) |
55 | 45, 51, 54 | divcld 11987 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
56 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺:𝑌⟶ℂ) |
57 | | inss2 4221 |
. . . . . . 7
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
58 | 57, 35 | sselid 3972 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ 𝑌) |
59 | 56, 58 | ffvelcdmd 7077 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝑧) ∈ ℂ) |
60 | 55, 59 | mulcld 11231 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) ∈ ℂ) |
61 | | ssdif 4131 |
. . . . . . . 8
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑌 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶})) |
62 | 57, 61 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑌 ∖ {𝐶})) |
63 | 62 | sselda 3974 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑧 ∈ (𝑌 ∖ {𝐶})) |
64 | 14, 5 | sstrd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
65 | 5, 13, 14 | dvbss 25752 |
. . . . . . . 8
⊢ (𝜑 → dom (𝑆 D 𝐺) ⊆ 𝑌) |
66 | | reldv 25721 |
. . . . . . . . 9
⊢ Rel
(𝑆 D 𝐺) |
67 | | releldm 5933 |
. . . . . . . . 9
⊢ ((Rel
(𝑆 D 𝐺) ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑆 D 𝐺)) |
68 | 66, 11, 67 | sylancr 586 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ dom (𝑆 D 𝐺)) |
69 | 65, 68 | sseldd 3975 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
70 | 13, 64, 69 | dvlem 25747 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
71 | 63, 70 | syldan 590 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
72 | 71, 44 | mulcld 11231 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)) ∈ ℂ) |
73 | | ssidd 3997 |
. . . 4
⊢ (𝜑 → ℂ ⊆
ℂ) |
74 | | txtopon 23417 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐽 ∈
(TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ ×
ℂ))) |
75 | 19, 19, 74 | mp2an 689 |
. . . . 5
⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ
× ℂ)) |
76 | 75 | toponrestid 22745 |
. . . 4
⊢ (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ ×
ℂ)) |
77 | 9 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
78 | 6, 46, 42 | dvlem 25747 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ) |
79 | 78 | fmpttd 7106 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ) |
80 | | ssdif 4131 |
. . . . . . . . . . 11
⊢ ((𝑋 ∩ 𝑌) ⊆ 𝑋 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶})) |
81 | 33, 80 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∖ {𝐶})) |
82 | 46 | ssdifssd 4134 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∖ {𝐶}) ⊆ ℂ) |
83 | | eqid 2724 |
. . . . . . . . . 10
⊢ (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) |
84 | 33, 7 | sstrid 3985 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑆) |
85 | 84, 25 | sseqtrd 4014 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ∪
(𝐽 ↾t
𝑆)) |
86 | | difssd 4124 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∪ (𝐽
↾t 𝑆)
∖ 𝑋) ⊆ ∪ (𝐽
↾t 𝑆)) |
87 | 85, 86 | unssd 4178 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪
(𝐽 ↾t
𝑆)) |
88 | | ssun1 4164 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) |
90 | 28 | ntrss 22881 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)) ⊆ ∪
(𝐽 ↾t
𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
91 | 23, 87, 89, 90 | syl3anc 1368 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
92 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) |
93 | 2, 3, 92, 5, 6, 7 | eldv 25749 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐶(𝑆 D 𝐹)𝐾 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
94 | 1, 93 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))) |
95 | 94 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑋)) |
96 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) |
97 | 2, 3, 96, 5, 13, 14 | eldv 25749 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐶(𝑆 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))) |
98 | 11, 97 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌) ∧ 𝐿 ∈ ((𝑥 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑥) − (𝐺‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))) |
99 | 98 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘𝑌)) |
100 | 95, 99 | elind 4186 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘𝑋) ∩ ((int‘(𝐽 ↾t 𝑆))‘𝑌))) |
101 | 100, 30 | eleqtrrd 2828 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌))) |
102 | 91, 101 | sseldd 3975 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋)))) |
103 | 102, 42 | elind 4186 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
104 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑋) |
105 | | eqid 2724 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t 𝑆) ↾t 𝑋) = ((𝐽 ↾t 𝑆) ↾t 𝑋) |
106 | 28, 105 | restntr 23008 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑋 ⊆ ∪ (𝐽
↾t 𝑆)
∧ (𝑋 ∩ 𝑌) ⊆ 𝑋) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
107 | 23, 26, 104, 106 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋)) |
108 | 3 | cnfldtop 24622 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐽 ∈ Top |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 ∈ Top) |
110 | | cnex 11187 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
111 | | ssexg 5313 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
112 | 5, 110, 111 | sylancl 585 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆 ∈ V) |
113 | | restabs 22991 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
114 | 109, 7, 112, 113 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑋) = (𝐽 ↾t 𝑋)) |
115 | 114 | fveq2d 6885 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑋)) = (int‘(𝐽 ↾t 𝑋))) |
116 | 115 | fveq1d 6883 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑋))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
117 | 107, 116 | eqtr3d 2766 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑋))) ∩ 𝑋) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
118 | 103, 117 | eleqtrd 2827 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
119 | | undif1 4467 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∪ {𝐶}) |
120 | 42 | snssd 4804 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝐶} ⊆ 𝑋) |
121 | | ssequn2 4175 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐶} ⊆ 𝑋 ↔ (𝑋 ∪ {𝐶}) = 𝑋) |
122 | 120, 121 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∪ {𝐶}) = 𝑋) |
123 | 119, 122 | eqtrid 2776 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋 ∖ {𝐶}) ∪ {𝐶}) = 𝑋) |
124 | 123 | oveq2d 7417 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑋)) |
125 | 124 | fveq2d 6885 |
. . . . . . . . . . . 12
⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑋))) |
126 | | undif1 4467 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = ((𝑋 ∩ 𝑌) ∪ {𝐶}) |
127 | 42, 69 | elind 4186 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ (𝑋 ∩ 𝑌)) |
128 | 127 | snssd 4804 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝐶} ⊆ (𝑋 ∩ 𝑌)) |
129 | | ssequn2 4175 |
. . . . . . . . . . . . . 14
⊢ ({𝐶} ⊆ (𝑋 ∩ 𝑌) ↔ ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
130 | 128, 129 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
131 | 126, 130 | eqtrid 2776 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}) = (𝑋 ∩ 𝑌)) |
132 | 125, 131 | fveq12d 6888 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑋))‘(𝑋 ∩ 𝑌))) |
133 | 118, 132 | eleqtrrd 2828 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑋 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
134 | 79, 81, 82, 3, 83, 133 | limcres 25737 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
135 | 81 | resmptd 6030 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)))) |
136 | 135 | oveq1d 7416 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
137 | 134, 136 | eqtr3d 2766 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
138 | 77, 137 | eleqtrd 2827 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
139 | | eqid 2724 |
. . . . . . . . . . . 12
⊢ (𝐽 ↾t 𝑌) = (𝐽 ↾t 𝑌) |
140 | 139, 3 | dvcnp2 25771 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌 ⊆ 𝑆) ∧ 𝐶 ∈ dom (𝑆 D 𝐺)) → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
141 | 5, 13, 14, 68, 140 | syl31anc 1370 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶)) |
142 | 3, 139 | cnplimc 25738 |
. . . . . . . . . . 11
⊢ ((𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌) → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
143 | 64, 69, 142 | syl2anc 583 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ∈ (((𝐽 ↾t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)))) |
144 | 141, 143 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶))) |
145 | 144 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐶) ∈ (𝐺 limℂ 𝐶)) |
146 | | difss 4123 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) |
147 | 146, 57 | sstri 3983 |
. . . . . . . . . . 11
⊢ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌 |
148 | 147 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ 𝑌) |
149 | | eqid 2724 |
. . . . . . . . . 10
⊢ (𝐽 ↾t (𝑌 ∪ {𝐶})) = (𝐽 ↾t (𝑌 ∪ {𝐶})) |
150 | | difssd 4124 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∪ (𝐽
↾t 𝑆)
∖ 𝑌) ⊆ ∪ (𝐽
↾t 𝑆)) |
151 | 85, 150 | unssd 4178 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪
(𝐽 ↾t
𝑆)) |
152 | | ssun1 4164 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) |
154 | 28 | ntrss 22881 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)) ⊆ ∪
(𝐽 ↾t
𝑆) ∧ (𝑋 ∩ 𝑌) ⊆ ((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
155 | 23, 151, 153, 154 | syl3anc 1368 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ⊆ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
156 | 155, 101 | sseldd 3975 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌)))) |
157 | 156, 69 | elind 4186 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
158 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ 𝑌) |
159 | | eqid 2724 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t 𝑆) ↾t 𝑌) = ((𝐽 ↾t 𝑆) ↾t 𝑌) |
160 | 28, 159 | restntr 23008 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝑆) ∈ Top ∧ 𝑌 ⊆ ∪ (𝐽
↾t 𝑆)
∧ (𝑋 ∩ 𝑌) ⊆ 𝑌) → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
161 | 23, 27, 158, 160 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌)) |
162 | | restabs 22991 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V) → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
163 | 109, 14, 112, 162 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐽 ↾t 𝑆) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
164 | 163 | fveq2d 6885 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (int‘((𝐽 ↾t 𝑆) ↾t 𝑌)) = (int‘(𝐽 ↾t 𝑌))) |
165 | 164 | fveq1d 6883 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((int‘((𝐽 ↾t 𝑆) ↾t 𝑌))‘(𝑋 ∩ 𝑌)) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
166 | 161, 165 | eqtr3d 2766 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((int‘(𝐽 ↾t 𝑆))‘((𝑋 ∩ 𝑌) ∪ (∪ (𝐽 ↾t 𝑆) ∖ 𝑌))) ∩ 𝑌) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
167 | 157, 166 | eleqtrd 2827 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
168 | 69 | snssd 4804 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝐶} ⊆ 𝑌) |
169 | | ssequn2 4175 |
. . . . . . . . . . . . . . 15
⊢ ({𝐶} ⊆ 𝑌 ↔ (𝑌 ∪ {𝐶}) = 𝑌) |
170 | 168, 169 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 ∪ {𝐶}) = 𝑌) |
171 | 170 | oveq2d 7417 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 ↾t (𝑌 ∪ {𝐶})) = (𝐽 ↾t 𝑌)) |
172 | 171 | fveq2d 6885 |
. . . . . . . . . . . 12
⊢ (𝜑 → (int‘(𝐽 ↾t (𝑌 ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑌))) |
173 | 172, 131 | fveq12d 6888 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘(𝐽 ↾t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
174 | 167, 173 | eleqtrrd 2828 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t (𝑌 ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
175 | 13, 148, 64, 3, 149, 174 | limcres 25737 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = (𝐺 limℂ 𝐶)) |
176 | 13, 148 | feqresmpt 6951 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧))) |
177 | 176 | oveq1d 7416 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
178 | 175, 177 | eqtr3d 2766 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
179 | 145, 178 | eleqtrd 2827 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐺‘𝑧)) limℂ 𝐶)) |
180 | 3 | mpomulcn 24707 |
. . . . . . . 8
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |
181 | 5, 6, 7 | dvcl 25750 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ) |
182 | 1, 181 | mpdan 684 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℂ) |
183 | 13, 69 | ffvelcdmd 7077 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ) |
184 | 182, 183 | opelxpd 5705 |
. . . . . . . 8
⊢ (𝜑 → 〈𝐾, (𝐺‘𝐶)〉 ∈ (ℂ ×
ℂ)) |
185 | 75 | toponunii 22740 |
. . . . . . . . 9
⊢ (ℂ
× ℂ) = ∪ (𝐽 ×t 𝐽) |
186 | 185 | cncnpi 23104 |
. . . . . . . 8
⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 〈𝐾, (𝐺‘𝐶)〉 ∈ (ℂ × ℂ))
→ (𝑢 ∈ ℂ,
𝑣 ∈ ℂ ↦
(𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, (𝐺‘𝐶)〉)) |
187 | 180, 184,
186 | sylancr 586 |
. . . . . . 7
⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐾, (𝐺‘𝐶)〉)) |
188 | 55, 59, 73, 73, 3, 76, 138, 179, 187 | limccnp2 25743 |
. . . . . 6
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) limℂ 𝐶)) |
189 | | df-mpt 5222 |
. . . . . . 7
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} |
190 | 189 | oveq1i 7411 |
. . . . . 6
⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) limℂ 𝐶) = ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} limℂ 𝐶) |
191 | 188, 190 | eleqtrdi 2835 |
. . . . 5
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) ∈ ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} limℂ 𝐶)) |
192 | | ovmpot 7561 |
. . . . . 6
⊢ ((𝐾 ∈ ℂ ∧ (𝐺‘𝐶) ∈ ℂ) → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶))) |
193 | 182, 183,
192 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → (𝐾(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝐶)) = (𝐾 · (𝐺‘𝐶))) |
194 | | ovmpot 7561 |
. . . . . . . . . . 11
⊢
(((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) |
195 | 55, 59, 194 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) |
196 | 195 | eqeq2d 2735 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ↔ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))) |
197 | 196 | pm5.32da 578 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))))) |
198 | 197 | opabbidv 5204 |
. . . . . . 7
⊢ (𝜑 → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))}) |
199 | | df-mpt 5222 |
. . . . . . 7
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))} |
200 | 198, 199 | eqtr4di 2782 |
. . . . . 6
⊢ (𝜑 → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)))) |
201 | 200 | oveq1d 7416 |
. . . . 5
⊢ (𝜑 → ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) limℂ 𝐶)) |
202 | 191, 193,
201 | 3eltr3d 2839 |
. . . 4
⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) limℂ 𝐶)) |
203 | 16 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
204 | 70 | fmpttd 7106 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))):(𝑌 ∖ {𝐶})⟶ℂ) |
205 | 64 | ssdifssd 4134 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∖ {𝐶}) ⊆ ℂ) |
206 | | eqid 2724 |
. . . . . . . . . 10
⊢ (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) |
207 | | undif1 4467 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = (𝑌 ∪ {𝐶}) |
208 | 207, 170 | eqtrid 2776 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 ∖ {𝐶}) ∪ {𝐶}) = 𝑌) |
209 | 208 | oveq2d 7417 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})) = (𝐽 ↾t 𝑌)) |
210 | 209 | fveq2d 6885 |
. . . . . . . . . . . 12
⊢ (𝜑 → (int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶}))) = (int‘(𝐽 ↾t 𝑌))) |
211 | 210, 131 | fveq12d 6888 |
. . . . . . . . . . 11
⊢ (𝜑 → ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶})) = ((int‘(𝐽 ↾t 𝑌))‘(𝑋 ∩ 𝑌))) |
212 | 167, 211 | eleqtrrd 2828 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ((int‘(𝐽 ↾t ((𝑌 ∖ {𝐶}) ∪ {𝐶})))‘(((𝑋 ∩ 𝑌) ∖ {𝐶}) ∪ {𝐶}))) |
213 | 204, 62, 205, 3, 206, 212 | limcres 25737 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
214 | 62 | resmptd 6030 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))) |
215 | 214 | oveq1d 7416 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
216 | 213, 215 | eqtr3d 2766 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ (𝑌 ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
217 | 203, 216 | eleqtrd 2827 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
218 | 84, 5 | sstrd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∩ 𝑌) ⊆ ℂ) |
219 | | cncfmptc 24754 |
. . . . . . . . . 10
⊢ (((𝐹‘𝐶) ∈ ℂ ∧ (𝑋 ∩ 𝑌) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑧 ∈
(𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ)) |
220 | 43, 218, 73, 219 | syl3anc 1368 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ∈ ((𝑋 ∩ 𝑌)–cn→ℂ)) |
221 | | eqidd 2725 |
. . . . . . . . 9
⊢ (𝑧 = 𝐶 → (𝐹‘𝐶) = (𝐹‘𝐶)) |
222 | 220, 127,
221 | cnmptlimc 25741 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
223 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → (𝐹‘𝐶) ∈ ℂ) |
224 | 223 | fmpttd 7106 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)):(𝑋 ∩ 𝑌)⟶ℂ) |
225 | 224 | limcdif 25727 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶) = (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶)) |
226 | | resmpt 6027 |
. . . . . . . . . . 11
⊢ (((𝑋 ∩ 𝑌) ∖ {𝐶}) ⊆ (𝑋 ∩ 𝑌) → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶))) |
227 | 146, 226 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶))) |
228 | 227 | oveq1d 7416 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) ↾ ((𝑋 ∩ 𝑌) ∖ {𝐶})) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
229 | 225, 228 | eqtrd 2764 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ (𝑋 ∩ 𝑌) ↦ (𝐹‘𝐶)) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
230 | 222, 229 | eleqtrd 2827 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (𝐹‘𝐶)) limℂ 𝐶)) |
231 | 5, 13, 14 | dvcl 25750 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶(𝑆 D 𝐺)𝐿) → 𝐿 ∈ ℂ) |
232 | 11, 231 | mpdan 684 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℂ) |
233 | 232, 43 | opelxpd 5705 |
. . . . . . . 8
⊢ (𝜑 → 〈𝐿, (𝐹‘𝐶)〉 ∈ (ℂ ×
ℂ)) |
234 | 185 | cncnpi 23104 |
. . . . . . . 8
⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 〈𝐿, (𝐹‘𝐶)〉 ∈ (ℂ × ℂ))
→ (𝑢 ∈ ℂ,
𝑣 ∈ ℂ ↦
(𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐿, (𝐹‘𝐶)〉)) |
235 | 180, 233,
234 | sylancr 586 |
. . . . . . 7
⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝐿, (𝐹‘𝐶)〉)) |
236 | 71, 44, 73, 73, 3, 76, 217, 230, 235 | limccnp2 25743 |
. . . . . 6
⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) limℂ 𝐶)) |
237 | | df-mpt 5222 |
. . . . . . 7
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} |
238 | 237 | oveq1i 7411 |
. . . . . 6
⊢ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) limℂ 𝐶) = ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} limℂ 𝐶) |
239 | 236, 238 | eleqtrdi 2835 |
. . . . 5
⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ∈ ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} limℂ 𝐶)) |
240 | | ovmpot 7561 |
. . . . . 6
⊢ ((𝐿 ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶))) |
241 | 232, 43, 240 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → (𝐿(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = (𝐿 · (𝐹‘𝐶))) |
242 | 42 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑋) |
243 | 32, 242 | ffvelcdmd 7077 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ) |
244 | | ovmpot 7561 |
. . . . . . . . . . 11
⊢
(((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) |
245 | 71, 243, 244 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) |
246 | 245 | eqeq2d 2735 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)) ↔ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) |
247 | 246 | pm5.32da 578 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶))) ↔ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))) |
248 | 247 | opabbidv 5204 |
. . . . . . 7
⊢ (𝜑 → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))}) |
249 | | df-mpt 5222 |
. . . . . . 7
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) = {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))} |
250 | 248, 249 | eqtr4di 2782 |
. . . . . 6
⊢ (𝜑 → {〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) |
251 | 250 | oveq1d 7416 |
. . . . 5
⊢ (𝜑 → ({〈𝑧, 𝑤〉 ∣ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ∧ 𝑤 = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝐶)))} limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) limℂ 𝐶)) |
252 | 239, 241,
251 | 3eltr3d 2839 |
. . . 4
⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) limℂ 𝐶)) |
253 | 3 | addcn 24703 |
. . . . 5
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
254 | 182, 183 | mulcld 11231 |
. . . . . 6
⊢ (𝜑 → (𝐾 · (𝐺‘𝐶)) ∈ ℂ) |
255 | 232, 43 | mulcld 11231 |
. . . . . 6
⊢ (𝜑 → (𝐿 · (𝐹‘𝐶)) ∈ ℂ) |
256 | 254, 255 | opelxpd 5705 |
. . . . 5
⊢ (𝜑 → 〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉 ∈ (ℂ ×
ℂ)) |
257 | 185 | cncnpi 23104 |
. . . . 5
⊢ (( +
∈ ((𝐽
×t 𝐽) Cn
𝐽) ∧ 〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉 ∈ (ℂ × ℂ))
→ + ∈ (((𝐽
×t 𝐽) CnP
𝐽)‘〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉)) |
258 | 253, 256,
257 | sylancr 586 |
. . . 4
⊢ (𝜑 → + ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈(𝐾 · (𝐺‘𝐶)), (𝐿 · (𝐹‘𝐶))〉)) |
259 | 60, 72, 73, 73, 3, 76, 202, 252, 258 | limccnp2 25743 |
. . 3
⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) limℂ 𝐶)) |
260 | 37, 243 | subcld 11568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) − (𝐹‘𝐶)) ∈ ℂ) |
261 | 260, 59 | mulcld 11231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) ∈ ℂ) |
262 | 69 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ 𝑌) |
263 | 56, 262 | ffvelcdmd 7077 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝐺‘𝐶) ∈ ℂ) |
264 | 59, 263 | subcld 11568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐺‘𝑧) − (𝐺‘𝐶)) ∈ ℂ) |
265 | 264, 243 | mulcld 11231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) ∈ ℂ) |
266 | 47, 242 | sseldd 3975 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐶 ∈ ℂ) |
267 | 48, 266 | subcld 11568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (𝑧 − 𝐶) ∈ ℂ) |
268 | 261, 265,
267, 54 | divdird 12025 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)))) |
269 | 37, 59 | mulcld 11231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ) |
270 | 243, 59 | mulcld 11231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝑧)) ∈ ℂ) |
271 | 243, 263 | mulcld 11231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · (𝐺‘𝐶)) ∈ ℂ) |
272 | 269, 270,
271 | npncand 11592 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
273 | 37, 243, 59 | subdird 11668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧)))) |
274 | 264, 243 | mulcomd 11232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶)))) |
275 | 243, 59, 263 | subdid 11667 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹‘𝐶) · ((𝐺‘𝑧) − (𝐺‘𝐶))) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
276 | 274, 275 | eqtrd 2764 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) = (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
277 | 273, 276 | oveq12d 7419 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = ((((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝑧))) + (((𝐹‘𝐶) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶))))) |
278 | 6 | ffnd 6708 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn 𝑋) |
279 | 278 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐹 Fn 𝑋) |
280 | 13 | ffnd 6708 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 Fn 𝑌) |
281 | 280 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝐺 Fn 𝑌) |
282 | | ssexg 5313 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ⊆ ℂ ∧ ℂ
∈ V) → 𝑋 ∈
V) |
283 | 46, 110, 282 | sylancl 585 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ V) |
284 | 283 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑋 ∈ V) |
285 | | ssexg 5313 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ⊆ ℂ ∧ ℂ
∈ V) → 𝑌 ∈
V) |
286 | 64, 110, 285 | sylancl 585 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ V) |
287 | 286 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → 𝑌 ∈ V) |
288 | | eqid 2724 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝑌) = (𝑋 ∩ 𝑌) |
289 | | eqidd 2725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
290 | | eqidd 2725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ 𝑌) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
291 | 279, 281,
284, 287, 288, 289, 290 | ofval 7674 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝑧 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
292 | 35, 291 | mpdan 684 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘f · 𝐺)‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
293 | | eqidd 2725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑋) → (𝐹‘𝐶) = (𝐹‘𝐶)) |
294 | | eqidd 2725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ 𝑌) → (𝐺‘𝐶) = (𝐺‘𝐶)) |
295 | 279, 281,
284, 287, 288, 293, 294 | ofval 7674 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) ∧ 𝐶 ∈ (𝑋 ∩ 𝑌)) → ((𝐹 ∘f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶))) |
296 | 127, 295 | mpidan 686 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((𝐹 ∘f · 𝐺)‘𝐶) = ((𝐹‘𝐶) · (𝐺‘𝐶))) |
297 | 292, 296 | oveq12d 7419 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − ((𝐹‘𝐶) · (𝐺‘𝐶)))) |
298 | 272, 277,
297 | 3eqtr4d 2774 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) = (((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶))) |
299 | 298 | oveq1d 7416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) + (((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶))) / (𝑧 − 𝐶)) = ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
300 | 260, 59, 267, 54 | div23d 12024 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) = ((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧))) |
301 | 264, 243,
267, 54 | div23d 12024 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶)) = ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))) |
302 | 300, 301 | oveq12d 7419 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → (((((𝐹‘𝑧) − (𝐹‘𝐶)) · (𝐺‘𝑧)) / (𝑧 − 𝐶)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) · (𝐹‘𝐶)) / (𝑧 − 𝐶))) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) |
303 | 268, 299,
302 | 3eqtr3d 2772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶})) → ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶)) = (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) |
304 | 303 | mpteq2dva 5238 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶))))) |
305 | 304 | oveq1d 7416 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶) = ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ (((((𝐹‘𝑧) − (𝐹‘𝐶)) / (𝑧 − 𝐶)) · (𝐺‘𝑧)) + ((((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) · (𝐹‘𝐶)))) limℂ 𝐶)) |
306 | 259, 305 | eleqtrrd 2828 |
. 2
⊢ (𝜑 → ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)) |
307 | | eqid 2724 |
. . 3
⊢ (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) = (𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) |
308 | | mulcl 11190 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
309 | 308 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
310 | 309, 6, 13, 283, 286, 288 | off 7681 |
. . 3
⊢ (𝜑 → (𝐹 ∘f · 𝐺):(𝑋 ∩ 𝑌)⟶ℂ) |
311 | 2, 3, 307, 5, 310, 84 | eldv 25749 |
. 2
⊢ (𝜑 → (𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ↔ (𝐶 ∈ ((int‘(𝐽 ↾t 𝑆))‘(𝑋 ∩ 𝑌)) ∧ ((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶))) ∈ ((𝑧 ∈ ((𝑋 ∩ 𝑌) ∖ {𝐶}) ↦ ((((𝐹 ∘f · 𝐺)‘𝑧) − ((𝐹 ∘f · 𝐺)‘𝐶)) / (𝑧 − 𝐶))) limℂ 𝐶)))) |
312 | 31, 306, 311 | mpbir2and 710 |
1
⊢ (𝜑 → 𝐶(𝑆 D (𝐹 ∘f · 𝐺))((𝐾 · (𝐺‘𝐶)) + (𝐿 · (𝐹‘𝐶)))) |