P. 158 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cncfmpt1f 15701*	Composition of continuous functions. -cn-> analogue of cnmpt11f 15387. (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 15702*	Composition of continuous functions. -cn-> analogue of cnmpt12f 15389. (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 15703*	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 15704	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 15700 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 15705*	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 15706*	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 15707*	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 15708*	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 15709*	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 15710*	Lemma for mulcncf 15711. (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 15711*	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 15712*	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 15713*	The canonical bijection from ( RR X. RR ) to CC described in cnref1o 10053 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 15714*	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 15715*	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 15716*	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 15717*	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 15718*	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 15719*	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 15720*	Lemma for dedekindeu 15726. 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 15721*	Lemma for dedekindeu 15726. 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 15722*	Lemma for dedekindeu 15726. 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 15723*	Lemma for dedekindeu 15726. 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 15724*	Lemma for dedekindeu 15726. 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 15725*	Lemma for dedekindeu 15726. 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 15726*	A Dedekind cut identifies a unique real number. Similar to df-inp 7833 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 15727*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8398 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 15728*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8398 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 15729*	Lemma for dedekindicc 15736. 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 15730*	Lemma for dedekindicc 15736. 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 15731*	Lemma for dedekindicc 15736. 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 15732*	Lemma for dedekindicc 15736. 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 15733*	Lemma for dedekindicc 15736. 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 15734*	Lemma for dedekindicc 15736. 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 15735*	Lemma for dedekindicc 15736. Same as dedekindicc 15736, 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 15736*	A Dedekind cut identifies a unique real number. Similar to df-inp 7833 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 15737*	Lemma for ivthinc 15746. 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 15738*	Lemma for ivthinc 15746. 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 15739*	Lemma for ivthinc 15746. 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 15740*	Lemma for ivthinc 15746. 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 15741*	Lemma for ivthinc 15746. 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 15742*	Lemma for ivthinc 15746. 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 15743*	Lemma for ivthinc 15746. 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 15744*	Lemma for ivthinc 15746. 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 15745*	Lemma for ivthinc 15746. 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 15746*	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 15747*	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 15748*	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 15746). 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 15749	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 15750*	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 15751*	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 15752*	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 15753*	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 15754*	Lemma for ivthdich 15756. 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 15755*	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 15756*	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 15746 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 15749, hovera 15750, and hoverb 15751, 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 8393, c < 1 or 0 < c, and that leads to z <_ 0 by hoverlt1 15752 or 0 <_ z by hovergt0 15753. (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 15757	The limit operator.
class lim CC
Syntax	cdv 15758	The derivative operator.
class _D
Definition	df-limced 15759*	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 15760*	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 15761	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 15762	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( F lim CC B ) C_ CC
Theorem	ellimc3apf 15763*	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 15764*	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 15765*	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 15766*	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 15767*	Lemma for limcimo 15768. (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 15768*	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 15769	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 15770	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 15771	Lemma for cnplimccntop 15773. 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 15772	Lemma for cnplimccntop 15773. 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 15773	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 15774*	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 15775*	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 15776	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 15777*	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 15778	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 15779*	Lemma for limccnp2cntop 15780. 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 15780*	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 15781*	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 15782	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 15783*	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 15784*	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 15785*	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 15786	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 15787	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 15788	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 15789	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 )
Theorem	recnprss 15790	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	dvfgg 15791	Explicitly write out the functionality condition on derivative for S = RR and CC. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jun-2023.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S _D F ) : dom ( S _D F ) --> CC )
Theorem	dvfpm 15792	The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
|- ( F e. ( CC ^pm RR ) -> ( RR _D F ) : dom ( RR _D F ) --> CC )
Theorem	dvfcnpm 15793	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
|- ( F e. ( CC ^pm CC ) -> ( CC _D F ) : dom ( CC _D F ) --> CC )
Theorem	dvidlemap 15794*	Lemma for dvid 15798 and dvconst 15797. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|- ( ph -> F : CC --> CC )   &    |- ( ( ph /\ ( x e. CC /\ z e. CC /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( CC _D F ) = ( CC X. { B } ) )
Theorem	dvidrelem 15795*	Lemma for dvidre 15800 and dvconstre 15799. Analogue of dvidlemap 15794 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ ( x e. RR /\ z e. RR /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( RR _D F ) = ( RR X. { B } ) )
Theorem	dvidsslem 15796*	Lemma for dvconstss 15801. Analogue of dvidlemap 15794 where F is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> X e. J )   &    |- ( ( ph /\ ( x e. X /\ z e. X /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( S _D F ) = ( X X. { B } ) )
Theorem	dvconst 15797	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|- ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
Theorem	dvid 15798	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
Theorem	dvconstre 15799	Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( A e. CC -> ( RR _D ( RR X. { A } ) ) = ( RR X. { 0 } ) )
Theorem	dvidre 15800	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( RR _D ( _I |` RR ) ) = ( RR X. { 1 } )