P. 116 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11501-11600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recvguniq 11501*	Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) < ( L + x ) /\ L < ( ( F ` k ) + x ) ) )   &    |- ( ph -> M e. RR )   &    |- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) < ( M + x ) /\ M < ( ( F ` k ) + x ) ) )   =>    |- ( ph -> L = M )
4.8.4  Square root; absolute value
Syntax	csqrt 11502	Extend class notation to include square root of a complex number.
class sqr
Syntax	cabs 11503	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-rsqrt 11504*	Define a function whose value is the square root of a nonnegative real number. Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.)
|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
Definition	df-abs 11505	Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
Theorem	sqrtrval 11506*	Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
|- ( A e. RR -> ( sqr ` A ) = ( iota_ x e. RR ( ( x ^ 2 ) = A /\ 0 <_ x ) ) )
Theorem	absval 11507	The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( A e. CC -> ( abs ` A ) = ( sqr ` ( A x. ( * ` A ) ) ) )
Theorem	rennim 11508	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
|- ( A e. RR -> ( _i x. A ) e/ RR+ )
Theorem	sqrt0rlem 11509	Lemma for sqrt0 11510. (Contributed by Jim Kingdon, 26-Aug-2020.)
|- ( ( A e. RR /\ ( ( A ^ 2 ) = 0 /\ 0 <_ A ) ) <-> A = 0 )
Theorem	sqrt0 11510	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( sqr ` 0 ) = 0
Theorem	resqrexlem1arp 11511	Lemma for resqrex 11532. 1 + A is a positive real (expressed in a way that will help apply seqf 10681 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( NN X. { ( 1 + A ) } ) ` N ) e. RR+ )
Theorem	resqrexlemp1rp 11512*	Lemma for resqrex 11532. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10681 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ ( B e. RR+ /\ C e. RR+ ) ) -> ( B ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) C ) e. RR+ )
Theorem	resqrexlemf 11513*	Lemma for resqrex 11532. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- 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 -> F : NN --> RR+ )
Theorem	resqrexlemf1 11514*	Lemma for resqrex 11532. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- 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 -> ( F ` 1 ) = ( 1 + A ) )
Theorem	resqrexlemfp1 11515*	Lemma for resqrex 11532. Recursion rule. This sequence is the ancient method for computing square roots, often known as the babylonian method, although known to many ancient cultures. (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 /\ N e. NN ) -> ( F ` ( N + 1 ) ) = ( ( ( F ` N ) + ( A / ( F ` N ) ) ) / 2 ) )
Theorem	resqrexlemover 11516*	Lemma for resqrex 11532. Each element of the sequence is an overestimate. (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 /\ N e. NN ) -> A < ( ( F ` N ) ^ 2 ) )
Theorem	resqrexlemdec 11517*	Lemma for resqrex 11532. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-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 /\ N e. NN ) -> ( F ` ( N + 1 ) ) < ( F ` N ) )
Theorem	resqrexlemdecn 11518*	Lemma for resqrex 11532. The sequence is decreasing. (Contributed by Jim Kingdon, 31-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 -> N e. NN )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N < M )   =>    |- ( ph -> ( F ` M ) < ( F ` N ) )
Theorem	resqrexlemlo 11519*	Lemma for resqrex 11532. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-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 /\ N e. NN ) -> ( 1 / ( 2 ^ N ) ) < ( F ` N ) )
Theorem	resqrexlemcalc1 11520*	Lemma for resqrex 11532. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-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 /\ N e. NN ) -> ( ( ( F ` ( N + 1 ) ) ^ 2 ) - A ) = ( ( ( ( ( F ` N ) ^ 2 ) - A ) ^ 2 ) / ( 4 x. ( ( F ` N ) ^ 2 ) ) ) )
Theorem	resqrexlemcalc2 11521*	Lemma for resqrex 11532. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-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 /\ N e. NN ) -> ( ( ( F ` ( N + 1 ) ) ^ 2 ) - A ) <_ ( ( ( ( F ` N ) ^ 2 ) - A ) / 4 ) )
Theorem	resqrexlemcalc3 11522*	Lemma for resqrex 11532. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-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 /\ N e. NN ) -> ( ( ( F ` N ) ^ 2 ) - A ) <_ ( ( ( F ` 1 ) ^ 2 ) / ( 4 ^ ( N - 1 ) ) ) )
Theorem	resqrexlemnmsq 11523*	Lemma for resqrex 11532. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-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 -> N e. NN )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N <_ M )   =>    |- ( ph -> ( ( ( F ` N ) ^ 2 ) - ( ( F ` M ) ^ 2 ) ) < ( ( ( F ` 1 ) ^ 2 ) / ( 4 ^ ( N - 1 ) ) ) )
Theorem	resqrexlemnm 11524*	Lemma for resqrex 11532. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-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 -> N e. NN )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N <_ M )   =>    |- ( ph -> ( ( F ` N ) - ( F ` M ) ) < ( ( ( ( F ` 1 ) ^ 2 ) x. 2 ) / ( 2 ^ ( N - 1 ) ) ) )
Theorem	resqrexlemcvg 11525*	Lemma for resqrex 11532. 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 11526*	Lemma for resqrex 11532. 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 11527*	Lemma for resqrex 11532. 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 11528*	Lemma for resqrex 11532. 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 11529*	Lemma for resqrex 11532. 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 11530*	Lemma for resqrex 11532. 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 11531*	Lemma for resqrex 11532. 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 11532*	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 11533*	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 11534*	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 11535	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR )
Theorem	rersqrtthlem 11536	Lemma for resqrtth 11537. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( sqr ` A ) ) )
Theorem	resqrtth 11537	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 11538	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtge0 11539	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 11540	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 11541	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 11542	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 11543	Square root is strictly monotonic. Closed form of sqrtlti 11643. (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 11544	Analogue to sqrt11 11545 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 11545	The square root function is one-to-one. Also see sqrt11ap 11544 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 11546	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 11547	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 11548	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 11549	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 11550	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 11551	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 11552	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|- ( sqr ` 1 ) = 1
Theorem	sqrt4 11553	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|- ( sqr ` 4 ) = 2
Theorem	sqrt9 11554	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|- ( sqr ` 9 ) = 3
Theorem	sqrt2gt1lt2 11555	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 11556	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscl 11557	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|- ( A e. CC -> ( abs ` A ) e. RR )
Theorem	abscj 11558	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 11559	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2 11560	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 11561	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 11562	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 11563	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 11564	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( abs ` 0 ) = 0
Theorem	absi 11565	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( abs ` _i ) = 1
Theorem	absge0 11566	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 11567	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 11568	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 11569	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 11570	The absolute value of a number is zero iff the number is zero. Also see abs00ap 11568 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 11571	A complex number is zero iff its absolute value is zero. Deduction form of abs00 11570. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) = 0 <-> A = 0 ) )
Theorem	abs00bd 11572	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 11573	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 11574	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 11575	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 11576	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 11577	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 11578	The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- ( abs ` 1 ) = 1
Theorem	absnid 11579	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 11580	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 11581	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 11582	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 11583	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|- ( A e. RR -> ( abs ` A ) = ( sqr ` ( A ^ 2 ) ) )
Theorem	absresq 11584	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 11585	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 11586	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 11587	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 11588	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 11589	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 11590	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 11591	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 11592	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 11593	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 11594	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 11595	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 11596	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 11597	If the absolute value of a complex number is less than a real, its difference from the real is nonzero. See also abssubap0 11596 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 11598	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 11599	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 11600	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 ) )