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