Definition df-limced 14265

Description: Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.)

Assertion

Ref	Expression
df-limced	|- lim CC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y e. CC | ( ( f : dom f --> CC /\ dom f C_ CC ) /\ ( x e. CC /\ A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e ) ) ) } )

Distinct variable group:   e, d, f, x, y, z

Detailed syntax breakdown of Definition df-limced

Step	Hyp	Ref	Expression
1		climc 14263	. 2 class lim CC
2		vf	. . 3 setvar f
3		vx	. . 3 setvar x
4		cc 7812	. . . 4 class CC
5		cpm 6652	. . . 4 class ^pm
6	4, 4, 5	co 5878	. . 3 class ( CC ^pm CC )
7	2	cv 1352	. . . . . . . 8 class f
8	7	cdm 4628	. . . . . . 7 class dom f
9	8, 4, 7	wf 5214	. . . . . 6 wff f : dom f --> CC
10	8, 4	wss 3131	. . . . . 6 wff dom f C_ CC
11	9, 10	wa 104	. . . . 5 wff ( f : dom f --> CC /\ dom f C_ CC )
12	3	cv 1352	. . . . . . 7 class x
13	12, 4	wcel 2148	. . . . . 6 wff x e. CC
14		vz	. . . . . . . . . . . . 13 setvar z
15	14	cv 1352	. . . . . . . . . . . 12 class z
16		cap 8541	. . . . . . . . . . . 12 class #
17	15, 12, 16	wbr 4005	. . . . . . . . . . 11 wff z # x
18		cmin 8131	. . . . . . . . . . . . . 14 class -
19	15, 12, 18	co 5878	. . . . . . . . . . . . 13 class ( z - x )
20		cabs 11009	. . . . . . . . . . . . 13 class abs
21	19, 20	cfv 5218	. . . . . . . . . . . 12 class ( abs ` ( z - x ) )
22		vd	. . . . . . . . . . . . 13 setvar d
23	22	cv 1352	. . . . . . . . . . . 12 class d
24		clt 7995	. . . . . . . . . . . 12 class <
25	21, 23, 24	wbr 4005	. . . . . . . . . . 11 wff ( abs ` ( z - x ) ) < d
26	17, 25	wa 104	. . . . . . . . . 10 wff ( z # x /\ ( abs ` ( z - x ) ) < d )
27	15, 7	cfv 5218	. . . . . . . . . . . . 13 class ( f ` z )
28		vy	. . . . . . . . . . . . . 14 setvar y
29	28	cv 1352	. . . . . . . . . . . . 13 class y
30	27, 29, 18	co 5878	. . . . . . . . . . . 12 class ( ( f ` z ) - y )
31	30, 20	cfv 5218	. . . . . . . . . . 11 class ( abs ` ( ( f ` z ) - y ) )
32		ve	. . . . . . . . . . . 12 setvar e
33	32	cv 1352	. . . . . . . . . . 11 class e
34	31, 33, 24	wbr 4005	. . . . . . . . . 10 wff ( abs ` ( ( f ` z ) - y ) ) < e
35	26, 34	wi 4	. . . . . . . . 9 wff ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e )
36	35, 14, 8	wral 2455	. . . . . . . 8 wff A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e )
37		crp 9656	. . . . . . . 8 class RR+
38	36, 22, 37	wrex 2456	. . . . . . 7 wff E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e )
39	38, 32, 37	wral 2455	. . . . . 6 wff A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e )
40	13, 39	wa 104	. . . . 5 wff ( x e. CC /\ A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e ) )
41	11, 40	wa 104	. . . 4 wff ( ( f : dom f --> CC /\ dom f C_ CC ) /\ ( x e. CC /\ A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e ) ) )
42	41, 28, 4	crab 2459	. . 3 class { y e. CC | ( ( f : dom f --> CC /\ dom f C_ CC ) /\ ( x e. CC /\ A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e ) ) ) }
43	2, 3, 6, 4, 42	cmpo 5880	. 2 class ( f e. ( CC ^pm CC ) , x e. CC |-> { y e. CC | ( ( f : dom f --> CC /\ dom f C_ CC ) /\ ( x e. CC /\ A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e ) ) ) } )
44	1, 43	wceq 1353	1 wff lim CC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y e. CC | ( ( f : dom f --> CC /\ dom f C_ CC ) /\ ( x e. CC /\ A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e ) ) ) } )

This definition is referenced by:  limcrcl  14267  limccl  14268  ellimc3apf  14269