P. 217 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21601-21700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rerest 21601	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	tgioo3 21602	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Thierry Arnoux, 3-Jul-2019.)
|- J = ( TopOpen ` RRfld )   =>    |- ( topGen ` ran (,) ) = J
Theorem	xrtgioo 21603	The topology on the extended reals coincides with the standard topology on the reals, when restricted to RR. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- J = ( (ordTop ` <_ ) ↾t RR )   =>    |- ( topGen ` ran (,) ) = J
Theorem	xrrest 21604	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = (ordTop ` <_ )   &    |- R = ( topGen ` ran (,) )   =>    |- ( A C_ RR -> ( X ↾t A ) = ( R ↾t A ) )
Theorem	xrrest2 21605	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- X = (ordTop ` <_ )   =>    |- ( A C_ RR -> ( J ↾t A ) = ( X ↾t A ) )
Theorem	xrsxmet 21606	The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- D = ( dist ` RR*s )   =>    |- D e. ( *Met ` RR* )
Theorem	xrsdsre 21607	The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- D = ( dist ` RR*s )   =>    |- ( D |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
Theorem	xrsblre 21608	Any ball of the metric of the extended reals centered on an element of RR is entirely contained in RR. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- D = ( dist ` RR*s )   =>    |- ( ( P e. RR /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ RR )
Theorem	xrsmopn 21609	The metric on the extended reals generates a topology, but this does not match the order topology on RR*; for example { +oo } is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- D = ( dist ` RR*s )   &    |- J = ( MetOpen ` D )   =>    |- (ordTop ` <_ ) C_ J
Theorem	zcld 21610	The integers are a closed set in the topology on RR. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- J = ( topGen ` ran (,) )   =>    |- ZZ e. ( Clsd ` J )
Theorem	recld2 21611	The real numbers are a closed set in the topology on CC. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- RR e. ( Clsd ` J )
Theorem	zcld2 21612	The integers are a closed set in the topology on CC. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ZZ e. ( Clsd ` J )
Theorem	zdis 21613	The integers are a discrete set in the topology on CC. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( J ↾t ZZ ) = ~P ZZ
Theorem	sszcld 21614	Every subset of the integers are closed in the topology on CC. (Contributed by Mario Carneiro, 6-Jul-2017.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( A C_ ZZ -> A e. ( Clsd ` J ) )
Theorem	reperflem 21615*	A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016.)
|- J = ( TopOpen ` ℂfld )   &    |- ( ( u e. S /\ v e. RR ) -> ( u + v ) e. S )   &    |- S C_ CC   =>    |- ( J ↾t S ) e. Perf
Theorem	reperf 21616	The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( J ↾t RR ) e. Perf
Theorem	cnperf 21617	The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Perf
Theorem	iccntr 21618	The interior of a closed interval in the standard topology on RR is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
Theorem	icccmplem1 21619*	Lemma for icccmp 21622. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- J = ( topGen ` ran (,) )   &    |- T = ( J ↾t ( A [,] B ) )   &    |- D = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> U C_ J )   &    |- ( ph -> ( A [,] B ) C_ U. U )   =>    |- ( ph -> ( A e. S /\ A. y e. S y <_ B ) )
Theorem	icccmplem2 21620*	Lemma for icccmp 21622. (Contributed by Mario Carneiro, 13-Jun-2014.)
|- J = ( topGen ` ran (,) )   &    |- T = ( J ↾t ( A [,] B ) )   &    |- D = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> U C_ J )   &    |- ( ph -> ( A [,] B ) C_ U. U )   &    |- ( ph -> V e. U )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> ( G ( ball ` D ) C ) C_ V )   &    |- G = sup ( S , RR , < )   &    |- R = if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B )   =>    |- ( ph -> B e. S )
Theorem	icccmplem3 21621*	Lemma for icccmp 21622. (Contributed by Mario Carneiro, 13-Jun-2014.)
|- J = ( topGen ` ran (,) )   &    |- T = ( J ↾t ( A [,] B ) )   &    |- D = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> U C_ J )   &    |- ( ph -> ( A [,] B ) C_ U. U )   =>    |- ( ph -> B e. S )
Theorem	icccmp 21622	A closed interval in RR is compact. (Contributed by Mario Carneiro, 13-Jun-2014.)
|- J = ( topGen ` ran (,) )   &    |- T = ( J ↾t ( A [,] B ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> T e. Comp )
Theorem	reconnlem1 21623	Lemma for reconn 21625. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
|- ( ( ( A C_ RR /\ ( ( topGen ` ran (,) ) ↾t A ) e. Con ) /\ ( X e. A /\ Y e. A ) ) -> ( X [,] Y ) C_ A )
Theorem	reconnlem2 21624*	Lemma for reconn 21625. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
|- ( ph -> A C_ RR )   &    |- ( ph -> U e. ( topGen ` ran (,) ) )   &    |- ( ph -> V e. ( topGen ` ran (,) ) )   &    |- ( ph -> A. x e. A A. y e. A ( x [,] y ) C_ A )   &    |- ( ph -> B e. ( U i^i A ) )   &    |- ( ph -> C e. ( V i^i A ) )   &    |- ( ph -> ( U i^i V ) C_ ( RR \ A ) )   &    |- ( ph -> B <_ C )   &    |- S = sup ( ( U i^i ( B [,] C ) ) , RR , < )   =>    |- ( ph -> -. A C_ ( U u. V ) )
Theorem	reconn 21625*	A subset of the reals is connected iff it has the interval property. (Contributed by Jeff Hankins, 15-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
|- ( A C_ RR -> ( ( ( topGen ` ran (,) ) ↾t A ) e. Con <-> A. x e. A A. y e. A ( x [,] y ) C_ A ) )
Theorem	retopcon 21626	Corollary of reconn 21625. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
|- ( topGen ` ran (,) ) e. Con
Theorem	iccconn 21627	A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) e. Con )
Theorem	opnreen 21628	Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.)
|- ( ( A e. ( topGen ` ran (,) ) /\ A =/= (/) ) -> A ~~ ~P NN )
Theorem	rectbntr0 21629	A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ( A C_ RR /\ A ~<_ NN ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = (/) )
Theorem	xrge0gsumle 21630	A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> ( 0 [,] +oo ) )   &    |- ( ph -> B e. ( ~P A i^i Fin ) )   &    |- ( ph -> C C_ B )   =>    |- ( ph -> ( G gsumg ( F |` C ) ) <_ ( G gsumg ( F |` B ) ) )
Theorem	xrge0tsms 21631*	Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Proof shortened by AV, 26-Jul-2019.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> ( 0 [,] +oo ) )   &    |- S = sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsumg ( F |` s ) ) ) , RR* , < )   =>    |- ( ph -> ( G tsums F ) = { S } )
Theorem	xrge0tsms2 21632	Any finite or infinite sum in the nonnegative extended reals is convergent. This is a rather unique property of the set [ 0 , +oo ]; a similar theorem is not true for RR* or RR or [ 0 , +oo ). It is true for NN0 u. { +oo }, however, or more generally any additive submonoid of [ 0 , +oo ) with +oo adjoined. (Contributed by Mario Carneiro, 13-Sep-2015.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   =>    |- ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> ( G tsums F ) ~~ 1o )
Theorem	metdcnlem 21633	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- J = ( MetOpen ` D )   &    |- C = ( dist ` RR*s )   &    |- K = ( MetOpen ` C )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> Y e. X )   &    |- ( ph -> Z e. X )   &    |- ( ph -> ( A D Y ) < ( R / 2 ) )   &    |- ( ph -> ( B D Z ) < ( R / 2 ) )   =>    |- ( ph -> ( ( A D B ) C ( Y D Z ) ) < R )
Theorem	xmetdcn2 21634	The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 21635 we use the metric topology instead of the order topology on RR*, which makes the theorem a bit stronger. Since +oo is an isolated point in the metric topology, this is saying that for any points A , B which are an infinite distance apart, there is a product neighborhood around <. A , B >. such that d ( a , b ) = +oo for any a near A and b near B, i.e. the distance function is locally constant +oo. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- J = ( MetOpen ` D )   &    |- C = ( dist ` RR*s )   &    |- K = ( MetOpen ` C )   =>    |- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) )
Theorem	xmetdcn 21635	The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- J = ( MetOpen ` D )   &    |- K = (ordTop ` <_ )   =>    |- ( D e. ( *Met ` X ) -> D e. ( ( J tX J ) Cn K ) )
Theorem	metdcn2 21636	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- J = ( MetOpen ` D )   &    |- K = ( topGen ` ran (,) )   =>    |- ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn K ) )
Theorem	metdcn 21637	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- J = ( MetOpen ` D )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( D e. ( Met ` X ) -> D e. ( ( J tX J ) Cn K ) )
Theorem	msdcn 21638	The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   &    |- J = ( TopOpen ` M )   &    |- K = ( topGen ` ran (,) )   =>    |- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( ( J tX J ) Cn K ) )
Theorem	cnmpt1ds 21639*	Continuity of the metric function; analogue of cnmpt12f 20459 which cannot be used directly because D is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- D = ( dist ` G )   &    |- J = ( TopOpen ` G )   &    |- R = ( topGen ` ran (,) )   &    |- ( ph -> G e. MetSp )   &    |- ( ph -> K e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )   =>    |- ( ph -> ( x e. X |-> ( A D B ) ) e. ( K Cn R ) )
Theorem	cnmpt2ds 21640*	Continuity of the metric function; analogue of cnmpt22f 20468 which cannot be used directly because D is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- D = ( dist ` G )   &    |- J = ( TopOpen ` G )   &    |- R = ( topGen ` ran (,) )   &    |- ( ph -> G e. MetSp )   &    |- ( ph -> K e. (TopOn ` X ) )   &    |- ( ph -> L e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> ( A D B ) ) e. ( ( K tX L ) Cn R ) )
Theorem	nmcn 21641	The norm of a normed group is a continuous function. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- N = ( norm ` G )   &    |- J = ( TopOpen ` G )   &    |- K = ( topGen ` ran (,) )   =>    |- ( G e. NrmGrp -> N e. ( J Cn K ) )
Theorem	abscn 21642	The absolute value function on complex numbers is continuous. (Contributed by NM, 22-Aug-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( topGen ` ran (,) )   =>    |- abs e. ( J Cn K )
Theorem	metdsval 21643*	Value of the "distance to a set" function. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   =>    |- ( A e. X -> ( F ` A ) = sup ( ran ( y e. S |-> ( A D y ) ) , RR* , `' < ) )
Theorem	metdsf 21644*	The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   =>    |- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
Theorem	metdsge 21645*	The distance from the point A to the set S is greater than R iff the R-ball around A misses S. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   =>    |- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ R e. RR* ) -> ( R <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) R ) ) = (/) ) )
Theorem	metds0 21646*	If a point is in a set, its distance to the set is zero. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   =>    |- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) = 0 )
Theorem	metdstri 21647*	A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol d denotes the point-point and point-set distance functions, this theorem would be written d ( a , S ) <_ d ( a , b ) + d ( b , S ). (Contributed by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   =>    |- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) )
Theorem	metdsle 21648*	The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   =>    |- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( F ` B ) <_ ( A D B ) )
Theorem	metdsre 21649*	The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   =>    |- ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F : X --> RR )
Theorem	metdseq0 21650*	The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) -> ( ( F ` A ) = 0 <-> A e. ( ( cls ` J ) ` S ) ) )
Theorem	metdscnlem 21651*	Lemma for metdscn 21652. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   &    |- C = ( dist ` RR*s )   &    |- K = ( MetOpen ` C )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> S C_ X )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> ( A D B ) < R )   =>    |- ( ph -> ( ( F ` A ) +e -e ( F ` B ) ) < R )
Theorem	metdscn 21652*	The function F which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   &    |- C = ( dist ` RR*s )   &    |- K = ( MetOpen ` C )   =>    |- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F e. ( J Cn K ) )
Theorem	metdscn2 21653*	The function F which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ( D e. ( Met ` X ) /\ S C_ X /\ S =/= (/) ) -> F e. ( J Cn K ) )
Theorem	metnrmlem1a 21654*	Lemma for metnrm 21658. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> S e. ( Clsd ` J ) )   &    |- ( ph -> T e. ( Clsd ` J ) )   &    |- ( ph -> ( S i^i T ) = (/) )   =>    |- ( ( ph /\ A e. T ) -> ( 0 < ( F ` A ) /\ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR+ ) )
Theorem	metnrmlem1 21655*	Lemma for metnrm 21658. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> S e. ( Clsd ` J ) )   &    |- ( ph -> T e. ( Clsd ` J ) )   &    |- ( ph -> ( S i^i T ) = (/) )   =>    |- ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( A D B ) )
Theorem	metnrmlem2 21656*	Lemma for metnrm 21658. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> S e. ( Clsd ` J ) )   &    |- ( ph -> T e. ( Clsd ` J ) )   &    |- ( ph -> ( S i^i T ) = (/) )   &    |- U = U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) )   =>    |- ( ph -> ( U e. J /\ T C_ U ) )
Theorem	metnrmlem3 21657*	Lemma for metnrm 21658. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- F = ( x e. X |-> sup ( ran ( y e. S |-> ( x D y ) ) , RR* , `' < ) )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> S e. ( Clsd ` J ) )   &    |- ( ph -> T e. ( Clsd ` J ) )   &    |- ( ph -> ( S i^i T ) = (/) )   &    |- U = U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) )   &    |- G = ( x e. X |-> sup ( ran ( y e. T |-> ( x D y ) ) , RR* , `' < ) )   &    |- V = U_ s e. S ( s ( ball ` D ) ( if ( 1 <_ ( G ` s ) , 1 , ( G ` s ) ) / 2 ) )   =>    |- ( ph -> E. z e. J E. w e. J ( S C_ z /\ T C_ w /\ ( z i^i w ) = (/) ) )
Theorem	metnrm 21658	A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. Nrm )
Theorem	metreg 21659	A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. Reg )
Theorem	addcnlem 21660*	Lemma for addcn 21661, subcn 21662, and mulcn 21663. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- .+ : ( 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	addcn 21661	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 = ( TopOpen ` ℂfld )   =>    |- + e. ( ( J tX J ) Cn J )
Theorem	subcn 21662	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 = ( TopOpen ` ℂfld )   =>    |- - e. ( ( J tX J ) Cn J )
Theorem	mulcn 21663	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 = ( TopOpen ` ℂfld )   =>    |- x. e. ( ( J tX J ) Cn J )
Theorem	divcn 21664	Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t ( CC \ { 0 } ) )   =>    |- / e. ( ( J tX K ) Cn J )
Theorem	cnfldtgp 21665	The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ℂfld e. TopGrp
Theorem	fsumcn 21666*	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	fsum2cn 21667*	Version of fsumcn 21666 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.)
|- K = ( TopOpen ` ℂfld )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> L e. (TopOn ` Y ) )   &    |- ( ( ph /\ k e. A ) -> ( x e. X , y e. Y |-> B ) e. ( ( J tX L ) Cn K ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> sum_ k e. A B ) e. ( ( J tX L ) Cn K ) )
Theorem	expcn 21668*	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.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( J Cn J ) )
Theorem	divccn 21669*	Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x / A ) ) e. ( J Cn J ) )
Theorem	sqcn 21670*	The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( x e. CC |-> ( x ^ 2 ) ) e. ( J Cn J )
12.4.11  Topological definitions using the reals
Syntax	cii 21671	Extend class notation with the unit interval.
class II
Syntax	ccncf 21672	Extend class notation to include the operation which returns a class of continuous complex functions.
class -cn->
Definition	df-ii 21673	Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
Definition	df-cncf 21674*	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	iitopon 21675	The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- II e. (TopOn ` ( 0 [,] 1 ) )
Theorem	iitop 21676	The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- II e. Top
Theorem	iiuni 21677	The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Jan-2014.)
|- ( 0 [,] 1 ) = U. II
Theorem	dfii2 21678	Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
Theorem	dfii3 21679	Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- II = ( J ↾t ( 0 [,] 1 ) )
Theorem	dfii4 21680	Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- I = (ℂfld ↾s ( 0 [,] 1 ) )   =>    |- II = ( TopOpen ` I )
Theorem	dfii5 21681	The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- II = (ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
Theorem	iicmp 21682	The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.)
|- II e. Comp
Theorem	iicon 21683	The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- II e. Con
Theorem	cncfval 21684*	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 21685*	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 21686*	Version of elcncf 21685 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 21687	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> A C_ CC )
Theorem	cncfrss2 21688	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> B C_ CC )
Theorem	cncff 21689	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 21690*	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 21691*	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 21692*	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 21693	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	cncffvrn 21694	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 21695	The set of continuous functions is expanded when the range is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)
|- ( ( B C_ C /\ C C_ CC ) -> ( A -cn-> B ) C_ ( A -cn-> C ) )
Theorem	climcncf 21696	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 21697	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 21698	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 21699	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 21700	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )