P. 149 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14801-14900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tgqioo 14801	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 14802	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 14803	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 14804	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 14805	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 14806	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 14807*	Lemma for addcncntop 14808, subcncntop 14809, and mulcncntop 14810. (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 14808	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 14809	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 14810	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 14811*	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 14812*	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 14813*	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 14814*	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 14815*	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 8004. (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 14816	Extend class notation to include the operation which returns a class of continuous complex functions.
class -cn->
Definition	df-cncf 14817*	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 14818*	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 14819*	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 14820*	Version of elcncf 14819 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 14821	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> A C_ CC )
Theorem	cncfrss2 14822	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> B C_ CC )
Theorem	cncff 14823	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 14824*	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 14825*	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 14826*	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 14827	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 14828	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 14829	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 14830	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 14831	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 14832	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 14833	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 14834	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )
Theorem	mulc1cncf 14835*	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 14836*	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 14837	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 14838	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 14839	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 14840	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 14841	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 14842*	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 14843*	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 14844*	Composition of continuous functions. -cn-> analogue of cnmpt11f 14530. (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 14845*	Composition of continuous functions. -cn-> analogue of cnmpt12f 14532. (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 14846*	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 14847	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 14843 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 14848*	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 14849*	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 14850*	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 14851*	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 14852*	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 14853*	Lemma for mulcncf 14854. (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 14854*	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 14855*	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 14856*	The canonical bijection from ( RR X. RR ) to CC described in cnref1o 9727 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 14857*	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. - ) ) )
PART 10  BASIC REAL AND COMPLEX ANALYSIS
10.1  Continuity
Theorem	addcncf 14858*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( A + B ) ) e. ( X -cn-> CC ) )
Theorem	subcncf 14859*	The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( A - B ) ) e. ( X -cn-> CC ) )
Theorem	divcncfap 14860*	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> { y e. CC | y # 0 } ) )   =>    |- ( ph -> ( x e. X |-> ( A / B ) ) e. ( X -cn-> CC ) )
Theorem	maxcncf 14861*	The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> RR ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> RR ) )   =>    |- ( ph -> ( x e. X |-> sup ( { A , B } , RR , < ) ) e. ( X -cn-> RR ) )
Theorem	mincncf 14862*	The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> RR ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> RR ) )   =>    |- ( ph -> ( x e. X |-> inf ( { A , B } , RR , < ) ) e. ( X -cn-> RR ) )
10.1.1  Dedekind cuts
Theorem	dedekindeulemuub 14863*	Lemma for dedekindeu 14869. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A e. U )   =>    |- ( ph -> A. z e. L z < A )
Theorem	dedekindeulemub 14864*	Lemma for dedekindeu 14869. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. RR A. y e. L y < x )
Theorem	dedekindeulemloc 14865*	Lemma for dedekindeu 14869. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> A. x e. RR A. y e. RR ( x < y -> ( E. z e. L x < z \/ A. z e. L z < y ) ) )
Theorem	dedekindeulemlub 14866*	Lemma for dedekindeu 14869. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. RR ( A. y e. L -. x < y /\ A. y e. RR ( y < x -> E. z e. L y < z ) ) )
Theorem	dedekindeulemlu 14867*	Lemma for dedekindeu 14869. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. RR ( A. q e. L q < x /\ A. r e. U x < r ) )
Theorem	dedekindeulemeu 14868*	Lemma for dedekindeu 14869. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> ( A. q e. L q < A /\ A. r e. U A < r ) )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A. q e. L q < B /\ A. r e. U B < r ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> F. )
Theorem	dedekindeu 14869*	A Dedekind cut identifies a unique real number. Similar to df-inp 7535 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E! x e. RR ( A. q e. L q < x /\ A. r e. U x < r ) )
Theorem	suplociccreex 14870*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8101 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B < C )   &    |- ( ph -> A C_ ( B [,] C ) )   &    |- ( ph -> E. x x e. A )   &    |- ( ph -> A. x e. ( B [,] C ) A. y e. ( B [,] C ) ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) )   =>    |- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
Theorem	suplociccex 14871*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8101 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B < C )   &    |- ( ph -> A C_ ( B [,] C ) )   &    |- ( ph -> E. x x e. A )   &    |- ( ph -> A. x e. ( B [,] C ) A. y e. ( B [,] C ) ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) )   =>    |- ( ph -> E. x e. ( B [,] C ) ( A. y e. A -. x < y /\ A. y e. ( B [,] C ) ( y < x -> E. z e. A y < z ) ) )
Theorem	dedekindicclemuub 14872*	Lemma for dedekindicc 14879. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> C e. U )   =>    |- ( ph -> A. z e. L z < C )
Theorem	dedekindicclemub 14873*	Lemma for dedekindicc 14879. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. ( A [,] B ) A. y e. L y < x )
Theorem	dedekindicclemloc 14874*	Lemma for dedekindicc 14879. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( E. z e. L x < z \/ A. z e. L z < y ) ) )
Theorem	dedekindicclemlub 14875*	Lemma for dedekindicc 14879. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E. x e. ( A [,] B ) ( A. y e. L -. x < y /\ A. y e. ( A [,] B ) ( y < x -> E. z e. L y < z ) ) )
Theorem	dedekindicclemlu 14876*	Lemma for dedekindicc 14879. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E. x e. ( A [,] B ) ( A. q e. L q < x /\ A. r e. U x < r ) )
Theorem	dedekindicclemeu 14877*	Lemma for dedekindicc 14879. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   &    |- ( ph -> C e. ( A [,] B ) )   &    |- ( ph -> ( A. q e. L q < C /\ A. r e. U C < r ) )   &    |- ( ph -> D e. ( A [,] B ) )   &    |- ( ph -> ( A. q e. L q < D /\ A. r e. U D < r ) )   &    |- ( ph -> C < D )   =>    |- ( ph -> F. )
Theorem	dedekindicclemicc 14878*	Lemma for dedekindicc 14879. Same as dedekindicc 14879, except that we merely show x to be an element of ( A [,] B ). Later we will strengthen that to ( A (,) B ). (Contributed by Jim Kingdon, 5-Jan-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E! x e. ( A [,] B ) ( A. q e. L q < x /\ A. r e. U x < r ) )
Theorem	dedekindicc 14879*	A Dedekind cut identifies a unique real number. Similar to df-inp 7535 except that the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 19-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E! x e. ( A (,) B ) ( A. q e. L q < x /\ A. r e. U x < r ) )
10.1.2  Intermediate value theorem
Theorem	ivthinclemlm 14880*	Lemma for ivthinc 14889. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> E. q e. ( A [,] B ) q e. L )
Theorem	ivthinclemum 14881*	Lemma for ivthinc 14889. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> E. r e. ( A [,] B ) r e. R )
Theorem	ivthinclemlopn 14882*	Lemma for ivthinc 14889. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   &    |- ( ph -> Q e. L )   =>    |- ( ph -> E. r e. L Q < r )
Theorem	ivthinclemlr 14883*	Lemma for ivthinc 14889. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )
Theorem	ivthinclemuopn 14884*	Lemma for ivthinc 14889. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   &    |- ( ph -> S e. R )   =>    |- ( ph -> E. q e. R q < S )
Theorem	ivthinclemur 14885*	Lemma for ivthinc 14889. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> A. r e. ( A [,] B ) ( r e. R <-> E. q e. R q < r ) )
Theorem	ivthinclemdisj 14886*	Lemma for ivthinc 14889. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> ( L i^i R ) = (/) )
Theorem	ivthinclemloc 14887*	Lemma for ivthinc 14889. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. R ) ) )
Theorem	ivthinclemex 14888*	Lemma for ivthinc 14889. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> E! z e. ( A (,) B ) ( A. q e. L q < z /\ A. r e. R z < r ) )
Theorem	ivthinc 14889*	The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   =>    |- ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )
Theorem	ivthdec 14890*	The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` B ) < U /\ U < ( F ` A ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` y ) < ( F ` x ) )   =>    |- ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )
Theorem	ivthreinc 14891*	Restating the intermediate value theorem. Given a hypothesis stating the intermediate value theorem (in a strong form which is not provable given our axioms alone), provide a conclusion similar to the theorem as stated in the Metamath Proof Explorer (which is also similar to how we state the theorem for a strictly monotonic function at ivthinc 14889). Being able to have a hypothesis stating the intermediate value theorem will be helpful when it comes time to show that it implies a constructive taboo. This version of the theorem requires that the function F is continuous on the entire real line, not just ( A [,] B ) which may be an unnecessary condition but which is sufficient for the way we want to use it. (Contributed by Jim Kingdon, 7-Jul-2025.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( RR -cn-> RR ) )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ph -> A. f ( f e. ( RR -cn-> RR ) -> A. a e. RR A. b e. RR ( ( a < b /\ ( f ` a ) < 0 /\ 0 < ( f ` b ) ) -> E. x e. RR ( a < x /\ x < b /\ ( f ` x ) = 0 ) ) ) )   =>    |- ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )
Theorem	hovercncf 14892	The hover function is continuous. By hover function, we mean a a function which starts out as a line of slope one, is constant at zero from zero to one, and then resumes as a slope of one. (Contributed by Jim Kingdon, 20-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- F e. ( RR -cn-> RR )
Theorem	hovera 14893*	A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( Z e. RR -> ( F ` ( Z - 1 ) ) < Z )
Theorem	hoverb 14894*	A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( Z e. RR -> Z < ( F ` ( Z + 2 ) ) )
Theorem	hoverlt1 14895*	The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( ( C e. RR /\ C < 1 ) -> ( F ` C ) <_ 0 )
Theorem	hovergt0 14896*	The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( ( C e. RR /\ 0 < C ) -> 0 <_ ( F ` C ) )
Theorem	ivthdichlem 14897*	Lemma for ivthdich 14899. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   &    |- ( ph -> Z e. RR )   &    |- ( ph -> A. f ( f e. ( RR -cn-> RR ) -> A. a e. RR A. b e. RR ( ( a < b /\ ( f ` a ) < 0 /\ 0 < ( f ` b ) ) -> E. x e. RR ( a < x /\ x < b /\ ( f ` x ) = 0 ) ) ) )   =>    |- ( ph -> ( Z <_ 0 \/ 0 <_ Z ) )
Theorem	dich0 14898*	Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- ( A. z e. RR ( z <_ 0 \/ 0 <_ z ) <-> A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) )
Theorem	ivthdich 14899*	The intermediate value theorem implies real number dichotomy. Because real number dichotomy (also known as analytic LLPO) is a constructive taboo, this means we will be unable to prove the intermediate value theorem as stated here (although versions with additional conditions, such as ivthinc 14889 for strictly monotonic functions, can be proved). The proof is via a function which we call the hover function and which is also described in Section 5.1 of [Bauer], p. 493. Consider any real number z. We want to show that z <_ 0 \/ 0 <_ z. Because of hovercncf 14892, hovera 14893, and hoverb 14894, we are able to apply the intermediate value theorem to get a value c such that the hover function at c equals z. By axltwlin 8096, c < 1 or 0 < c, and that leads to z <_ 0 by hoverlt1 14895 or 0 <_ z by hovergt0 14896. (Contributed by Jim Kingdon and Mario Carneiro, 22-Jul-2025.)
|- ( A. f ( f e. ( RR -cn-> RR ) -> A. a e. RR A. b e. RR ( ( a < b /\ ( f ` a ) < 0 /\ 0 < ( f ` b ) ) -> E. x e. RR ( a < x /\ x < b /\ ( f ` x ) = 0 ) ) ) -> A. r e. RR A. s e. RR ( r <_ s \/ s <_ r ) )
10.2  Derivatives
10.2.1  Real and complex differentiation
10.2.1.1  Derivatives of functions of one complex or real variable
Syntax	climc 14900	The limit operator.
class lim CC