gg-dvcnp2

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

	Ref	Expression
Hypotheses	gg-dvcnp.j	⊢ 𝐽 = ( 𝐾 ↾_t 𝐴 )
	gg-dvcnp.k	⊢ 𝐾 = ( TopOpen ‘ ℂ_fld )
Assertion	gg-dvcnp2	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		gg-dvcnp.j	⊢ 𝐽 = ( 𝐾 ↾_t 𝐴 )
2		gg-dvcnp.k	⊢ 𝐾 = ( TopOpen ‘ ℂ_fld )
3		simpl2	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 : 𝐴 ⟶ ℂ )
4	3	ffvelcdmda	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
5	2	cnfldtop	⊢ 𝐾 ∈ Top
6		simpl1	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑆 ⊆ ℂ )
7		cnex	⊢ ℂ ∈ V
8		ssexg	⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
9	6 7 8	sylancl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑆 ∈ V )
10		resttop	⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐾 ↾_t 𝑆 ) ∈ Top )
11	5 9 10	sylancr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐾 ↾_t 𝑆 ) ∈ Top )
12		simpl3	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐴 ⊆ 𝑆 )
13	2	cnfldtopon	⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
14		resttopon	⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾_t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
15	13 6 14	sylancr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐾 ↾_t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
16		toponuni	⊢ ( ( 𝐾 ↾_t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( 𝐾 ↾_t 𝑆 ) )
17	15 16	syl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑆 = ∪ ( 𝐾 ↾_t 𝑆 ) )
18	12 17	sseqtrd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐴 ⊆ ∪ ( 𝐾 ↾_t 𝑆 ) )
19		eqid	⊢ ∪ ( 𝐾 ↾_t 𝑆 ) = ∪ ( 𝐾 ↾_t 𝑆 )
20	19	ntrss2	⊢ ( ( ( 𝐾 ↾_t 𝑆 ) ∈ Top ∧ 𝐴 ⊆ ∪ ( 𝐾 ↾_t 𝑆 ) ) → ( ( int ‘ ( 𝐾 ↾_t 𝑆 ) ) ‘ 𝐴 ) ⊆ 𝐴 )
21	11 18 20	syl2anc	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( int ‘ ( 𝐾 ↾_t 𝑆 ) ) ‘ 𝐴 ) ⊆ 𝐴 )
22		eqid	⊢ ( 𝐾 ↾_t 𝑆 ) = ( 𝐾 ↾_t 𝑆 )
23		eqid	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) )
24		simp1	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝑆 ⊆ ℂ )
25		simp2	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐹 : 𝐴 ⟶ ℂ )
26		simp3	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐴 ⊆ 𝑆 )
27	22 2 23 24 25 26	eldv	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾_t 𝑆 ) ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) lim_ℂ 𝐵 ) ) ) )
28	27	simprbda	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾_t 𝑆 ) ) ‘ 𝐴 ) )
29	21 28	sseldd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ 𝐴 )
30	3 29	ffvelcdmd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
31	30	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
32	4 31	subcld	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
33		ssidd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ℂ ⊆ ℂ )
34		txtopon	⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐾 ×_t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
35	13 13 34	mp2an	⊢ ( 𝐾 ×_t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
36	35	toponrestid	⊢ ( 𝐾 ×_t 𝐾 ) = ( ( 𝐾 ×_t 𝐾 ) ↾_t ( ℂ × ℂ ) )
37	12 6	sstrd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐴 ⊆ ℂ )
38		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑥 − 𝐵 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑥 − 𝐵 ) ) )
39	22 2 38 24 25 26	eldv	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾_t 𝑆 ) ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑥 − 𝐵 ) ) ) lim_ℂ 𝐵 ) ) ) )
40	39	simprbda	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾_t 𝑆 ) ) ‘ 𝐴 ) )
41	21 40	sseldd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ 𝐴 )
42	3 37 41	dvlem	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ )
43	37	ssdifssd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
44	43	sselda	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ℂ )
45	37 41	sseldd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ℂ )
46	45	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
47	44 46	subcld	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ∈ ℂ )
48	27	simplbda	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) lim_ℂ 𝐵 ) )
49		limcresi	⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) lim_ℂ 𝐵 ) ⊆ ( ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) lim_ℂ 𝐵 )
50		difss	⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
51		resmpt	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) )
52	50 51	ax-mp	⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) )
53	52	oveq1i	⊢ ( ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) lim_ℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) lim_ℂ 𝐵 )
54	49 53	sseqtri	⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) lim_ℂ 𝐵 ) ⊆ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) lim_ℂ 𝐵 )
55	45	subidd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐵 − 𝐵 ) = 0 )
56		ssid	⊢ ℂ ⊆ ℂ
57		cncfmptid	⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ 𝑧 ) ∈ ( 𝐴 –cn→ ℂ ) )
58	37 56 57	sylancl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ 𝑧 ) ∈ ( 𝐴 –cn→ ℂ ) )
59		cncfmptc	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
60	45 37 33 59	syl3anc	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
61	58 60	subcncf	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
62		oveq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 − 𝐵 ) = ( 𝐵 − 𝐵 ) )
63	61 41 62	cnmptlimc	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐵 − 𝐵 ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) lim_ℂ 𝐵 ) )
64	55 63	eqeltrrd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) lim_ℂ 𝐵 ) )
65	54 64	sselid	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) lim_ℂ 𝐵 ) )
66	2	mpomulcn	⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×_t 𝐾 ) Cn 𝐾 )
67	24 25 26	dvcl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ )
68		0cn	⊢ 0 ∈ ℂ
69		opelxpi	⊢ ( ( 𝑦 ∈ ℂ ∧ 0 ∈ ℂ ) → ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) )
70	67 68 69	sylancl	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) )
71	35	toponunii	⊢ ( ℂ × ℂ ) = ∪ ( 𝐾 ×_t 𝐾 )
72	71	cncnpi	⊢ ( ( ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×_t 𝐾 ) Cn 𝐾 ) ∧ ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( 𝐾 ×_t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 𝑦 , 0 ⟩ ) )
73	66 70 72	sylancr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( 𝐾 ×_t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 𝑦 , 0 ⟩ ) )
74	42 47 33 33 2 36 48 65 73	limccnp2	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) lim_ℂ 𝐵 ) )
75		df-mpt	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) }
76	75	oveq1i	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) lim_ℂ 𝐵 ) = ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } lim_ℂ 𝐵 )
77	74 76	eleqtrdi	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) ∈ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } lim_ℂ 𝐵 ) )
78		0cnd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ℂ )
79		ovmul	⊢ ( ( 𝑦 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) = ( 𝑦 · 0 ) )
80	67 78 79	syl2anc	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) = ( 𝑦 · 0 ) )
81	3 37 29	dvlem	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ )
82	37 29	sseldd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ℂ )
83	82	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
84	44 83	subcld	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ∈ ℂ )
85		ovmul	⊢ ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ ∧ ( 𝑧 − 𝐵 ) ∈ ℂ ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) )
86	81 84 85	syl2anc	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) )
87	86	eqeq2d	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ↔ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) )
88	87	pm5.32da	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) ↔ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) ) )
89	88	opabbidv	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) } )
90		df-mpt	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) }
91	89 90	eqtr4di	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) )
92	91	oveq1d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } lim_ℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) lim_ℂ 𝐵 ) )
93	77 80 92	3eltr3d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 · 0 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) lim_ℂ 𝐵 ) )
94	67	mul01d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 · 0 ) = 0 )
95	3	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐹 : 𝐴 ⟶ ℂ )
96		simpr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) )
97	50 96	sselid	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ 𝐴 )
98	95 97	ffvelcdmd	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
99	30	adantr	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
100	98 99	subcld	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
101		eldifsni	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑧 ≠ 𝐵 )
102	101	adantl	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ≠ 𝐵 )
103	44 83 102	subne0d	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ≠ 0 )
104	100 84 103	divcan1d	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) )
105	104	mpteq2dva	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) )
106	105	oveq1d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) lim_ℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) )
107	93 94 106	3eltr3d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) )
108	32	fmpttd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) : 𝐴 ⟶ ℂ )
109	108	limcdif	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) = ( ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) lim_ℂ 𝐵 ) )
110		resmpt	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) )
111	50 110	ax-mp	⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) )
112	111	oveq1i	⊢ ( ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) lim_ℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 )
113	109 112	eqtrdi	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) )
114	107 113	eleqtrrd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) )
115		cncfmptc	⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
116	30 37 33 115	syl3anc	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
117		eqidd	⊢ ( 𝑧 = 𝐵 → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
118	116 29 117	cnmptlimc	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) lim_ℂ 𝐵 ) )
119	2	addcn	⊢ + ∈ ( ( 𝐾 ×_t 𝐾 ) Cn 𝐾 )
120		opelxpi	⊢ ( ( 0 ∈ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℂ ) → ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) )
121	68 30 120	sylancr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) )
122	71	cncnpi	⊢ ( ( + ∈ ( ( 𝐾 ×_t 𝐾 ) Cn 𝐾 ) ∧ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) ) → + ∈ ( ( ( 𝐾 ×_t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ) )
123	119 121 122	sylancr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → + ∈ ( ( ( 𝐾 ×_t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ) )
124	32 31 33 33 2 36 114 118 123	limccnp2	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 0 + ( 𝐹 ‘ 𝐵 ) ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) )
125	30	addlidd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 0 + ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝐵 ) )
126	4 31	npcand	⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝑧 ) )
127	126	mpteq2dva	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
128	3	feqmptd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
129	127 128	eqtr4d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) = 𝐹 )
130	129	oveq1d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) lim_ℂ 𝐵 ) = ( 𝐹 lim_ℂ 𝐵 ) )
131	124 125 130	3eltr3d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 lim_ℂ 𝐵 ) )
132	2 1	cnplimc	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 lim_ℂ 𝐵 ) ) ) )
133	37 29 132	syl2anc	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 lim_ℂ 𝐵 ) ) ) )
134	3 131 133	mpbir2and	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )
135	134	ex	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) 𝑦 → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
136	135	exlimdv	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
137		eldmg	⊢ ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) → ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ↔ ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) )
138	137	ibi	⊢ ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) → ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 )
139	136 138	impel	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem gg-dvcnp2

Proof