P. 153 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15201-15300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	metcnp 15201*	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 15202*	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 15201 (and Munkres' metcn 15203) for compatibility with df-lm 14879. 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 15203*	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 15204*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 15201. (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 15205*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 15202. (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 15206*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 15205 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 15207*	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 15208*	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 15209*	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 15210*	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 15211	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 15212	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 15213	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- ( topGen ` ran (,) ) e. Top
Theorem	uniretop 15214	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 15215	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 15216	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 15217	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 15218	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 15219	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 15220	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( abs o. - ) e. ( *Met ` CC )
Theorem	cntoptopon 15221	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 15222	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 15223	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 15224*	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 15225	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. MetSp
Theorem	cnfldxms 15226	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. *MetSp
Theorem	cnfldtps 15227	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. TopSp
Theorem	cnfldtopn 15228	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J = ( MetOpen ` ( abs o. - ) )
Theorem	cnfldtopon 15229	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 15230	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Top
Theorem	unicntopcntop 15231	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 15232	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 15233	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 15234	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 15235*	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 15236	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 15237	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 15238	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 15239	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 15240	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 15241	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 15242	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 15243	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 15244	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 15245	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 15246	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 15247	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 15248	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 15249	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 15250*	Lemma for addcncntop 15251, subcncntop 15252, and mulcncntop 15253. (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 15251	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 15252	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 15253	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 15254*	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 15255*	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 15256*	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 15257*	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 15258*	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 8133. (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 15259	Extend class notation to include the operation which returns a class of continuous complex functions.
class -cn->
Definition	df-cncf 15260*	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 15261*	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 15262*	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 15263*	Version of elcncf 15262 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 15264	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> A C_ CC )
Theorem	cncfrss2 15265	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> B C_ CC )
Theorem	cncff 15266	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 15267*	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 15268*	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 15269*	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 15270	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 15271	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 15272	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 15273	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 15274	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 15275	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 15276	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 15277	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )
Theorem	mulc1cncf 15278*	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 15279*	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 15280	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 15281	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 15282	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 15283	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 15284	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 15285*	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 15286*	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 15287*	Composition of continuous functions. -cn-> analogue of cnmpt11f 14973. (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 15288*	Composition of continuous functions. -cn-> analogue of cnmpt12f 14975. (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 15289*	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 15290	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 15286 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 15291*	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 15292*	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 15293*	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 15294*	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 ) )
Theorem	negfcncf 15295*	The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- G = ( x e. A |-> -u ( F ` x ) )   =>    |- ( F e. ( A -cn-> CC ) -> G e. ( A -cn-> CC ) )
Theorem	mulcncflem 15296*	Lemma for mulcncf 15297. (Contributed by Jim Kingdon, 29-May-2023.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   &    |- ( ph -> V e. X )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> F e. RR+ )   &    |- ( ph -> G e. RR+ )   &    |- ( ph -> S e. RR+ )   &    |- ( ph -> T e. RR+ )   &    |- ( ph -> A. u e. X ( ( abs ` ( u - V ) ) < S -> ( abs ` ( ( ( x e. X |-> A ) ` u ) - ( ( x e. X |-> A ) ` V ) ) ) < F ) )   &    |- ( ph -> A. u e. X ( ( abs ` ( u - V ) ) < T -> ( abs ` ( ( ( x e. X |-> B ) ` u ) - ( ( x e. X |-> B ) ` V ) ) ) < G ) )   &    |- ( ph -> A. u e. X ( ( ( abs ` ( [_ u / x ]_ A - [_ V / x ]_ A ) ) < F /\ ( abs ` ( [_ u / x ]_ B - [_ V / x ]_ B ) ) < G ) -> ( abs ` ( ( [_ u / x ]_ A x. [_ u / x ]_ B ) - ( [_ V / x ]_ A x. [_ V / x ]_ B ) ) ) < E ) )   =>    |- ( ph -> E. d e. RR+ A. u e. X ( ( abs ` ( u - V ) ) < d -> ( abs ` ( ( ( x e. X |-> ( A x. B ) ) ` u ) - ( ( x e. X |-> ( A x. B ) ) ` V ) ) ) < E ) )
Theorem	mulcncf 15297*	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( X -cn-> CC ) )
Theorem	expcncf 15298*	The power function on complex numbers, for fixed exponent N, is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
Theorem	cnrehmeocntop 15299*	The canonical bijection from ( RR X. RR ) to CC described in cnref1o 9858 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if ( RR X. RR ) is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.)
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )   &    |- J = ( topGen ` ran (,) )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- F e. ( ( J tX J ) Homeo K )
Theorem	cnopnap 15300*	The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.)
|- ( A e. CC -> { w e. CC | w # A } e. ( MetOpen ` ( abs o. - ) ) )