P. 112 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11101-11200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	absgt0ap 11101	The absolute value of a number apart from zero is positive. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( A e. CC -> ( A # 0 <-> 0 < ( abs ` A ) ) )
Theorem	nnabscl 11102	The absolute value of a nonzero integer is a positive integer. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
Theorem	abssub 11103	Swapping order of subtraction doesn't change the absolute value. (Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
Theorem	abssubge0 11104	Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( B - A ) ) = ( B - A ) )
Theorem	abssuble0 11105	Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( B - A ) )
Theorem	abstri 11106	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by NM, 7-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs3dif 11107	Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
Theorem	abs2dif 11108	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs2dif2 11109	Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difabs 11110	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) )
Theorem	recan 11111*	Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) <-> A = B ) )
Theorem	absf 11112	Mapping domain and codomain of the absolute value function. (Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- abs : CC --> RR
Theorem	abs3lem 11113	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	fzomaxdiflem 11114	Lemma for fzomaxdif 11115. (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 11115	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 11116*	Lemma for cau3 11117. (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 11117*	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 10990 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 11118*	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 11119*	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 11120	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 11121	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 11122	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 11123	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 11124	Square root of square. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrtsqi 11125	Square root of square. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqsqrti 11126	Square of square root. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	sqrtge0i 11127	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 11128	A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( abs ` A ) = A )
Theorem	absnidi 11129	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 11130	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 11131	Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- ( abs ` A ) = ( sqr ` ( A ^ 2 ) )
Theorem	sqrtpclii 11132	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 11133	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 11134	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 11135	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 11136	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 11137	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 11138	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 11139	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 11140	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 11141	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 11142	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) )
Theorem	absvalsq2i 11143	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 11144	Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` A ) e. RR
Theorem	absge0i 11145	Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- 0 <_ ( abs ` A )
Theorem	absval2i 11146	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 11147	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 11148	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 11149	Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` -u A ) = ( abs ` A )
Theorem	abscji 11150	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 11151	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 11152	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 11153	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 11154	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 11155	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 11156	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 11157	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 11158	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 11159	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 11160	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 11161	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 11162	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 11163	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 11164	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 11165	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 11166	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 11167	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 11168	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 11169	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 11170	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 11171	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 11172	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 11173	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 11174	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 11175	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 11176	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 11177	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 11178	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 11179	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 11180	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 11181	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 11182	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 11183	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) e. RR )
Theorem	absvalsqd 11184	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 11185	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 11186	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( abs ` A ) )
Theorem	absval2d 11187	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 11188	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 11189	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 11190	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 11191	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscjd 11192	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 11193	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 11194	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 11195	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 11196	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 11197	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 11198	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 11199	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 11200	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 ) ) )