P. 114 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11301-11400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sqrtthi 11301	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 11302	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 11303	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 11304	Square root of square. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrtsqi 11305	Square root of square. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqsqrti 11306	Square of square root. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	sqrtge0i 11307	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 11308	A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( abs ` A ) = A )
Theorem	absnidi 11309	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 11310	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 11311	Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- ( abs ` A ) = ( sqr ` ( A ^ 2 ) )
Theorem	sqrtpclii 11312	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 11313	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 11314	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 11315	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 11316	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 11317	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 11318	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 11319	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 11320	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 11321	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 11322	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) )
Theorem	absvalsq2i 11323	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 11324	Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` A ) e. RR
Theorem	absge0i 11325	Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- 0 <_ ( abs ` A )
Theorem	absval2i 11326	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 11327	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 11328	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 11329	Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` -u A ) = ( abs ` A )
Theorem	abscji 11330	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 11331	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 11332	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 11333	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 11334	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 11335	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 11336	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 11337	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 11338	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 11339	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 11340	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 11341	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 11342	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 11343	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 11344	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 11345	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 11346	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 11347	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 11348	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 11349	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 11350	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 11351	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 11352	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 11353	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 11354	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 11355	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 11356	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 11357	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 11358	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 11359	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 11360	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 11361	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 11362	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 11363	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) e. RR )
Theorem	absvalsqd 11364	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 11365	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 11366	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( abs ` A ) )
Theorem	absval2d 11367	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 11368	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 11369	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 11370	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 11371	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscjd 11372	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 11373	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 11374	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 11375	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 11376	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 11377	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 11378	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 11379	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 11380	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 11381	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 11382	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 11383	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 11384*	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 10363. (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 11385	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 11386	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 11387	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 11388	Lemma for maxabs 11391. A variation of maxleim 11387- 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 11389	Lemma for maxabs 11391. 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 11390*	Lemma for maxabs 11391. 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 11391	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 11392	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 11393	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 , < ) )
Theorem	maxle2 11394	The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> B <_ sup ( { A , B } , RR , < ) )
Theorem	maxleast 11395	The maximum of two reals is a least upper bound. Lemma 3.11 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 22-Dec-2021.)
|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A <_ C /\ B <_ C ) ) -> sup ( { A , B } , RR , < ) <_ C )
Theorem	maxleastb 11396	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( sup ( { A , B } , RR , < ) <_ C <-> ( A <_ C /\ B <_ C ) ) )
Theorem	maxleastlt 11397	The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ C < sup ( { A , B } , RR , < ) ) ) -> ( C < A \/ C < B ) )
Theorem	maxleb 11398	Equivalence of <_ and being equal to the maximum of two reals. Lemma 3.12 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> sup ( { A , B } , RR , < ) = B ) )
Theorem	dfabsmax 11399	Absolute value of a real number in terms of maximum. Definition 3.13 of [Geuvers], p. 11. (Contributed by BJ and Jim Kingdon, 21-Dec-2021.)
|- ( A e. RR -> ( abs ` A ) = sup ( { A , -u A } , RR , < ) )
Theorem	maxltsup 11400	Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( sup ( { A , B } , RR , < ) < C <-> ( A < C /\ B < C ) ) )