P. 120 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fzomaxdiflem 11901	Lemma for fzomaxdif 11902. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( ( A e. ( C..^ D ) /\ B e. ( C..^ D ) ) /\ A <_ B ) -> ( abs ` ( B - A ) ) e. ( 0..^ ( D - C ) ) )
Theorem	fzomaxdif 11902	A bound on the separation of two points in a half-open range. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( A e. ( C..^ D ) /\ B e. ( C..^ D ) ) -> ( abs ` ( A - B ) ) e. ( 0..^ ( D - C ) ) )
Theorem	cau3lem 11903*	Lemma for cau3 11904. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.)
|- Z C_ ZZ   &    |- ( ta -> ps )   &    |- ( ( F ` k ) = ( F ` j ) -> ( ps <-> ch ) )   &    |- ( ( F ` k ) = ( F ` m ) -> ( ps <-> th ) )   &    |- ( ( ph /\ ch /\ ps ) -> ( G ` ( ( F ` j ) D ( F ` k ) ) ) = ( G ` ( ( F ` k ) D ( F ` j ) ) ) )   &    |- ( ( ph /\ th /\ ch ) -> ( G ` ( ( F ` m ) D ( F ` j ) ) ) = ( G ` ( ( F ` j ) D ( F ` m ) ) ) )   &    |- ( ( ph /\ ( ps /\ th ) /\ ( ch /\ x e. RR ) ) -> ( ( ( G ` ( ( F ` k ) D ( F ` j ) ) ) < ( x / 2 ) /\ ( G ` ( ( F ` j ) D ( F ` m ) ) ) < ( x / 2 ) ) -> ( G ` ( ( F ` k ) D ( F ` m ) ) ) < x ) )   =>    |- ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ta /\ ( G ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ta /\ A. m e. ( ZZ>= ` k ) ( G ` ( ( F ` k ) D ( F ` m ) ) ) < x ) ) )
Theorem	cau3 11904*	Convert between three-quantifier and four-quantifier versions of the Cauchy criterion. (In particular, the four-quantifier version has no occurrence of j in the assertion, so it can be used with rexanuz 11776 and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. m e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
Theorem	cau4 11905*	Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   =>    |- ( N e. Z -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
Theorem	caubnd2 11906*	A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. y e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < y )
Theorem	amgm2 11907	Arithmetic-geometric mean inequality for n = 2. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) <_ ( ( A + B ) / 2 ) )
Theorem	sqrtthi 11908	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 <_ A -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtcli 11909	The square root of a nonnegative real is a real. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` A ) e. RR )
Theorem	sqrtgt0i 11910	The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 < A -> 0 < ( sqr ` A ) )
Theorem	sqrtmsqi 11911	Square root of square. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrtsqi 11912	Square root of square. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqsqrti 11913	Square of square root. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	sqrtge0i 11914	The square root of a nonnegative real is nonnegative. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 <_ A -> 0 <_ ( sqr ` A ) )
Theorem	absidi 11915	A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( abs ` A ) = A )
Theorem	absnidi 11916	A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( A <_ 0 -> ( abs ` A ) = -u A )
Theorem	leabsi 11917	A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- A <_ ( abs ` A )
Theorem	absrei 11918	Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- ( abs ` A ) = ( sqr ` ( A ^ 2 ) )
Theorem	sqrtpclii 11919	The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   &    |- 0 < A   =>    |- ( sqr ` A ) e. RR
Theorem	sqrtgt0ii 11920	The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   &    |- 0 < A   =>    |- 0 < ( sqr ` A )
Theorem	sqrt11i 11921	The square root function is one-to-one. (Contributed by NM, 27-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) )
Theorem	sqrtmuli 11922	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) )
Theorem	sqrtmulii 11923	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 <_ A   &    |- 0 <_ B   =>    |- ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) )
Theorem	sqrtmsq2i 11924	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = B <-> A = ( B x. B ) ) )
Theorem	sqrtlei 11925	Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) )
Theorem	sqrtlti 11926	Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) )
Theorem	abslti 11927	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) )
Theorem	abslei 11928	Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) )
Theorem	absvalsqi 11929	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) )
Theorem	absvalsq2i 11930	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) )
Theorem	abscli 11931	Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` A ) e. RR
Theorem	absge0i 11932	Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- 0 <_ ( abs ` A )
Theorem	absval2i 11933	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	abs00i 11934	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) = 0 <-> A = 0 )
Theorem	absgt0api 11935	The absolute value of a nonzero number is positive. Remark in [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   =>    |- ( A # 0 <-> 0 < ( abs ` A ) )
Theorem	absnegi 11936	Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` -u A ) = ( abs ` A )
Theorem	abscji 11937	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( abs ` ( * ` A ) ) = ( abs ` A )
Theorem	releabsi 11938	The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Re ` A ) <_ ( abs ` A )
Theorem	abssubi 11939	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( abs ` ( A - B ) ) = ( abs ` ( B - A ) )
Theorem	absmuli 11940	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) )
Theorem	sqabsaddi 11941	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )
Theorem	sqabssubi 11942	Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )
Theorem	absdivapzi 11943	Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )
Theorem	abstrii 11944	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. This is Metamath 100 proof #91. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) )
Theorem	abs3difi 11945	Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) )
Theorem	abs3lemi 11946	Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. RR   =>    |- ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D )
Theorem	rpsqrtcld 11947	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( sqr ` A ) e. RR+ )
Theorem	sqrtgt0d 11948	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 < ( sqr ` A ) )
Theorem	absnidd 11949	A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A <_ 0 )   =>    |- ( ph -> ( abs ` A ) = -u A )
Theorem	leabsd 11950	A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ ( abs ` A ) )
Theorem	absred 11951	Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( abs ` A ) = ( sqr ` ( A ^ 2 ) ) )
Theorem	resqrtcld 11952	The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` A ) e. RR )
Theorem	sqrtmsqd 11953	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrtsqd 11954	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqrtge0d 11955	The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> 0 <_ ( sqr ` A ) )
Theorem	absidd 11956	A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( abs ` A ) = A )
Theorem	sqrtdivd 11957	Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) )
Theorem	sqrtmuld 11958	Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) )
Theorem	sqrtsq2d 11959	Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) )
Theorem	sqrtled 11960	Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) )
Theorem	sqrtltd 11961	Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) )
Theorem	sqr11d 11962	The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> ( sqr ` A ) = ( sqr ` B ) )   =>    |- ( ph -> A = B )
Theorem	absltd 11963	Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) ) )
Theorem	absled 11964	Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) )
Theorem	abssubge0d 11965	Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( B - A ) ) = ( B - A ) )
Theorem	abssuble0d 11966	Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( A - B ) ) = ( B - A ) )
Theorem	absdifltd 11967	The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) < C <-> ( ( B - C ) < A /\ A < ( B + C ) ) ) )
Theorem	absdifled 11968	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) <_ C <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )
Theorem	icodiamlt 11969	Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) ) -> ( abs ` ( C - D ) ) < ( B - A ) )
Theorem	abscld 11970	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) e. RR )
Theorem	absvalsqd 11971	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2d 11972	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	absge0d 11973	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( abs ` A ) )
Theorem	absval2d 11974	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
Theorem	abs00d 11975	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	absne0d 11976	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( abs ` A ) =/= 0 )
Theorem	absrpclapd 11977	The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( abs ` A ) e. RR+ )
Theorem	absnegd 11978	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscjd 11979	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` ( * ` A ) ) = ( abs ` A ) )
Theorem	releabsd 11980	The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` A ) <_ ( abs ` A ) )
Theorem	absexpd 11981	Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )
Theorem	abssubd 11982	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
Theorem	absmuld 11983	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
Theorem	absdivapd 11984	Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )
Theorem	abstrid 11985	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difd 11986	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs2dif2d 11987	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difabsd 11988	Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs3difd 11989	Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
Theorem	abs3lemd 11990	Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. RR )   &    |- ( ph -> ( abs ` ( A - C ) ) < ( D / 2 ) )   &    |- ( ph -> ( abs ` ( C - B ) ) < ( D / 2 ) )   =>    |- ( ph -> ( abs ` ( A - B ) ) < D )
Theorem	qdenre 11991*	The rational numbers are dense in RR: any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 10708. (Contributed by BJ, 15-Oct-2021.)
|- ( ( A e. RR /\ B e. RR+ ) -> E. x e. QQ ( abs ` ( x - A ) ) < B )
4.8.5  The maximum of two real numbers
Theorem	maxcom 11992	The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- sup ( { A , B } , RR , < ) = sup ( { B , A } , RR , < )
Theorem	maxabsle 11993	An upper bound for { A , B }. (Contributed by Jim Kingdon, 20-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> A <_ ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )
Theorem	maxleim 11994	Value of maximum when we know which number is larger. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> sup ( { A , B } , RR , < ) = B ) )
Theorem	maxabslemab 11995	Lemma for maxabs 11998. A variation of maxleim 11994- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) = B )
Theorem	maxabslemlub 11996	Lemma for maxabs 11998. A least upper bound for { A , B }. (Contributed by Jim Kingdon, 20-Dec-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> C < ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )   =>    |- ( ph -> ( C < A \/ C < B ) )
Theorem	maxabslemval 11997*	Lemma for maxabs 11998. Value of the supremum. (Contributed by Jim Kingdon, 22-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) e. RR /\ A. x e. { A , B } -. ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) < x /\ A. x e. RR ( x < ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) -> E. z e. { A , B } x < z ) ) )
Theorem	maxabs 11998	Maximum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 20-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) = ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )
Theorem	maxcl 11999	The maximum of two real numbers is a real number. (Contributed by Jim Kingdon, 22-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) e. RR )
Theorem	maxle1 12000	The maximum of two reals is no smaller than the first real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> A <_ sup ( { A , B } , RR , < ) )