P. 113 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11201-11300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	resqrexlemcvg 11201*	Lemma for resqrex 11208. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> E. r e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( r + x ) /\ r < ( ( F ` i ) + x ) ) )
Theorem	resqrexlemgt0 11202*	Lemma for resqrex 11208. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   =>    |- ( ph -> 0 <_ L )
Theorem	resqrexlemoverl 11203*	Lemma for resqrex 11208. Every term in the sequence is an overestimate compared with the limit L. Although this theorem is stated in terms of a particular sequence the proof could be adapted for any decreasing convergent sequence. (Contributed by Jim Kingdon, 9-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   &    |- ( ph -> K e. NN )   =>    |- ( ph -> L <_ ( F ` K ) )
Theorem	resqrexlemglsq 11204*	Lemma for resqrex 11208. The sequence formed by squaring each term of F converges to ( L ^ 2 ). (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   &    |- G = ( x e. NN |-> ( ( F ` x ) ^ 2 ) )   =>    |- ( ph -> A. e e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( G ` k ) < ( ( L ^ 2 ) + e ) /\ ( L ^ 2 ) < ( ( G ` k ) + e ) ) )
Theorem	resqrexlemga 11205*	Lemma for resqrex 11208. The sequence formed by squaring each term of F converges to A. (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   &    |- G = ( x e. NN |-> ( ( F ` x ) ^ 2 ) )   =>    |- ( ph -> A. e e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( G ` k ) < ( A + e ) /\ A < ( ( G ` k ) + e ) ) )
Theorem	resqrexlemsqa 11206*	Lemma for resqrex 11208. The square of a limit is A. (Contributed by Jim Kingdon, 7-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   =>    |- ( ph -> ( L ^ 2 ) = A )
Theorem	resqrexlemex 11207*	Lemma for resqrex 11208. Existence of square root given a sequence which converges to the square root. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
Theorem	resqrex 11208*	Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
Theorem	rsqrmo 11209*	Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> E* x e. RR ( ( x ^ 2 ) = A /\ 0 <_ x ) )
Theorem	rersqreu 11210*	Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> E! x e. RR ( ( x ^ 2 ) = A /\ 0 <_ x ) )
Theorem	resqrtcl 11211	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR )
Theorem	rersqrtthlem 11212	Lemma for resqrtth 11213. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( sqr ` A ) ) )
Theorem	resqrtth 11213	Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	remsqsqrt 11214	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtge0 11215	The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqr ` A ) )
Theorem	sqrtgt0 11216	The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- ( ( A e. RR /\ 0 < A ) -> 0 < ( sqr ` A ) )
Theorem	sqrtmul 11217	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) )
Theorem	sqrtle 11218	Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) )
Theorem	sqrtlt 11219	Square root is strictly monotonic. Closed form of sqrtlti 11319. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) )
Theorem	sqrt11ap 11220	Analogue to sqrt11 11221 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) # ( sqr ` B ) <-> A # B ) )
Theorem	sqrt11 11221	The square root function is one-to-one. Also see sqrt11ap 11220 which would follow easily from this given excluded middle, but which is proved another way without it. (Contributed by Scott Fenton, 11-Jun-2013.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) )
Theorem	sqrt00 11222	A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) = 0 <-> A = 0 ) )
Theorem	rpsqrtcl 11223	The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.)
|- ( A e. RR+ -> ( sqr ` A ) e. RR+ )
Theorem	sqrtdiv 11224	Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) )
Theorem	sqrtsq2 11225	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) )
Theorem	sqrtsq 11226	Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqrtmsq 11227	Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrt1 11228	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|- ( sqr ` 1 ) = 1
Theorem	sqrt4 11229	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|- ( sqr ` 4 ) = 2
Theorem	sqrt9 11230	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|- ( sqr ` 9 ) = 3
Theorem	sqrt2gt1lt2 11231	The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- ( 1 < ( sqr ` 2 ) /\ ( sqr ` 2 ) < 2 )
Theorem	absneg 11232	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscl 11233	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|- ( A e. CC -> ( abs ` A ) e. RR )
Theorem	abscj 11234	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.)
|- ( A e. CC -> ( abs ` ( * ` A ) ) = ( abs ` A ) )
Theorem	absvalsq 11235	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2 11236	Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	sqabsadd 11237	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-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	sqabssub 11238	Square of absolute value of difference. (Contributed by NM, 21-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	absval2 11239	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
|- ( A e. CC -> ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
Theorem	abs0 11240	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( abs ` 0 ) = 0
Theorem	absi 11241	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( abs ` _i ) = 1
Theorem	absge0 11242	Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( A e. CC -> 0 <_ ( abs ` A ) )
Theorem	absrpclap 11243	The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ( A e. CC /\ A # 0 ) -> ( abs ` A ) e. RR+ )
Theorem	abs00ap 11244	The absolute value of a number is apart from zero iff the number is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( A e. CC -> ( ( abs ` A ) # 0 <-> A # 0 ) )
Theorem	absext 11245	Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) # ( abs ` B ) -> A # B ) )
Theorem	abs00 11246	The absolute value of a number is zero iff the number is zero. Also see abs00ap 11244 which is similar but for apartness. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )
Theorem	abs00ad 11247	A complex number is zero iff its absolute value is zero. Deduction form of abs00 11246. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) = 0 <-> A = 0 ) )
Theorem	abs00bd 11248	If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = 0 )   =>    |- ( ph -> ( abs ` A ) = 0 )
Theorem	absreimsq 11249	Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
Theorem	absreim 11250	Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.)
|- ( ( A e. RR /\ B e. RR ) -> ( abs ` ( A + ( _i x. B ) ) ) = ( sqr ` ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
Theorem	absmul 11251	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
Theorem	absdivap 11252	Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ( A e. CC /\ B e. CC /\ B # 0 ) -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )
Theorem	absid 11253	A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
Theorem	abs1 11254	The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- ( abs ` 1 ) = 1
Theorem	absnid 11255	A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.)
|- ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )
Theorem	leabs 11256	A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.)
|- ( A e. RR -> A <_ ( abs ` A ) )
Theorem	qabsor 11257	The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|- ( A e. QQ -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )
Theorem	qabsord 11258	The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|- ( ph -> A e. QQ )   =>    |- ( ph -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )
Theorem	absre 11259	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|- ( A e. RR -> ( abs ` A ) = ( sqr ` ( A ^ 2 ) ) )
Theorem	absresq 11260	Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.)
|- ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
Theorem	absexp 11261	Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )
Theorem	absexpzap 11262	Absolute value of integer exponentiation. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )
Theorem	abssq 11263	Square can be moved in and out of absolute value. (Contributed by Scott Fenton, 18-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( abs ` ( A ^ 2 ) ) )
Theorem	sqabs 11264	The squares of two reals are equal iff their absolute values are equal. (Contributed by NM, 6-Mar-2009.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( abs ` A ) = ( abs ` B ) ) )
Theorem	absrele 11265	The absolute value of a complex number is greater than or equal to the absolute value of its real part. (Contributed by NM, 1-Apr-2005.)
|- ( A e. CC -> ( abs ` ( Re ` A ) ) <_ ( abs ` A ) )
Theorem	absimle 11266	The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( A e. CC -> ( abs ` ( Im ` A ) ) <_ ( abs ` A ) )
Theorem	nn0abscl 11267	The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005.)
|- ( A e. ZZ -> ( abs ` A ) e. NN0 )
Theorem	zabscl 11268	The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( A e. ZZ -> ( abs ` A ) e. ZZ )
Theorem	ltabs 11269	A number which is less than its absolute value is negative. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- ( ( A e. RR /\ A < ( abs ` A ) ) -> A < 0 )
Theorem	abslt 11270	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) ) )
Theorem	absle 11271	Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) )
Theorem	abssubap0 11272	If the absolute value of a complex number is less than a real, its difference from the real is apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.)
|- ( ( A e. CC /\ B e. RR /\ ( abs ` A ) < B ) -> ( B - A ) # 0 )
Theorem	abssubne0 11273	If the absolute value of a complex number is less than a real, its difference from the real is nonzero. See also abssubap0 11272 which is the same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.)
|- ( ( A e. CC /\ B e. RR /\ ( abs ` A ) < B ) -> ( B - A ) =/= 0 )
Theorem	absdiflt 11274	The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) < C <-> ( ( B - C ) < A /\ A < ( B + C ) ) ) )
Theorem	absdifle 11275	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) <_ C <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )
Theorem	elicc4abs 11276	Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( ( A - B ) [,] ( A + B ) ) <-> ( abs ` ( C - A ) ) <_ B ) )
Theorem	lenegsq 11277	Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.)
|- ( ( A e. RR /\ B e. RR /\ 0 <_ B ) -> ( ( A <_ B /\ -u A <_ B ) <-> ( A ^ 2 ) <_ ( B ^ 2 ) ) )
Theorem	releabs 11278	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, 1-Apr-2005.)
|- ( A e. CC -> ( Re ` A ) <_ ( abs ` A ) )
Theorem	recvalap 11279	Reciprocal expressed with a real denominator. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( ( A e. CC /\ A # 0 ) -> ( 1 / A ) = ( ( * ` A ) / ( ( abs ` A ) ^ 2 ) ) )
Theorem	absidm 11280	The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.)
|- ( A e. CC -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
Theorem	absgt0ap 11281	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 11282	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 11283	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 11284	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 11285	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 11286	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 11287	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 11288	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 11289	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 11290	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 11291*	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 11292	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 11293	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 11294	Lemma for fzomaxdif 11295. (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 11295	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 11296*	Lemma for cau3 11297. (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 11297*	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 11170 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 11298*	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 11299*	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 11300	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 ) )