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
PART 10  BASIC REAL AND COMPLEX ANALYSIS
10.1  Continuity
Theorem	addcncf 15301*	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 15302*	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 15303*	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 15304*	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 15305*	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 15306*	Lemma for dedekindeu 15312. 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 15307*	Lemma for dedekindeu 15312. 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 15308*	Lemma for dedekindeu 15312. 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 15309*	Lemma for dedekindeu 15312. 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 15310*	Lemma for dedekindeu 15312. 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 15311*	Lemma for dedekindeu 15312. 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 15312*	A Dedekind cut identifies a unique real number. Similar to df-inp 7664 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 15313*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8230 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 15314*	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8230 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 15315*	Lemma for dedekindicc 15322. 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 15316*	Lemma for dedekindicc 15322. 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 15317*	Lemma for dedekindicc 15322. 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 15318*	Lemma for dedekindicc 15322. 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 15319*	Lemma for dedekindicc 15322. 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 15320*	Lemma for dedekindicc 15322. 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 15321*	Lemma for dedekindicc 15322. Same as dedekindicc 15322, 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 15322*	A Dedekind cut identifies a unique real number. Similar to df-inp 7664 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 15323*	Lemma for ivthinc 15332. 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 15324*	Lemma for ivthinc 15332. 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 15325*	Lemma for ivthinc 15332. 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 15326*	Lemma for ivthinc 15332. 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 15327*	Lemma for ivthinc 15332. 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 15328*	Lemma for ivthinc 15332. 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 15329*	Lemma for ivthinc 15332. 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 15330*	Lemma for ivthinc 15332. 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 15331*	Lemma for ivthinc 15332. 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 15332*	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 15333*	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 15334*	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 15332). 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 15335	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 15336*	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 15337*	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 15338*	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 15339*	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 15340*	Lemma for ivthdich 15342. 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 15341*	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 15342*	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 15332 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 15335, hovera 15336, and hoverb 15337, 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 8225, c < 1 or 0 < c, and that leads to z <_ 0 by hoverlt1 15338 or 0 <_ z by hovergt0 15339. (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 15343	The limit operator.
class lim CC
Syntax	cdv 15344	The derivative operator.
class _D
Definition	df-limced 15345*	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 15346*	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 15347	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 15348	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( F lim CC B ) C_ CC
Theorem	ellimc3apf 15349*	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 15350*	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 15351*	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 15352*	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 15353*	Lemma for limcimo 15354. (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 15354*	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 15355	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 15356	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 15357	Lemma for cnplimccntop 15359. 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 15358	Lemma for cnplimccntop 15359. 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 15359	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 15360*	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 15361*	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 15362	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 15363*	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 15364	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 15365*	Lemma for limccnp2cntop 15366. 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 15366*	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 15367*	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 15368	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 15369*	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 15370*	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 15371*	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 15372	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 15373	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 15374	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 15375	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 15376	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	dvfgg 15377	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 15378	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 15379	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 15380*	Lemma for dvid 15384 and dvconst 15383. (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 15381*	Lemma for dvidre 15386 and dvconstre 15385. Analogue of dvidlemap 15380 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 15382*	Lemma for dvconstss 15387. Analogue of dvidlemap 15380 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 15383	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 15384	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 15385	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 15386	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( RR _D ( _I |` RR ) ) = ( RR X. { 1 } )
Theorem	dvconstss 15387	Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> X e. J )   &    |- ( ph -> A e. CC )   =>    |- ( ph -> ( S _D ( X X. { A } ) ) = ( X X. { 0 } ) )
Theorem	dvcnp2cntop 15388	A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- J = ( K ↾t A )   &    |- K = ( MetOpen ` ( abs o. - ) )   =>    |- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )
Theorem	dvcn 15389	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> F e. ( A -cn-> CC ) )
Theorem	dvaddxxbr 15390	The sum rule for derivatives at a point. That is, if the derivative of F at C is K and the derivative of G at C is L, then the derivative of the pointwise sum of those two functions at C is K + L. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> C ( S _D F ) K )   &    |- ( ph -> C ( S _D G ) L )   &    |- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> C ( S _D ( F oF + G ) ) ( K + L ) )
Theorem	dvmulxxbr 15391	The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 15393. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> C ( S _D F ) K )   &    |- ( ph -> C ( S _D G ) L )   &    |- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> C ( S _D ( F oF x. G ) ) ( ( K x. ( G ` C ) ) + ( L x. ( F ` C ) ) ) )
Theorem	dvaddxx 15392	The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 15390. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> C e. dom ( S _D F ) )   &    |- ( ph -> C e. dom ( S _D G ) )   =>    |- ( ph -> ( ( S _D ( F oF + G ) ) ` C ) = ( ( ( S _D F ) ` C ) + ( ( S _D G ) ` C ) ) )
Theorem	dvmulxx 15393	The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 15391. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> C e. dom ( S _D F ) )   &    |- ( ph -> C e. dom ( S _D G ) )   =>    |- ( ph -> ( ( S _D ( F oF x. G ) ) ` C ) = ( ( ( ( S _D F ) ` C ) x. ( G ` C ) ) + ( ( ( S _D G ) ` C ) x. ( F ` C ) ) ) )
Theorem	dviaddf 15394	The sum rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X C_ S )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> dom ( S _D G ) = X )   =>    |- ( ph -> ( S _D ( F oF + G ) ) = ( ( S _D F ) oF + ( S _D G ) ) )
Theorem	dvimulf 15395	The product rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X C_ S )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> dom ( S _D G ) = X )   =>    |- ( ph -> ( S _D ( F oF x. G ) ) = ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) )
Theorem	dvcoapbr 15396*	The chain rule for derivatives at a point. The u # C -> ( G ` u ) # ( G ` C ) hypothesis constrains what functions work for G. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> X )   &    |- ( ph -> Y C_ T )   &    |- ( ph -> A. u e. Y ( u # C -> ( G ` u ) # ( G ` C ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> T C_ CC )   &    |- ( ph -> ( G ` C ) ( S _D F ) K )   &    |- ( ph -> C ( T _D G ) L )   &    |- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> C ( T _D ( F o. G ) ) ( K x. L ) )
Theorem	dvcjbr 15397	The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 15398. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ RR )   &    |- ( ph -> C e. dom ( RR _D F ) )   =>    |- ( ph -> C ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` C ) ) )
Theorem	dvcj 15398	The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 15397. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. F ) ) = ( * o. ( RR _D F ) ) )
Theorem	dvfre 15399	The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ( F : A --> RR /\ A C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
Theorem	dvexp 15400*	Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|- ( N e. NN -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )