P. 154 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15301-15400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imcncf 15301	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 15302	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )
Theorem	mulc1cncf 15303*	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 15304*	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 15305	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 15306	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 15307	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 15308	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 15309	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 15310*	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 15311*	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 15312*	Composition of continuous functions. -cn-> analogue of cnmpt11f 14998. (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 15313*	Composition of continuous functions. -cn-> analogue of cnmpt12f 15000. (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 15314*	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 15315	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 15311 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 15316*	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 15317*	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 15318*	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 15319*	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 15320*	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 15321*	Lemma for mulcncf 15322. (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 15322*	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 15323*	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 15324*	The canonical bijection from ( RR X. RR ) to CC described in cnref1o 9875 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 15325*	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 15326*	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 15327*	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 15328*	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 15329*	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 15330*	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 15331*	Lemma for dedekindeu 15337. 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 15332*	Lemma for dedekindeu 15337. 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 15333*	Lemma for dedekindeu 15337. 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 15334*	Lemma for dedekindeu 15337. 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 15335*	Lemma for dedekindeu 15337. 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 15336*	Lemma for dedekindeu 15337. 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 15337*	A Dedekind cut identifies a unique real number. Similar to df-inp 7676 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 15338*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8242 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 15339*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8242 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 15340*	Lemma for dedekindicc 15347. 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 15341*	Lemma for dedekindicc 15347. 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 15342*	Lemma for dedekindicc 15347. 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 15343*	Lemma for dedekindicc 15347. 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 15344*	Lemma for dedekindicc 15347. 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 15345*	Lemma for dedekindicc 15347. 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 15346*	Lemma for dedekindicc 15347. Same as dedekindicc 15347, 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 15347*	A Dedekind cut identifies a unique real number. Similar to df-inp 7676 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 15348*	Lemma for ivthinc 15357. 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 15349*	Lemma for ivthinc 15357. 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 15350*	Lemma for ivthinc 15357. 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 15351*	Lemma for ivthinc 15357. 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 15352*	Lemma for ivthinc 15357. 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 15353*	Lemma for ivthinc 15357. 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 15354*	Lemma for ivthinc 15357. 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 15355*	Lemma for ivthinc 15357. 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 15356*	Lemma for ivthinc 15357. 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 15357*	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 15358*	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 15359*	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 15357). 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 15360	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 15361*	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 15362*	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 15363*	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 15364*	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 15365*	Lemma for ivthdich 15367. 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 15366*	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 15367*	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 15357 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 15360, hovera 15361, and hoverb 15362, 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 8237, c < 1 or 0 < c, and that leads to z <_ 0 by hoverlt1 15363 or 0 <_ z by hovergt0 15364. (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 15368	The limit operator.
class lim CC
Syntax	cdv 15369	The derivative operator.
class _D
Definition	df-limced 15370*	Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.)
|- lim CC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y e. CC | ( ( f : dom f --> CC /\ dom f C_ CC ) /\ ( x e. CC /\ A. e e. RR+ E. d e. RR+ A. z e. dom f ( ( z # x /\ ( abs ` ( z - x ) ) < d ) -> ( abs ` ( ( f ` z ) - y ) ) < e ) ) ) } )
Definition	df-dvap 15371*	Define the derivative operator. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set s here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of CC and is well-behaved when s contains no isolated points, we will restrict our attention to the cases s = RR or s = CC for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )
Theorem	limcrcl 15372	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( C e. ( F lim CC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
Theorem	limccl 15373	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( F lim CC B ) C_ CC
Theorem	ellimc3apf 15374*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- F/_ z F   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z # B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
Theorem	ellimc3ap 15375*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon, 3-Jun-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z # B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
Theorem	limcdifap 15376*	It suffices to consider functions which are not defined at B to define the limit of a function. In particular, the value of the original function F at B does not affect the limit of F. (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   =>    |- ( ph -> ( F lim CC B ) = ( ( F |` { x e. A | x # B } ) lim CC B ) )
Theorem	limcmpted 15377*	Express the limit operator for a function defined by a mapping, via epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ( ph /\ z e. A ) -> D e. CC )   =>    |- ( ph -> ( C e. ( ( z e. A |-> D ) lim CC B ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z # B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( D - C ) ) < x ) ) ) )
Theorem	limcimolemlt 15378*	Lemma for limcimo 15379. (Contributed by Jim Kingdon, 3-Jul-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B e. C )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. ( K ↾t S ) )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> { q e. C | q # B } C_ A )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> X e. ( F lim CC B ) )   &    |- ( ph -> Y e. ( F lim CC B ) )   &    |- ( ph -> A. z e. A ( ( z # B /\ ( abs ` ( z - B ) ) < D ) -> ( abs ` ( ( F ` z ) - X ) ) < ( ( abs ` ( X - Y ) ) / 2 ) ) )   &    |- ( ph -> G e. RR+ )   &    |- ( ph -> A. w e. A ( ( w # B /\ ( abs ` ( w - B ) ) < G ) -> ( abs ` ( ( F ` w ) - Y ) ) < ( ( abs ` ( X - Y ) ) / 2 ) ) )   =>    |- ( ph -> ( abs ` ( X - Y ) ) < ( abs ` ( X - Y ) ) )
Theorem	limcimo 15379*	Conditions which ensure there is at most one limit value of F at B. (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 8-Jul-2023.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B e. C )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. ( K ↾t S ) )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> { q e. C | q # B } C_ A )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> E* x x e. ( F lim CC B ) )
Theorem	limcresi 15380	Any limit of F is also a limit of the restriction of F. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( F lim CC B ) C_ ( ( F |` C ) lim CC B )
Theorem	cnplimcim 15381	If a function is continuous at B, its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( K ↾t A )   =>    |- ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) -> ( F : A --> CC /\ ( F ` B ) e. ( F lim CC B ) ) ) )
Theorem	cnplimclemle 15382	Lemma for cnplimccntop 15384. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( K ↾t A )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> B e. A )   &    |- ( ph -> ( F ` B ) e. ( F lim CC B ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> Z e. A )   &    |- ( ( ph /\ Z # B /\ ( abs ` ( Z - B ) ) < D ) -> ( abs ` ( ( F ` Z ) - ( F ` B ) ) ) < ( E / 2 ) )   &    |- ( ph -> ( abs ` ( Z - B ) ) < D )   =>    |- ( ph -> ( abs ` ( ( F ` Z ) - ( F ` B ) ) ) < E )
Theorem	cnplimclemr 15383	Lemma for cnplimccntop 15384. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( K ↾t A )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> B e. A )   &    |- ( ph -> ( F ` B ) e. ( F lim CC B ) )   =>    |- ( ph -> F e. ( ( J CnP K ) ` B ) )
Theorem	cnplimccntop 15384	A function is continuous at B iff its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( K ↾t A )   =>    |- ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F lim CC B ) ) ) )
Theorem	cnlimcim 15385*	If F is a continuous function, the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.)
|- ( A C_ CC -> ( F e. ( A -cn-> CC ) -> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F lim CC x ) ) ) )
Theorem	cnlimc 15386*	F is a continuous function iff the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( A C_ CC -> ( F e. ( A -cn-> CC ) <-> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F lim CC x ) ) ) )
Theorem	cnlimci 15387	If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F e. ( A -cn-> D ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> ( F ` B ) e. ( F lim CC B ) )
Theorem	cnmptlimc 15388*	If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> ( x e. A |-> X ) e. ( A -cn-> D ) )   &    |- ( ph -> B e. A )   &    |- ( x = B -> X = Y )   =>    |- ( ph -> Y e. ( ( x e. A |-> X ) lim CC B ) )
Theorem	limccnpcntop 15389	If the limit of F at B is C and G is continuous at C, then the limit of G o. F at B is G ( C ). (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 18-Jun-2023.)
|- ( ph -> F : A --> D )   &    |- ( ph -> D C_ CC )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( K ↾t D )   &    |- ( ph -> C e. ( F lim CC B ) )   &    |- ( ph -> G e. ( ( J CnP K ) ` C ) )   =>    |- ( ph -> ( G ` C ) e. ( ( G o. F ) lim CC B ) )
Theorem	limccnp2lem 15390*	Lemma for limccnp2cntop 15391. This is most of the result, expressed in epsilon-delta form, with a large number of hypotheses so that lengthy expressions do not need to be repeated. (Contributed by Jim Kingdon, 9-Nov-2023.)
|- ( ( ph /\ x e. A ) -> R e. X )   &    |- ( ( ph /\ x e. A ) -> S e. Y )   &    |- ( ph -> X C_ CC )   &    |- ( ph -> Y C_ CC )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( ( K tX K ) ↾t ( X X. Y ) )   &    |- ( ph -> C e. ( ( x e. A |-> R ) lim CC B ) )   &    |- ( ph -> D e. ( ( x e. A |-> S ) lim CC B ) )   &    |- ( ph -> H e. ( ( J CnP K ) ` <. C , D >. ) )   &    |- F/ x ph   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> L e. RR+ )   &    |- ( ph -> A. r e. X A. s e. Y ( ( ( C ( ( abs o. - ) |` ( X X. X ) ) r ) < L /\ ( D ( ( abs o. - ) |` ( Y X. Y ) ) s ) < L ) -> ( ( C H D ) ( abs o. - ) ( r H s ) ) < E ) )   &    |- ( ph -> F e. RR+ )   &    |- ( ph -> A. x e. A ( ( x # B /\ ( abs ` ( x - B ) ) < F ) -> ( abs ` ( R - C ) ) < L ) )   &    |- ( ph -> G e. RR+ )   &    |- ( ph -> A. x e. A ( ( x # B /\ ( abs ` ( x - B ) ) < G ) -> ( abs ` ( S - D ) ) < L ) )   =>    |- ( ph -> E. d e. RR+ A. x e. A ( ( x # B /\ ( abs ` ( x - B ) ) < d ) -> ( abs ` ( ( R H S ) - ( C H D ) ) ) < E ) )
Theorem	limccnp2cntop 15391*	The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Nov-2023.)
|- ( ( ph /\ x e. A ) -> R e. X )   &    |- ( ( ph /\ x e. A ) -> S e. Y )   &    |- ( ph -> X C_ CC )   &    |- ( ph -> Y C_ CC )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- J = ( ( K tX K ) ↾t ( X X. Y ) )   &    |- ( ph -> C e. ( ( x e. A |-> R ) lim CC B ) )   &    |- ( ph -> D e. ( ( x e. A |-> S ) lim CC B ) )   &    |- ( ph -> H e. ( ( J CnP K ) ` <. C , D >. ) )   =>    |- ( ph -> ( C H D ) e. ( ( x e. A |-> ( R H S ) ) lim CC B ) )
Theorem	limccoap 15392*	Composition of two limits. This theorem is only usable in the case where x # X implies R(x) # C so it is less general than might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.) (Revised by Jim Kingdon, 18-Dec-2023.)
|- ( ( ph /\ x e. { w e. A | w # X } ) -> R e. { w e. B | w # C } )   &    |- ( ( ph /\ y e. { w e. B | w # C } ) -> S e. CC )   &    |- ( ph -> C e. ( ( x e. { w e. A | w # X } |-> R ) lim CC X ) )   &    |- ( ph -> D e. ( ( y e. { w e. B | w # C } |-> S ) lim CC C ) )   &    |- ( y = R -> S = T )   =>    |- ( ph -> D e. ( ( x e. { w e. A | w # X } |-> T ) lim CC X ) )
Theorem	reldvg 15393	The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> Rel ( S _D F ) )
Theorem	dvlemap 15394*	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|- ( ph -> F : D --> CC )   &    |- ( ph -> D C_ CC )   &    |- ( ph -> B e. D )   =>    |- ( ( ph /\ A e. { w e. D | w # B } ) -> ( ( ( F ` A ) - ( F ` B ) ) / ( A - B ) ) e. CC )
Theorem	dvfvalap 15395*	Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|- T = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. { w e. A | w # x } |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) lim CC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )
Theorem	eldvap 15396*	The differentiable predicate. A function F is differentiable at B with derivative C iff F is defined in a neighborhood of B and the difference quotient has limit C at B. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|- T = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- G = ( z e. { w e. A | w # B } |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> ( B ( S _D F ) C <-> ( B e. ( ( int ` T ) ` A ) /\ C e. ( G lim CC B ) ) ) )
Theorem	dvcl 15397	The derivative function takes values in the complex numbers. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ( ph /\ B ( S _D F ) C ) -> C e. CC )
Theorem	dvbssntrcntop 15398	The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> dom ( S _D F ) C_ ( ( int ` J ) ` A ) )
Theorem	dvbss 15399	The set of differentiable points is a subset of the domain of the function. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> dom ( S _D F ) C_ A )
Theorem	dvbsssg 15400	The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon, 28-Jun-2023.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> dom ( S _D F ) C_ S )