P. 156 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15501-15600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	metrest 15501	Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
|- D = ( C |` ( Y X. Y ) )   &    |- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( J ↾t Y ) = K )
Theorem	xmetxp 15502*	The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   =>    |- ( ph -> P e. ( *Met ` ( X X. Y ) ) )
Theorem	xmetxpbl 15503*	The maximum metric (Chebyshev distance) on the product of two sets, expressed in terms of balls centered on a point C with radius R. (Contributed by Jim Kingdon, 22-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> R e. RR* )   &    |- ( ph -> C e. ( X X. Y ) )   =>    |- ( ph -> ( C ( ball ` P ) R ) = ( ( ( 1st ` C ) ( ball ` M ) R ) X. ( ( 2nd ` C ) ( ball ` N ) R ) ) )
Theorem	xmettxlem 15504*	Lemma for xmettx 15505. (Contributed by Jim Kingdon, 15-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L C_ ( J tX K ) )
Theorem	xmettx 15505*	The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L = ( J tX K ) )
9.2.5  Continuity in metric spaces
Theorem	metcnp3 15506*	Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) )
Theorem	metcnp 15507*	Two ways to say a mapping from metric C to metric D is continuous at point P. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnp2 15508*	Two ways to say a mapping from metric C to metric D is continuous at point P. The distance arguments are swapped compared to metcnp 15507 (and Munkres' metcn 15509) for compatibility with df-lm 15185. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) ) )
Theorem	metcn 15509*	Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnpi 15510*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 15507. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) )
Theorem	metcnpi2 15511*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 15508. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) < x -> ( ( F ` y ) D ( F ` P ) ) < A ) )
Theorem	metcnpi3 15512*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 15511 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
Theorem	txmetcnp 15513*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) ) )
Theorem	txmetcn 15514*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
Theorem	metcnpd 15515*	Two ways to say a mapping from metric C to metric D is continuous at point P. (Contributed by Jim Kingdon, 14-Jun-2023.)
|- ( ph -> J = ( MetOpen ` C ) )   &    |- ( ph -> K = ( MetOpen ` D ) )   &    |- ( ph -> C e. ( *Met ` X ) )   &    |- ( ph -> D e. ( *Met ` Y ) )   &    |- ( ph -> P e. X )   =>    |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) )
9.2.6  Topology on the reals
Theorem	qtopbasss 15516*	The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Jim Kingdon, 22-May-2023.)
|- S C_ RR*   &    |- ( ( x e. S /\ y e. S ) -> sup ( { x , y } , RR* , < ) e. S )   &    |- ( ( x e. S /\ y e. S ) -> inf ( { x , y } , RR* , < ) e. S )   =>    |- ( (,) " ( S X. S ) ) e. TopBases
Theorem	qtopbas 15517	The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)
|- ( (,) " ( QQ X. QQ ) ) e. TopBases
Theorem	retopbas 15518	A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
|- ran (,) e. TopBases
Theorem	retop 15519	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- ( topGen ` ran (,) ) e. Top
Theorem	uniretop 15520	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
|- RR = U. ( topGen ` ran (,) )
Theorem	retopon 15521	The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( topGen ` ran (,) ) e. (TopOn ` RR )
Theorem	retps 15522	The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
|- K = { <. ( Base ` ndx ) , RR >. , <. (TopSet ` ndx ) , ( topGen ` ran (,) ) >. }   =>    |- K e. TopSp
Theorem	iooretopg 15523	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) e. ( topGen ` ran (,) ) )
Theorem	cnmetdval 15524	Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- D = ( abs o. - )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A D B ) = ( abs ` ( A - B ) ) )
Theorem	cnmet 15525	The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.)
|- ( abs o. - ) e. ( Met ` CC )
Theorem	cnxmet 15526	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( abs o. - ) e. ( *Met ` CC )
Theorem	cntoptopon 15527	The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- J e. (TopOn ` CC )
Theorem	cntoptop 15528	The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- J e. Top
Theorem	cnbl0 15529	Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- D = ( abs o. - )   =>    |- ( R e. RR* -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` D ) R ) )
Theorem	cnblcld 15530*	Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- D = ( abs o. - )   =>    |- ( R e. RR* -> ( `' abs " ( 0 [,] R ) ) = { x e. CC | ( 0 D x ) <_ R } )
Theorem	cnfldms 15531	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. MetSp
Theorem	cnfldxms 15532	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. *MetSp
Theorem	cnfldtps 15533	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. TopSp
Theorem	cnfldtopn 15534	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J = ( MetOpen ` ( abs o. - ) )
Theorem	cnfldtopon 15535	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. (TopOn ` CC )
Theorem	cnfldtop 15536	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Top
Theorem	unicntopcntop 15537	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
|- CC = U. ( MetOpen ` ( abs o. - ) )
Theorem	unicntop 15538	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC = U. ( TopOpen ` ℂfld )
Theorem	cnopncntop 15539	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
|- CC e. ( MetOpen ` ( abs o. - ) )
Theorem	cnopn 15540	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC e. ( TopOpen ` ℂfld )
Theorem	reopnap 15541*	The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.)
|- ( A e. RR -> { w e. RR | w # A } e. ( topGen ` ran (,) ) )
Theorem	remetdval 15542	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )
Theorem	remet 15543	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- D e. ( Met ` RR )
Theorem	rexmet 15544	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- D e. ( *Met ` RR )
Theorem	bl2ioo 15545	A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A ( ball ` D ) B ) = ( ( A - B ) (,) ( A + B ) ) )
Theorem	ioo2bl 15546	An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) = ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) )
Theorem	ioo2blex 15547	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) e. ran ( ball ` D ) )
Theorem	blssioo 15548	The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ran ( ball ` D ) C_ ran (,)
Theorem	tgioo 15549	The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- J = ( MetOpen ` D )   =>    |- ( topGen ` ran (,) ) = J
Theorem	tgqioo 15550	The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.)
|- Q = ( topGen ` ( (,) " ( QQ X. QQ ) ) )   =>    |- ( topGen ` ran (,) ) = Q
Theorem	resubmet 15551	The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
|- R = ( topGen ` ran (,) )   &    |- J = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )   =>    |- ( A C_ RR -> J = ( R ↾t A ) )
Theorem	tgioo2cntop 15552	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( topGen ` ran (,) ) = ( J ↾t RR )
Theorem	rerestcntop 15553	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- R = ( topGen ` ran (,) )   =>    |- ( A C_ RR -> ( J ↾t A ) = ( R ↾t A ) )
Theorem	tgioo2 15554	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( topGen ` ran (,) ) = ( J ↾t RR )
Theorem	rerest 15555	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- R = ( topGen ` ran (,) )   =>    |- ( A C_ RR -> ( J ↾t A ) = ( R ↾t A ) )
Theorem	addcncntoplem 15556*	Lemma for addcncntop 15557, subcncntop 15558, and mulcncntop 15559. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- .+ : ( CC X. CC ) --> CC   &    |- ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( v - c ) ) < z ) -> ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) < a ) )   =>    |- .+ e. ( ( J tX J ) Cn J )
Theorem	addcncntop 15557	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- + e. ( ( J tX J ) Cn J )
Theorem	subcncntop 15558	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- - e. ( ( J tX J ) Cn J )
Theorem	mulcncntop 15559	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- x. e. ( ( J tX J ) Cn J )
Theorem	divcnap 15560*	Complex number division is a continuous function, when the second argument is apart from zero. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- K = ( J ↾t { x e. CC | x # 0 } )   =>    |- ( y e. CC , z e. { x e. CC | x # 0 } |-> ( y / z ) ) e. ( ( J tX K ) Cn J )
Theorem	mpomulcn 15561*	Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( x e. CC , y e. CC |-> ( x x. y ) ) e. ( ( J tX J ) Cn J )
Theorem	fsumcncntop 15562*	A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )   =>    |- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )
Theorem	fsumcn 15563*	A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- K = ( TopOpen ` ℂfld )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )   =>    |- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )
Theorem	expcn 15564*	The power function on complex numbers, for fixed exponent N, is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) Avoid ax-mulf 8266. (Revised by GG, 16-Mar-2025.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( J Cn J ) )
9.2.7  Topological definitions using the reals
Syntax	ccncf 15565	Extend class notation to include the operation which returns a class of continuous complex functions.
class -cn->
Definition	df-cncf 15566*	Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|- -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )
Theorem	cncfval 15567*	The value of the continuous complex function operation is the set of continuous functions from A to B. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = { f e. ( B ^m A ) | A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) } )
Theorem	elcncf 15568*	Membership in the set of continuous complex functions from A to B. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|- ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) ) )
Theorem	elcncf2 15569*	Version of elcncf 15568 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.)
|- ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) )
Theorem	cncfrss 15570	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> A C_ CC )
Theorem	cncfrss2 15571	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> B C_ CC )
Theorem	cncff 15572	A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> F : A --> B )
Theorem	cncfi 15573*	Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( ( F e. ( A -cn-> B ) /\ C e. A /\ R e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) )
Theorem	elcncf1di 15574*	Membership in the set of continuous complex functions from A to B. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ( ph -> F : A --> B )   &    |- ( ph -> ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ ) )   &    |- ( ph -> ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) )   =>    |- ( ph -> ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) ) )
Theorem	elcncf1ii 15575*	Membership in the set of continuous complex functions from A to B. (Contributed by Paul Chapman, 26-Nov-2007.)
|- F : A --> B   &    |- ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ )   &    |- ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) )
Theorem	rescncf 15576	A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( C C_ A -> ( F e. ( A -cn-> B ) -> ( F |` C ) e. ( C -cn-> B ) ) )
Theorem	cncfcdm 15577	Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( C C_ CC /\ F e. ( A -cn-> B ) ) -> ( F e. ( A -cn-> C ) <-> F : A --> C ) )
Theorem	cncfss 15578	The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)
|- ( ( B C_ C /\ C C_ CC ) -> ( A -cn-> B ) C_ ( A -cn-> C ) )
Theorem	climcncf 15579	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. ( A -cn-> B ) )   &    |- ( ph -> G : Z --> A )   &    |- ( ph -> G ~~> D )   &    |- ( ph -> D e. A )   =>    |- ( ph -> ( F o. G ) ~~> ( F ` D ) )
Theorem	abscncf 15580	Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- abs e. ( CC -cn-> RR )
Theorem	recncf 15581	Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- Re e. ( CC -cn-> RR )
Theorem	imcncf 15582	Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- Im e. ( CC -cn-> RR )
Theorem	cjcncf 15583	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )
Theorem	mulc1cncf 15584*	Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. CC |-> ( A x. x ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	divccncfap 15585*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|- F = ( x e. CC |-> ( x / A ) )   =>    |- ( ( A e. CC /\ A # 0 ) -> F e. ( CC -cn-> CC ) )
Theorem	cncfco 15586	The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( ph -> F e. ( A -cn-> B ) )   &    |- ( ph -> G e. ( B -cn-> C ) )   =>    |- ( ph -> ( G o. F ) e. ( A -cn-> C ) )
Theorem	cncfmet 15587	Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- C = ( ( abs o. - ) |` ( A X. A ) )   &    |- D = ( ( abs o. - ) |` ( B X. B ) )   &    |- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( J Cn K ) )
Theorem	cncfcncntop 15588	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- K = ( J ↾t A )   &    |- L = ( J ↾t B )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( K Cn L ) )
Theorem	cncfcn1cntop 15589	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( CC -cn-> CC ) = ( J Cn J )
Theorem	cncfcn1 15590	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( CC -cn-> CC ) = ( J Cn J )
Theorem	cncfmptc 15591*	A constant function is a continuous function on CC. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> ( x e. S |-> A ) e. ( S -cn-> T ) )
Theorem	cncfmptid 15592*	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.)
|- ( ( S C_ T /\ T C_ CC ) -> ( x e. S |-> x ) e. ( S -cn-> T ) )
Theorem	cncfmpt1f 15593*	Composition of continuous functions. -cn-> analogue of cnmpt11f 15279. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- ( ph -> F e. ( CC -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( X -cn-> CC ) )
Theorem	cncfmpt2fcntop 15594*	Composition of continuous functions. -cn-> analogue of cnmpt12f 15281. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> F e. ( ( J tX J ) Cn J ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) )
Theorem	addccncf 15595*	Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- F = ( x e. CC |-> ( x + A ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	idcncf 15596	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 15592 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> x )   =>    |- F e. ( CC -cn-> CC )
Theorem	sub1cncf 15597*	Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> ( x - A ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	sub2cncf 15598*	Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> ( A - x ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	cdivcncfap 15599*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
|- F = ( x e. { y e. CC | y # 0 } |-> ( A / x ) )   =>    |- ( A e. CC -> F e. ( { y e. CC | y # 0 } -cn-> CC ) )
Theorem	negcncf 15600*	The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- F = ( x e. A |-> -u x )   =>    |- ( A C_ CC -> F e. ( A -cn-> CC ) )