P. 214 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21301-21400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reperflem 21301*	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 21302	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 21303	The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Perf
Theorem	iccntr 21304	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 21305*	Lemma for icccmp 21308. (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 21306*	Lemma for icccmp 21308. (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 21307*	Lemma for icccmp 21308. (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 21308	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 21309	Lemma for reconn 21311. 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 21310*	Lemma for reconn 21311. (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 21311*	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 21312	Corollary of reconn 21311. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.)
|- ( topGen ` ran (,) ) e. Con
Theorem	iccconn 21313	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 21314	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 21315	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 21316	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 21317*	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 21318	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 21319	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 21320	The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 21321 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 21321	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 21322	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 21323	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 21324	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 21325*	Continuity of the metric function; analogue of cnmpt12f 20145 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 21326*	Continuity of the metric function; analogue of cnmpt22f 20154 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 21327	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 21328	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 21329*	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 21330*	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 21331*	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 21332*	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 21333*	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 21334*	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 21335*	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 21336*	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 21337*	Lemma for metdscn 21338. (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 21338*	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 21339*	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 21340*	Lemma for metnrm 21344. (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 21341*	Lemma for metnrm 21344. (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 21342*	Lemma for metnrm 21344. (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 21343*	Lemma for metnrm 21344. (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 21344	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 21345	A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. Reg )
Theorem	addcnlem 21346*	Lemma for addcn 21347, subcn 21348, and mulcn 21349. (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 21347	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 21348	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 21349	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 21350	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 21351	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 21352*	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 21353*	Version of fsumcn 21352 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 21354*	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 21355*	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 21356*	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 21357	Extend class notation with the unit interval.
class II
Syntax	ccncf 21358	Extend class notation to include the operation which returns a class of continuous complex functions.
class -cn->
Definition	df-ii 21359	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 21360*	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 21361	The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- II e. (TopOn ` ( 0 [,] 1 ) )
Theorem	iitop 21362	The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- II e. Top
Theorem	iiuni 21363	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 21364	Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
Theorem	dfii3 21365	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 21366	Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- I = (ℂfld ↾s ( 0 [,] 1 ) )   =>    |- II = ( TopOpen ` I )
Theorem	dfii5 21367	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 21368	The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.)
|- II e. Comp
Theorem	iicon 21369	The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- II e. Con
Theorem	cncfval 21370*	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 21371*	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 21372*	Version of elcncf 21371 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 21373	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> A C_ CC )
Theorem	cncfrss2 21374	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> B C_ CC )
Theorem	cncff 21375	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 21376*	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 21377*	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 21378*	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 21379	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 21380	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 21381	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 21382	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 21383	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 21384	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 21385	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 21386	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )
Theorem	mulc1cncf 21387*	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	divccncf 21388*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
|- F = ( x e. CC |-> ( x / A ) )   =>    |- ( ( A e. CC /\ A =/= 0 ) -> F e. ( CC -cn-> CC ) )
Theorem	cncfco 21389	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 21390	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	cncfcn 21391	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t A )   &    |- L = ( J ↾t B )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( K Cn L ) )
Theorem	cncfcn1 21392	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 21393*	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 21394*	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 21395*	Composition of continuous functions. -cn-> analog of cnmpt11f 20143. (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	cncfmpt2f 21396*	Composition of continuous functions. -cn-> analog of cnmpt12f 20145. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- ( 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	cncfmpt2ss 21397*	Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.)
|- J = ( TopOpen ` ℂfld )   &    |- F e. ( ( J tX J ) Cn J )   &    |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> S ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> S ) )   &    |- S C_ CC   &    |- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )   =>    |- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) )
Theorem	addccncf 21398*	Adding 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	cdivcncf 21399*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- F = ( x e. ( CC \ { 0 } ) |-> ( A / x ) )   =>    |- ( A e. CC -> F e. ( ( CC \ { 0 } ) -cn-> CC ) )
Theorem	negcncf 21400*	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 ) )