MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvcnp2 Structured version   Visualization version   GIF version

Theorem dvcnp2 23403
Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
dvcnp.j 𝐽 = (𝐾t 𝐴)
dvcnp.k 𝐾 = (TopOpen‘ℂfld)
Assertion
Ref Expression
dvcnp2 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))

Proof of Theorem dvcnp2
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldmg 5225 . . 3 (𝐵 ∈ dom (𝑆 D 𝐹) → (𝐵 ∈ dom (𝑆 D 𝐹) ↔ ∃𝑦 𝐵(𝑆 D 𝐹)𝑦))
21ibi 254 . 2 (𝐵 ∈ dom (𝑆 D 𝐹) → ∃𝑦 𝐵(𝑆 D 𝐹)𝑦)
3 simpl2 1057 . . . . . 6 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹:𝐴⟶ℂ)
43ffvelrnda 6249 . . . . . . . . 9 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ ℂ)
5 dvcnp.k . . . . . . . . . . . . . . 15 𝐾 = (TopOpen‘ℂfld)
65cnfldtop 22326 . . . . . . . . . . . . . 14 𝐾 ∈ Top
7 simpl1 1056 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 ⊆ ℂ)
8 cnex 9870 . . . . . . . . . . . . . . 15 ℂ ∈ V
9 ssexg 4724 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
107, 8, 9sylancl 692 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 ∈ V)
11 resttop 20713 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑆 ∈ V) → (𝐾t 𝑆) ∈ Top)
126, 10, 11sylancr 693 . . . . . . . . . . . . 13 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐾t 𝑆) ∈ Top)
13 simpl3 1058 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴𝑆)
145cnfldtopon 22325 . . . . . . . . . . . . . . . 16 𝐾 ∈ (TopOn‘ℂ)
15 resttopon 20714 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾t 𝑆) ∈ (TopOn‘𝑆))
1614, 7, 15sylancr 693 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐾t 𝑆) ∈ (TopOn‘𝑆))
17 toponuni 20481 . . . . . . . . . . . . . . 15 ((𝐾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = (𝐾t 𝑆))
1816, 17syl 17 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 = (𝐾t 𝑆))
1913, 18sseqtrd 3600 . . . . . . . . . . . . 13 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 (𝐾t 𝑆))
20 eqid 2606 . . . . . . . . . . . . . 14 (𝐾t 𝑆) = (𝐾t 𝑆)
2120ntrss2 20610 . . . . . . . . . . . . 13 (((𝐾t 𝑆) ∈ Top ∧ 𝐴 (𝐾t 𝑆)) → ((int‘(𝐾t 𝑆))‘𝐴) ⊆ 𝐴)
2212, 19, 21syl2anc 690 . . . . . . . . . . . 12 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((int‘(𝐾t 𝑆))‘𝐴) ⊆ 𝐴)
23 eqid 2606 . . . . . . . . . . . . . 14 (𝐾t 𝑆) = (𝐾t 𝑆)
24 eqid 2606 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵))) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵)))
25 simp1 1053 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) → 𝑆 ⊆ ℂ)
26 simp2 1054 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) → 𝐹:𝐴⟶ℂ)
27 simp3 1055 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) → 𝐴𝑆)
2823, 5, 24, 25, 26, 27eldv 23382 . . . . . . . . . . . . 13 ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) → (𝐵(𝑆 D 𝐹)𝑦 ↔ (𝐵 ∈ ((int‘(𝐾t 𝑆))‘𝐴) ∧ 𝑦 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵))) lim 𝐵))))
2928simprbda 650 . . . . . . . . . . . 12 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ((int‘(𝐾t 𝑆))‘𝐴))
3022, 29sseldd 3565 . . . . . . . . . . 11 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵𝐴)
313, 30ffvelrnd 6250 . . . . . . . . . 10 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹𝐵) ∈ ℂ)
3231adantr 479 . . . . . . . . 9 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧𝐴) → (𝐹𝐵) ∈ ℂ)
334, 32subcld 10240 . . . . . . . 8 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧𝐴) → ((𝐹𝑧) − (𝐹𝐵)) ∈ ℂ)
34 ssid 3583 . . . . . . . . 9 ℂ ⊆ ℂ
3534a1i 11 . . . . . . . 8 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ℂ ⊆ ℂ)
36 txtopon 21143 . . . . . . . . . . 11 ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝐾 ∈ (TopOn‘ℂ)) → (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ × ℂ)))
3714, 14, 36mp2an 703 . . . . . . . . . 10 (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ × ℂ))
3837toponunii 20486 . . . . . . . . . . 11 (ℂ × ℂ) = (𝐾 ×t 𝐾)
3938restid 15860 . . . . . . . . . 10 ((𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ × ℂ)) → ((𝐾 ×t 𝐾) ↾t (ℂ × ℂ)) = (𝐾 ×t 𝐾))
4037, 39ax-mp 5 . . . . . . . . 9 ((𝐾 ×t 𝐾) ↾t (ℂ × ℂ)) = (𝐾 ×t 𝐾)
4140eqcomi 2615 . . . . . . . 8 (𝐾 ×t 𝐾) = ((𝐾 ×t 𝐾) ↾t (ℂ × ℂ))
4213, 7sstrd 3574 . . . . . . . . . . . 12 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 ⊆ ℂ)
433, 42, 30dvlem 23380 . . . . . . . . . . 11 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵)) ∈ ℂ)
4442ssdifssd 3706 . . . . . . . . . . . . 13 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐴 ∖ {𝐵}) ⊆ ℂ)
4544sselda 3564 . . . . . . . . . . . 12 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ)
4642, 30sseldd 3565 . . . . . . . . . . . . 13 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ℂ)
4746adantr 479 . . . . . . . . . . . 12 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
4845, 47subcld 10240 . . . . . . . . . . 11 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧𝐵) ∈ ℂ)
4928simplbda 651 . . . . . . . . . . 11 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵))) lim 𝐵))
50 limcresi 23369 . . . . . . . . . . . . 13 ((𝑧𝐴 ↦ (𝑧𝐵)) lim 𝐵) ⊆ (((𝑧𝐴 ↦ (𝑧𝐵)) ↾ (𝐴 ∖ {𝐵})) lim 𝐵)
51 difss 3695 . . . . . . . . . . . . . . 15 (𝐴 ∖ {𝐵}) ⊆ 𝐴
52 resmpt 5353 . . . . . . . . . . . . . . 15 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑧𝐴 ↦ (𝑧𝐵)) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧𝐵)))
5351, 52ax-mp 5 . . . . . . . . . . . . . 14 ((𝑧𝐴 ↦ (𝑧𝐵)) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧𝐵))
5453oveq1i 6534 . . . . . . . . . . . . 13 (((𝑧𝐴 ↦ (𝑧𝐵)) ↾ (𝐴 ∖ {𝐵})) lim 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧𝐵)) lim 𝐵)
5550, 54sseqtri 3596 . . . . . . . . . . . 12 ((𝑧𝐴 ↦ (𝑧𝐵)) lim 𝐵) ⊆ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧𝐵)) lim 𝐵)
5646subidd 10228 . . . . . . . . . . . . 13 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐵𝐵) = 0)
575subcn 22405 . . . . . . . . . . . . . . . 16 − ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
5857a1i 11 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → − ∈ ((𝐾 ×t 𝐾) Cn 𝐾))
59 cncfmptid 22451 . . . . . . . . . . . . . . . 16 ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧𝐴𝑧) ∈ (𝐴cn→ℂ))
6042, 34, 59sylancl 692 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧𝐴𝑧) ∈ (𝐴cn→ℂ))
61 cncfmptc 22450 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧𝐴𝐵) ∈ (𝐴cn→ℂ))
6246, 42, 35, 61syl3anc 1317 . . . . . . . . . . . . . . 15 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧𝐴𝐵) ∈ (𝐴cn→ℂ))
635, 58, 60, 62cncfmpt2f 22453 . . . . . . . . . . . . . 14 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧𝐴 ↦ (𝑧𝐵)) ∈ (𝐴cn→ℂ))
64 oveq1 6531 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → (𝑧𝐵) = (𝐵𝐵))
6563, 30, 64cnmptlimc 23374 . . . . . . . . . . . . 13 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐵𝐵) ∈ ((𝑧𝐴 ↦ (𝑧𝐵)) lim 𝐵))
6656, 65eqeltrrd 2685 . . . . . . . . . . . 12 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧𝐴 ↦ (𝑧𝐵)) lim 𝐵))
6755, 66sseldi 3562 . . . . . . . . . . 11 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧𝐵)) lim 𝐵))
685mulcn 22406 . . . . . . . . . . . 12 · ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
6925, 26, 27dvcl 23383 . . . . . . . . . . . . 13 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ)
70 0cn 9885 . . . . . . . . . . . . 13 0 ∈ ℂ
71 opelxpi 5059 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → ⟨𝑦, 0⟩ ∈ (ℂ × ℂ))
7269, 70, 71sylancl 692 . . . . . . . . . . . 12 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ⟨𝑦, 0⟩ ∈ (ℂ × ℂ))
7338cncnpi 20831 . . . . . . . . . . . 12 (( · ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ∧ ⟨𝑦, 0⟩ ∈ (ℂ × ℂ)) → · ∈ (((𝐾 ×t 𝐾) CnP 𝐾)‘⟨𝑦, 0⟩))
7468, 72, 73sylancr 693 . . . . . . . . . . 11 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → · ∈ (((𝐾 ×t 𝐾) CnP 𝐾)‘⟨𝑦, 0⟩))
7543, 48, 35, 35, 5, 41, 49, 67, 74limccnp2 23376 . . . . . . . . . 10 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦 · 0) ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵)) · (𝑧𝐵))) lim 𝐵))
7669mul01d 10083 . . . . . . . . . 10 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦 · 0) = 0)
773adantr 479 . . . . . . . . . . . . . . 15 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐹:𝐴⟶ℂ)
78 simpr 475 . . . . . . . . . . . . . . . 16 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
7951, 78sseldi 3562 . . . . . . . . . . . . . . 15 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧𝐴)
8077, 79ffvelrnd 6250 . . . . . . . . . . . . . 14 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹𝑧) ∈ ℂ)
8131adantr 479 . . . . . . . . . . . . . 14 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹𝐵) ∈ ℂ)
8280, 81subcld 10240 . . . . . . . . . . . . 13 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹𝑧) − (𝐹𝐵)) ∈ ℂ)
83 eldifsni 4257 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧𝐵)
8483adantl 480 . . . . . . . . . . . . . 14 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧𝐵)
8545, 47, 84subne0d 10249 . . . . . . . . . . . . 13 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧𝐵) ≠ 0)
8682, 48, 85divcan1d 10648 . . . . . . . . . . . 12 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵)) · (𝑧𝐵)) = ((𝐹𝑧) − (𝐹𝐵)))
8786mpteq2dva 4663 . . . . . . . . . . 11 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵)) · (𝑧𝐵))) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹𝑧) − (𝐹𝐵))))
8887oveq1d 6539 . . . . . . . . . 10 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹𝑧) − (𝐹𝐵)) / (𝑧𝐵)) · (𝑧𝐵))) lim 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹𝑧) − (𝐹𝐵))) lim 𝐵))
8975, 76, 883eltr3d 2698 . . . . . . . . 9 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹𝑧) − (𝐹𝐵))) lim 𝐵))
90 eqid 2606 . . . . . . . . . . . 12 (𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) = (𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵)))
9133, 90fmptd 6274 . . . . . . . . . . 11 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))):𝐴⟶ℂ)
9291limcdif 23360 . . . . . . . . . 10 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) lim 𝐵) = (((𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵))
93 resmpt 5353 . . . . . . . . . . . 12 ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹𝑧) − (𝐹𝐵))))
9451, 93ax-mp 5 . . . . . . . . . . 11 ((𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹𝑧) − (𝐹𝐵)))
9594oveq1i 6534 . . . . . . . . . 10 (((𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) ↾ (𝐴 ∖ {𝐵})) lim 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹𝑧) − (𝐹𝐵))) lim 𝐵)
9692, 95syl6eq 2656 . . . . . . . . 9 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) lim 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹𝑧) − (𝐹𝐵))) lim 𝐵))
9789, 96eleqtrrd 2687 . . . . . . . 8 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧𝐴 ↦ ((𝐹𝑧) − (𝐹𝐵))) lim 𝐵))
98 cncfmptc 22450 . . . . . . . . . 10 (((𝐹𝐵) ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧𝐴 ↦ (𝐹𝐵)) ∈ (𝐴cn→ℂ))
9931, 42, 35, 98syl3anc 1317 . . . . . . . . 9 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧𝐴 ↦ (𝐹𝐵)) ∈ (𝐴cn→ℂ))
100 eqidd 2607 . . . . . . . . 9 (𝑧 = 𝐵 → (𝐹𝐵) = (𝐹𝐵))
10199, 30, 100cnmptlimc 23374 . . . . . . . 8 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹𝐵) ∈ ((𝑧𝐴 ↦ (𝐹𝐵)) lim 𝐵))
1025addcn 22404 . . . . . . . . 9 + ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
103 opelxpi 5059 . . . . . . . . . 10 ((0 ∈ ℂ ∧ (𝐹𝐵) ∈ ℂ) → ⟨0, (𝐹𝐵)⟩ ∈ (ℂ × ℂ))
10470, 31, 103sylancr 693 . . . . . . . . 9 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ⟨0, (𝐹𝐵)⟩ ∈ (ℂ × ℂ))
10538cncnpi 20831 . . . . . . . . 9 (( + ∈ ((𝐾 ×t 𝐾) Cn 𝐾) ∧ ⟨0, (𝐹𝐵)⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐾 ×t 𝐾) CnP 𝐾)‘⟨0, (𝐹𝐵)⟩))
106102, 104, 105sylancr 693 . . . . . . . 8 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → + ∈ (((𝐾 ×t 𝐾) CnP 𝐾)‘⟨0, (𝐹𝐵)⟩))
10733, 32, 35, 35, 5, 41, 97, 101, 106limccnp2 23376 . . . . . . 7 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (0 + (𝐹𝐵)) ∈ ((𝑧𝐴 ↦ (((𝐹𝑧) − (𝐹𝐵)) + (𝐹𝐵))) lim 𝐵))
10831addid2d 10085 . . . . . . 7 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (0 + (𝐹𝐵)) = (𝐹𝐵))
1094, 32npcand 10244 . . . . . . . . . 10 ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧𝐴) → (((𝐹𝑧) − (𝐹𝐵)) + (𝐹𝐵)) = (𝐹𝑧))
110109mpteq2dva 4663 . . . . . . . . 9 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧𝐴 ↦ (((𝐹𝑧) − (𝐹𝐵)) + (𝐹𝐵))) = (𝑧𝐴 ↦ (𝐹𝑧)))
1113feqmptd 6141 . . . . . . . . 9 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 = (𝑧𝐴 ↦ (𝐹𝑧)))
112110, 111eqtr4d 2643 . . . . . . . 8 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧𝐴 ↦ (((𝐹𝑧) − (𝐹𝐵)) + (𝐹𝐵))) = 𝐹)
113112oveq1d 6539 . . . . . . 7 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧𝐴 ↦ (((𝐹𝑧) − (𝐹𝐵)) + (𝐹𝐵))) lim 𝐵) = (𝐹 lim 𝐵))
114107, 108, 1133eltr3d 2698 . . . . . 6 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹𝐵) ∈ (𝐹 lim 𝐵))
115 dvcnp.j . . . . . . . 8 𝐽 = (𝐾t 𝐴)
1165, 115cnplimc 23371 . . . . . . 7 ((𝐴 ⊆ ℂ ∧ 𝐵𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹𝐵) ∈ (𝐹 lim 𝐵))))
11742, 30, 116syl2anc 690 . . . . . 6 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹𝐵) ∈ (𝐹 lim 𝐵))))
1183, 114, 117mpbir2and 958 . . . . 5 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
119118ex 448 . . . 4 ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) → (𝐵(𝑆 D 𝐹)𝑦𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)))
120119exlimdv 1847 . . 3 ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) → (∃𝑦 𝐵(𝑆 D 𝐹)𝑦𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)))
121120imp 443 . 2 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ ∃𝑦 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
1222, 121sylan2 489 1 (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  wne 2776  Vcvv 3169  cdif 3533  wss 3536  {csn 4121  cop 4127   cuni 4363   class class class wbr 4574  cmpt 4634   × cxp 5023  dom cdm 5025  cres 5027  wf 5783  cfv 5787  (class class class)co 6524  cc 9787  0cc0 9789   + caddc 9792   · cmul 9794  cmin 10114   / cdiv 10530  t crest 15847  TopOpenctopn 15848  fldccnfld 19510  Topctop 20456  TopOnctopon 20457  intcnt 20570   Cn ccn 20777   CnP ccnp 20778   ×t ctx 21112  cnccncf 22415   lim climc 23346   D cdv 23347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868  ax-mulf 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-supp 7157  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-2o 7422  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-ixp 7769  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-fsupp 8133  df-fi 8174  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-4 10925  df-5 10926  df-6 10927  df-7 10928  df-8 10929  df-9 10930  df-n0 11137  df-z 11208  df-dec 11323  df-uz 11517  df-q 11618  df-rp 11662  df-xneg 11775  df-xadd 11776  df-xmul 11777  df-icc 12006  df-fz 12150  df-fzo 12287  df-seq 12616  df-exp 12675  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-struct 15640  df-ndx 15641  df-slot 15642  df-base 15643  df-sets 15644  df-ress 15645  df-plusg 15724  df-mulr 15725  df-starv 15726  df-sca 15727  df-vsca 15728  df-ip 15729  df-tset 15730  df-ple 15731  df-ds 15734  df-unif 15735  df-hom 15736  df-cco 15737  df-rest 15849  df-topn 15850  df-0g 15868  df-gsum 15869  df-topgen 15870  df-pt 15871  df-prds 15874  df-xrs 15928  df-qtop 15933  df-imas 15934  df-xps 15936  df-mre 16012  df-mrc 16013  df-acs 16015  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-submnd 17102  df-mulg 17307  df-cntz 17516  df-cmn 17961  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-mopn 19506  df-cnfld 19511  df-top 20460  df-bases 20461  df-topon 20462  df-topsp 20463  df-ntr 20573  df-cn 20780  df-cnp 20781  df-tx 21114  df-hmeo 21307  df-xms 21873  df-ms 21874  df-tms 21875  df-cncf 22417  df-limc 23350  df-dv 23351
This theorem is referenced by:  dvcn  23404  dvmulbr  23422  dvcobr  23429  fouriersw  38925
  Copyright terms: Public domain W3C validator