dvcnp2 - Metamath Proof Explorer

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

Theorem dvcnp2 26284

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.) Avoid ax-mulf 11317. (Revised by GG, 16-Mar-2025.)

**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.

Step	Hyp	Ref	Expression
1		simpl2 1211	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹:𝐴⟶ℂ)
2	1	ffvelcdmda 7114	. . . . . . . 8 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ)
3		dvcnp.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
4	3	cnfldtop 25146	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ Top
5		simpl1 1210	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 ⊆ ℂ)
6		cnex 11318	. . . . . . . . . . . . . 14 ⊢ ℂ ∈ V
7		ssexg 5286	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
8	5, 6, 7	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 ∈ V)
9		resttop 23522	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑆 ∈ V) → (𝐾 ↾_t 𝑆) ∈ Top)
10	4, 8, 9	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐾 ↾_t 𝑆) ∈ Top)
11		simpl3 1212	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 ⊆ 𝑆)
12	3	cnfldtopon 25145	. . . . . . . . . . . . . . 15 ⊢ 𝐾 ∈ (TopOn‘ℂ)
13		resttopon 23523	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
14	12, 5, 13	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆))
15		toponuni 23276	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ (𝐾 ↾_t 𝑆))
16	14, 15	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑆 = ∪ (𝐾 ↾_t 𝑆))
17	11, 16	sseqtrd 3949	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 ⊆ ∪ (𝐾 ↾_t 𝑆))
18		eqid 2763	. . . . . . . . . . . . 13 ⊢ ∪ (𝐾 ↾_t 𝑆) = ∪ (𝐾 ↾_t 𝑆)
19	18	ntrss2 23419	. . . . . . . . . . . 12 ⊢ (((𝐾 ↾_t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ (𝐾 ↾_t 𝑆)) → ((int‘(𝐾 ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
20	10, 17, 19	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((int‘(𝐾 ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
21		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝐾 ↾_t 𝑆) = (𝐾 ↾_t 𝑆)
22		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)))
23		simp1 1154	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → 𝑆 ⊆ ℂ)
24		simp2 1155	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → 𝐹:𝐴⟶ℂ)
25		simp3 1156	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → 𝐴 ⊆ 𝑆)
26	21, 3, 22, 23, 24, 25	eldv 26262	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → (𝐵(𝑆 D 𝐹)𝑦 ↔ (𝐵 ∈ ((int‘(𝐾 ↾_t 𝑆))‘𝐴) ∧ 𝑦 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) lim_ℂ 𝐵))))
27	26	simprbda 504	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ((int‘(𝐾 ↾_t 𝑆))‘𝐴))
28	20, 27	sseldd 3914	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ 𝐴)
29	1, 28	ffvelcdmd 7115	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹‘𝐵) ∈ ℂ)
30	29	adantr 486	. . . . . . . 8 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℂ)
31	2, 30	subcld 11706	. . . . . . 7 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) − (𝐹‘𝐵)) ∈ ℂ)
32		ssidd 3936	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ℂ ⊆ ℂ)
33		txtopon 23954	. . . . . . . . 9 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝐾 ∈ (TopOn‘ℂ)) → (𝐾 ×_t 𝐾) ∈ (TopOn‘(ℂ × ℂ)))
34	12, 12, 33	mp2an 705	. . . . . . . 8 ⊢ (𝐾 ×_t 𝐾) ∈ (TopOn‘(ℂ × ℂ))
35	34	toponrestid 23283	. . . . . . 7 ⊢ (𝐾 ×_t 𝐾) = ((𝐾 ×_t 𝐾) ↾_t (ℂ × ℂ))
36	11, 5	sstrd 3923	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐴 ⊆ ℂ)
37		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐵)) / (𝑥 − 𝐵)))
38	21, 3, 37, 23, 24, 25	eldv 26262	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → (𝐵(𝑆 D 𝐹)𝑦 ↔ (𝐵 ∈ ((int‘(𝐾 ↾_t 𝑆))‘𝐴) ∧ 𝑦 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))))
39	38	simprbda 504	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ((int‘(𝐾 ↾_t 𝑆))‘𝐴))
40	20, 39	sseldd 3914	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ 𝐴)
41	1, 36, 40	dvlem 26260	. . . . . . . . . . . 12 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) ∈ ℂ)
42	36	ssdifssd 4086	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐴 ∖ {𝐵}) ⊆ ℂ)
43	42	sselda 3913	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ)
44	36, 40	sseldd 3914	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ℂ)
45	44	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
46	43, 45	subcld 11706	. . . . . . . . . . . 12 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 − 𝐵) ∈ ℂ)
47	26	simplbda 505	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))) lim_ℂ 𝐵))
48		limcresi 26249	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) lim_ℂ 𝐵) ⊆ (((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) lim_ℂ 𝐵)
49		difss 4075	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴
50		resmpt 6045	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)))
51	49, 50	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵))
52	51	oveq1i 7459	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ↾ (𝐴 ∖ {𝐵})) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)) lim_ℂ 𝐵)
53	48, 52	sseqtri 3961	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) lim_ℂ 𝐵) ⊆ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)) lim_ℂ 𝐵)
54	44	subidd 11694	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐵 − 𝐵) = 0)
55		ssid 3935	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ⊆ ℂ
56		cncfmptid 25278	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cn→ℂ))
57	36, 55, 56	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ 𝑧) ∈ (𝐴–cn→ℂ))
58		cncfmptc 25277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))
59	44, 36, 32, 58	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))
60	57, 59	subcncf 25810	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) ∈ (𝐴–cn→ℂ))
61		oveq1 7456	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝐵 → (𝑧 − 𝐵) = (𝐵 − 𝐵))
62	60, 40, 61	cnmptlimc 26254	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐵 − 𝐵) ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) lim_ℂ 𝐵))
63	54, 62	eqeltrrd 2865	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ 𝐴 ↦ (𝑧 − 𝐵)) lim_ℂ 𝐵))
64	53, 63	sselid 3911	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ (𝑧 − 𝐵)) lim_ℂ 𝐵))
65	3	mpomulcn 25232	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐾 ×_t 𝐾) Cn 𝐾)
66	23, 24, 25	dvcl 26263	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝑦 ∈ ℂ)
67		0cn 11335	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℂ
68		opelxpi 5693	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → ⟨𝑦, 0⟩ ∈ (ℂ × ℂ))
69	66, 67, 68	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ⟨𝑦, 0⟩ ∈ (ℂ × ℂ))
70	34	toponunii 23278	. . . . . . . . . . . . . 14 ⊢ (ℂ × ℂ) = ∪ (𝐾 ×_t 𝐾)
71	70	cncnpi 23640	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((𝐾 ×_t 𝐾) Cn 𝐾) ∧ ⟨𝑦, 0⟩ ∈ (ℂ × ℂ)) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐾 ×_t 𝐾) CnP 𝐾)‘⟨𝑦, 0⟩))
72	65, 69, 71	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((𝐾 ×_t 𝐾) CnP 𝐾)‘⟨𝑦, 0⟩))
73	41, 46, 32, 32, 3, 35, 47, 64, 72	limccnp2 26256	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))0) ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵))) lim_ℂ 𝐵))
74		df-mpt 5191	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)))}
75	74	oveq1i 7459	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵))) lim_ℂ 𝐵) = ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)))} lim_ℂ 𝐵)
76	73, 75	eleqtrdi 2874	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))0) ∈ ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)))} lim_ℂ 𝐵))
77		0cnd 11336	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ℂ)
78		ovmpot 7611	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑦(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))0) = (𝑦 · 0))
79	66, 77, 78	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))0) = (𝑦 · 0))
80	1, 36, 28	dvlem 26260	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) ∈ ℂ)
81	36, 28	sseldd 3914	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐵 ∈ ℂ)
82	81	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
83	43, 82	subcld 11706	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 − 𝐵) ∈ ℂ)
84		ovmpot 7611	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) ∈ ℂ ∧ (𝑧 − 𝐵) ∈ ℂ) → ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)) = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵)))
85	80, 83, 84	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)) = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵)))
86	85	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)) ↔ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))))
87	86	pm5.32da 590	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵))) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵)))))
88	87	opabbidv 5175	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵)))})
89		df-mpt 5191	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵)))}
90	88, 89	eqtr4di 2816	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)))} = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))))
91	90	oveq1d 7464	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ({⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑤 = ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝑧 − 𝐵)))} lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) lim_ℂ 𝐵))
92	76, 79, 91	3eltr3d 2878	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦 · 0) ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) lim_ℂ 𝐵))
93	66	mul01d 11546	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑦 · 0) = 0)
94	1	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐹:𝐴⟶ℂ)
95		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
96	49, 95	sselid 3911	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ 𝐴)
97	94, 96	ffvelcdmd 7115	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ ℂ)
98	29	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝐵) ∈ ℂ)
99	97, 98	subcld 11706	. . . . . . . . . . . 12 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) − (𝐹‘𝐵)) ∈ ℂ)
100		eldifsni 4753	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ≠ 𝐵)
101	100	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ≠ 𝐵)
102	43, 82, 101	subne0d 11716	. . . . . . . . . . . 12 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 − 𝐵) ≠ 0)
103	99, 83, 102	divcan1d 12132	. . . . . . . . . . 11 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵)) = ((𝐹‘𝑧) − (𝐹‘𝐵)))
104	103	mpteq2dva 5202	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))))
105	104	oveq1d 7464	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝐹‘𝑧) − (𝐹‘𝐵)) / (𝑧 − 𝐵)) · (𝑧 − 𝐵))) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) lim_ℂ 𝐵))
106	92, 93, 105	3eltr3d 2878	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) lim_ℂ 𝐵))
107	31	fmpttd 7145	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))):𝐴⟶ℂ)
108	107	limcdif 26240	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) lim_ℂ 𝐵) = (((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) lim_ℂ 𝐵))
109		resmpt 6045	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))))
110	49, 109	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) = (𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵)))
111	110	oveq1i 7459	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) ↾ (𝐴 ∖ {𝐵})) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) lim_ℂ 𝐵)
112	108, 111	eqtrdi 2814	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) lim_ℂ 𝐵) = ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) lim_ℂ 𝐵))
113	106, 112	eleqtrrd 2867	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 0 ∈ ((𝑧 ∈ 𝐴 ↦ ((𝐹‘𝑧) − (𝐹‘𝐵))) lim_ℂ 𝐵))
114		cncfmptc 25277	. . . . . . . . 9 ⊢ (((𝐹‘𝐵) ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑧 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ (𝐴–cn→ℂ))
115	29, 36, 32, 114	syl3anc 1399	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ (𝐴–cn→ℂ))
116		eqidd 2764	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐹‘𝐵) = (𝐹‘𝐵))
117	115, 28, 116	cnmptlimc 26254	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹‘𝐵) ∈ ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝐵)) lim_ℂ 𝐵))
118	3	addcn 25229	. . . . . . . 8 ⊢ + ∈ ((𝐾 ×_t 𝐾) Cn 𝐾)
119		opelxpi 5693	. . . . . . . . 9 ⊢ ((0 ∈ ℂ ∧ (𝐹‘𝐵) ∈ ℂ) → ⟨0, (𝐹‘𝐵)⟩ ∈ (ℂ × ℂ))
120	67, 29, 119	sylancr 599	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ⟨0, (𝐹‘𝐵)⟩ ∈ (ℂ × ℂ))
121	70	cncnpi 23640	. . . . . . . 8 ⊢ (( + ∈ ((𝐾 ×_t 𝐾) Cn 𝐾) ∧ ⟨0, (𝐹‘𝐵)⟩ ∈ (ℂ × ℂ)) → + ∈ (((𝐾 ×_t 𝐾) CnP 𝐾)‘⟨0, (𝐹‘𝐵)⟩))
122	118, 120, 121	sylancr 599	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → + ∈ (((𝐾 ×_t 𝐾) CnP 𝐾)‘⟨0, (𝐹‘𝐵)⟩))
123	31, 30, 32, 32, 3, 35, 113, 117, 122	limccnp2 26256	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (0 + (𝐹‘𝐵)) ∈ ((𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) lim_ℂ 𝐵))
124	29	addlidd 11548	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (0 + (𝐹‘𝐵)) = (𝐹‘𝐵))
125	2, 30	npcand 11710	. . . . . . . . 9 ⊢ ((((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵)) = (𝐹‘𝑧))
126	125	mpteq2dva 5202	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧)))
127	1	feqmptd 6982	. . . . . . . 8 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧)))
128	126, 127	eqtr4d 2801	. . . . . . 7 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) = 𝐹)
129	128	oveq1d 7464	. . . . . 6 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → ((𝑧 ∈ 𝐴 ↦ (((𝐹‘𝑧) − (𝐹‘𝐵)) + (𝐹‘𝐵))) lim_ℂ 𝐵) = (𝐹 lim_ℂ 𝐵))
130	123, 124, 129	3eltr3d 2878	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵))
131		dvcnp.j	. . . . . . 7 ⊢ 𝐽 = (𝐾 ↾_t 𝐴)
132	3, 131	cnplimc 26251	. . . . . 6 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵))))
133	36, 28, 132	syl2anc 596	. . . . 5 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵))))
134	1, 130, 133	mpbir2and 726	. . . 4 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵(𝑆 D 𝐹)𝑦) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
135	134	ex 418	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → (𝐵(𝑆 D 𝐹)𝑦 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)))
136	135	exlimdv 1968	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) → (∃𝑦 𝐵(𝑆 D 𝐹)𝑦 → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)))
137		eldmg 5890	. . 3 ⊢ (𝐵 ∈ dom (𝑆 D 𝐹) → (𝐵 ∈ dom (𝑆 D 𝐹) ↔ ∃𝑦 𝐵(𝑆 D 𝐹)𝑦))
138	137	ibi 270	. 2 ⊢ (𝐵 ∈ dom (𝑆 D 𝐹) → ∃𝑦 𝐵(𝑆 D 𝐹)𝑦)
139	136, 138	impel 515	1 ⊢ (((𝑆 ⊆ ℂ ∧ 𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆) ∧ 𝐵 ∈ dom (𝑆 D 𝐹)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ≠ wne 2959 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 {csn 4588 ⟨cop 4838 ∪ cuni 4870 class class class wbr 5106 {copab 5171 ↦ cmpt 5190 × cxp 5654 dom cdm 5656 ↾ cres 5658 ⟶wf 6560 ‘cfv 6564 (class class class)co 7449 ∈ cmpo 7451 ℂcc 11235 0cc0 11237 + caddc 11240 · cmul 11242 − cmin 11578 / cdiv 12011 ↾_t crest 17632 TopOpenctopn 17633 ℂ_fldccnfld 21720 Topctop 23255 TopOnctopon 23272 intcnt 23379 Cn ccn 23586 CnP ccnp 23587 ×_t ctx 23923 –cn→ccncf 25241 lim_ℂ climc 26226 D cdv 26227

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314 ax-pre-sup 11315 ax-addf 11316

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-of 7723 df-om 7910 df-1st 8033 df-2nd 8034 df-supp 8213 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-er 8753 df-map 8885 df-pm 8886 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-fsupp 9390 df-fi 9438 df-sup 9469 df-inf 9470 df-oi 9539 df-card 10055 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-div 12012 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-7 12448 df-8 12449 df-9 12450 df-n0 12645 df-z 12732 df-dec 12853 df-uz 13004 df-q 13114 df-rp 13159 df-xneg 13279 df-xadd 13280 df-xmul 13281 df-icc 13521 df-fz 13678 df-fzo 13827 df-seq 14183 df-exp 14243 df-hash 14514 df-cj 15307 df-re 15308 df-im 15309 df-sqrt 15443 df-abs 15444 df-struct 17366 df-sets 17383 df-slot 17401 df-ndx 17413 df-base 17429 df-ress 17450 df-plusg 17482 df-mulr 17483 df-starv 17484 df-sca 17485 df-vsca 17486 df-ip 17487 df-tset 17488 df-ple 17489 df-ds 17491 df-unif 17492 df-hom 17493 df-cco 17494 df-rest 17634 df-topn 17635 df-0g 17653 df-gsum 17654 df-topgen 17655 df-pt 17656 df-prds 17659 df-xrs 17715 df-qtop 17720 df-imas 17721 df-xps 17723 df-mre 17797 df-mrc 17798 df-acs 17800 df-mgm 18857 df-sgrp 18949 df-mnd 18965 df-submnd 19020 df-mulg 19319 df-cntz 19573 df-cmn 20038 df-psmet 21712 df-xmet 21713 df-met 21714 df-bl 21715 df-mopn 21716 df-cnfld 21721 df-top 23256 df-topon 23273 df-topsp 23295 df-bases 23308 df-ntr 23382 df-cn 23589 df-cnp 23590 df-tx 23925 df-hmeo 24118 df-xms 24683 df-ms 24684 df-tms 24685 df-cncf 25243 df-limc 26230 df-dv 26231

This theorem is used by: dvcn 26285 dvmulbr 26303 dvcobr 26310 fouriersw 47508

W3C validator