Step | Hyp | Ref
| Expression |
1 | | eldmg 5564 |
. . 3
⊢ (𝐵 ∈ dom (𝑆 D 𝐹) → (𝐵 ∈ dom (𝑆 D 𝐹) ↔ ∃𝑦 𝐵(𝑆 D 𝐹)𝑦)) |
2 | 1 | ibi 259 |
. 2
⊢ (𝐵 ∈ dom (𝑆 D 𝐹) → ∃𝑦 𝐵(𝑆 D 𝐹)𝑦) |
3 | | simpl2 1201 |
. . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹:𝐴⟶ℂ) |
4 | 3 | ffvelrnda 6623 |
. . . . . . . . 9
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
5 | | dvcnp.k |
. . . . . . . . . . . . . . 15
⊢ 𝐾 =
(TopOpen‘ℂfld) |
6 | 5 | cnfldtop 22995 |
. . . . . . . . . . . . . 14
⊢ 𝐾 ∈ Top |
7 | | simpl1 1199 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 ⊆ ℂ) |
8 | | cnex 10353 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ V |
9 | | ssexg 5041 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
10 | 7, 8, 9 | sylancl 580 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 ∈ V) |
11 | | resttop 21372 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ 𝑆 ∈ V) → (𝐾 ↾t 𝑆) ∈ Top) |
12 | 6, 10, 11 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐾 ↾t 𝑆) ∈ Top) |
13 | | simpl3 1203 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 ⊆ 𝑆) |
14 | 5 | cnfldtopon 22994 |
. . . . . . . . . . . . . . . 16
⊢ 𝐾 ∈
(TopOn‘ℂ) |
15 | | resttopon 21373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ (𝐾
↾t 𝑆)
∈ (TopOn‘𝑆)) |
16 | 14, 7, 15 | sylancr 581 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆)) |
17 | | toponuni 21126 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐾 ↾t 𝑆)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 = ∪ (𝐾 ↾t 𝑆)) |
19 | 13, 18 | sseqtrd 3859 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 ⊆ ∪ (𝐾 ↾t 𝑆)) |
20 | | eqid 2777 |
. . . . . . . . . . . . . 14
⊢ ∪ (𝐾
↾t 𝑆) =
∪ (𝐾 ↾t 𝑆) |
21 | 20 | ntrss2 21269 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ↾t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ (𝐾
↾t 𝑆))
→ ((int‘(𝐾
↾t 𝑆))‘𝐴) ⊆ 𝐴) |
22 | 12, 19, 21 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((int‘(𝐾 ↾t 𝑆))‘𝐴) ⊆ 𝐴) |
23 | | eqid 2777 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ↾t 𝑆) = (𝐾 ↾t 𝑆) |
24 | | eqid 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) |
25 | | simp1 1127 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → 𝑆 ⊆ ℂ) |
26 | | simp2 1128 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → 𝐹:𝐴⟶ℂ) |
27 | | simp3 1129 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → 𝐴 ⊆ 𝑆) |
28 | 23, 5, 24, 25, 26, 27 | eldv 24099 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → (𝐵(𝑆 D 𝐹)𝑦 ↔ (𝐵 ∈ ((int‘(𝐾 ↾t 𝑆))‘𝐴) ∧ 𝑦 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) limℂ 𝐵)))) |
29 | 28 | simprbda 494 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ((int‘(𝐾 ↾t 𝑆))‘𝐴)) |
30 | 22, 29 | sseldd 3821 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ 𝐴) |
31 | 3, 30 | ffvelrnd 6624 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹‘𝐵) ∈ ℂ) |
32 | 31 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℂ) |
33 | 4, 32 | subcld 10734 |
. . . . . . . 8
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) − (𝐹‘𝐵)) ∈ ℂ) |
34 | | ssid 3841 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ℂ ⊆
ℂ) |
36 | | txtopon 21803 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝐾 ∈
(TopOn‘ℂ)) → (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ ×
ℂ))) |
37 | 14, 14, 36 | mp2an 682 |
. . . . . . . . 9
⊢ (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ
× ℂ)) |
38 | 37 | toponrestid 21133 |
. . . . . . . 8
⊢ (𝐾 ×t 𝐾) = ((𝐾 ×t 𝐾) ↾t (ℂ ×
ℂ)) |
39 | 13, 7 | sstrd 3830 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 ⊆ ℂ) |
40 | 3, 39, 30 | dvlem 24097 |
. . . . . . . . . . 11
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) ∈ ℂ) |
41 | 39 | ssdifssd 3970 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
42 | 41 | sselda 3820 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ) |
43 | 39, 30 | sseldd 3821 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ℂ) |
44 | 43 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
45 | 42, 44 | subcld 10734 |
. . . . . . . . . . 11
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 − 𝐵) ∈ ℂ) |
46 | 28 | simplbda 495 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) limℂ 𝐵)) |
47 | | limcresi 24086 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) limℂ 𝐵) ⊆ (((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵) |
48 | | difss 3959 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
49 | | resmpt 5699 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵))) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)) |
51 | 50 | oveq1i 6932 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)) limℂ 𝐵) |
52 | 47, 51 | sseqtri 3855 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) limℂ 𝐵) ⊆ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)) limℂ 𝐵) |
53 | 43 | subidd 10722 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐵 − 𝐵) = 0) |
54 | 5 | subcn 23077 |
. . . . . . . . . . . . . . . 16
⊢ −
∈ ((𝐾
×t 𝐾) Cn
𝐾) |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → − ∈ ((𝐾 ×t 𝐾) Cn 𝐾)) |
56 | | cncfmptid 23123 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑧
∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cn→ℂ)) |
57 | 39, 34, 56 | sylancl 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cn→ℂ)) |
58 | | cncfmptc 23122 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑧
∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ)) |
59 | 43, 39, 35, 58 | syl3anc 1439 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ)) |
60 | 5, 55, 57, 59 | cncfmpt2f 23125 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ∈ (𝐴–cn→ℂ)) |
61 | | oveq1 6929 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐵 → (𝑧 − 𝐵) = (𝐵 − 𝐵)) |
62 | 60, 30, 61 | cnmptlimc 24091 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐵 − 𝐵) ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) limℂ 𝐵)) |
63 | 53, 62 | eqeltrrd 2859 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) limℂ 𝐵)) |
64 | 52, 63 | sseldi 3818 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)) limℂ 𝐵)) |
65 | 5 | mulcn 23078 |
. . . . . . . . . . . 12
⊢ ·
∈ ((𝐾
×t 𝐾) Cn
𝐾) |
66 | 25, 26, 27 | dvcl 24100 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ) |
67 | | 0cn 10368 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℂ |
68 | | opelxpi 5392 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧ 0 ∈
ℂ) → 〈𝑦,
0〉 ∈ (ℂ × ℂ)) |
69 | 66, 67, 68 | sylancl 580 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 〈𝑦, 0〉 ∈ (ℂ ×
ℂ)) |
70 | 37 | toponunii 21128 |
. . . . . . . . . . . . 13
⊢ (ℂ
× ℂ) = ∪ (𝐾 ×t 𝐾) |
71 | 70 | cncnpi 21490 |
. . . . . . . . . . . 12
⊢ ((
· ∈ ((𝐾
×t 𝐾) Cn
𝐾) ∧ 〈𝑦, 0〉 ∈ (ℂ
× ℂ)) → · ∈ (((𝐾 ×t 𝐾) CnP 𝐾)‘〈𝑦, 0〉)) |
72 | 65, 69, 71 | sylancr 581 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → · ∈ (((𝐾 ×t 𝐾) CnP 𝐾)‘〈𝑦, 0〉)) |
73 | 40, 45, 35, 35, 5, 38, 46, 64, 72 | limccnp2 24093 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦 · 0) ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) limℂ 𝐵)) |
74 | 66 | mul01d 10575 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦 · 0) = 0) |
75 | 3 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐹:𝐴⟶ℂ) |
76 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ (𝐴 ∖ {𝐵})) |
77 | 48, 76 | sseldi 3818 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ 𝐴) |
78 | 75, 77 | ffvelrnd 6624 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ ℂ) |
79 | 31 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝐵) ∈ ℂ) |
80 | 78, 79 | subcld 10734 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) − (𝐹‘𝐵)) ∈ ℂ) |
81 | | eldifsni 4553 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ≠ 𝐵) |
82 | 81 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ≠ 𝐵) |
83 | 42, 44, 82 | subne0d 10743 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 − 𝐵) ≠ 0) |
84 | 80, 45, 83 | divcan1d 11152 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵)) = ((𝐹‘𝑧) − (𝐹‘𝐵))) |
85 | 84 | mpteq2dva 4979 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵)))) |
86 | 85 | oveq1d 6937 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) limℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) limℂ 𝐵)) |
87 | 73, 74, 86 | 3eltr3d 2872 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) limℂ 𝐵)) |
88 | 33 | fmpttd 6649 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))):𝐴⟶ℂ) |
89 | 88 | limcdif 24077 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) limℂ 𝐵) = (((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵)) |
90 | | resmpt 5699 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵)))) |
91 | 48, 90 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) |
92 | 91 | oveq1i 6932 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) limℂ 𝐵) |
93 | 89, 92 | syl6eq 2829 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) limℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) limℂ 𝐵)) |
94 | 87, 93 | eleqtrrd 2861 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) limℂ 𝐵)) |
95 | | cncfmptc 23122 |
. . . . . . . . . 10
⊢ (((𝐹‘𝐵) ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑧 ∈
𝐴 ↦ (𝐹‘𝐵)) ∈ (𝐴–cn→ℂ)) |
96 | 31, 39, 35, 95 | syl3anc 1439 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ (𝐴–cn→ℂ)) |
97 | | eqidd 2778 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝐹‘𝐵) = (𝐹‘𝐵)) |
98 | 96, 30, 97 | cnmptlimc 24091 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹‘𝐵) ∈ ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝐵)) limℂ 𝐵)) |
99 | 5 | addcn 23076 |
. . . . . . . . 9
⊢ + ∈
((𝐾 ×t
𝐾) Cn 𝐾) |
100 | | opelxpi 5392 |
. . . . . . . . . 10
⊢ ((0
∈ ℂ ∧ (𝐹‘𝐵) ∈ ℂ) → 〈0, (𝐹‘𝐵)〉 ∈ (ℂ ×
ℂ)) |
101 | 67, 31, 100 | sylancr 581 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 〈0, (𝐹‘𝐵)〉 ∈ (ℂ ×
ℂ)) |
102 | 70 | cncnpi 21490 |
. . . . . . . . 9
⊢ (( +
∈ ((𝐾
×t 𝐾) Cn
𝐾) ∧ 〈0, (𝐹‘𝐵)〉 ∈ (ℂ × ℂ))
→ + ∈ (((𝐾
×t 𝐾) CnP
𝐾)‘〈0, (𝐹‘𝐵)〉)) |
103 | 99, 101, 102 | sylancr 581 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → + ∈ (((𝐾 ×t 𝐾) CnP 𝐾)‘〈0, (𝐹‘𝐵)〉)) |
104 | 33, 32, 35, 35, 5, 38, 94, 98, 103 | limccnp2 24093 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (0 + (𝐹‘𝐵)) ∈ ((𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) limℂ 𝐵)) |
105 | 31 | addid2d 10577 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (0 + (𝐹‘𝐵)) = (𝐹‘𝐵)) |
106 | 4, 32 | npcand 10738 |
. . . . . . . . . 10
⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵)) = (𝐹‘𝑧)) |
107 | 106 | mpteq2dva 4979 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))) |
108 | 3 | feqmptd 6509 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))) |
109 | 107, 108 | eqtr4d 2816 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) = 𝐹) |
110 | 109 | oveq1d 6937 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) limℂ 𝐵) = (𝐹 limℂ 𝐵)) |
111 | 104, 105,
110 | 3eltr3d 2872 |
. . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)) |
112 | | dvcnp.j |
. . . . . . . 8
⊢ 𝐽 = (𝐾 ↾t 𝐴) |
113 | 5, 112 | cnplimc 24088 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)))) |
114 | 39, 30, 113 | syl2anc 579 |
. . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵)))) |
115 | 3, 111, 114 | mpbir2and 703 |
. . . . 5
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) |
116 | 115 | ex 403 |
. . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → (𝐵(𝑆 D 𝐹)𝑦 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
117 | 116 | exlimdv 1976 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → (∃𝑦 𝐵(𝑆 D 𝐹)𝑦 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
118 | 117 | imp 397 |
. 2
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ ∃𝑦 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) |
119 | 2, 118 | sylan2 586 |
1
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) |