P. 109 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cabs 10801	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-rsqrt 10802*	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 10803	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 10804*	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 10805	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 10806	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 10807	Lemma for sqrt0 10808. (Contributed by Jim Kingdon, 26-Aug-2020.)
|- ( ( A e. RR /\ ( ( A ^ 2 ) = 0 /\ 0 <_ A ) ) <-> A = 0 )
Theorem	sqrt0 10808	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( sqr ` 0 ) = 0
Theorem	resqrexlem1arp 10809	Lemma for resqrex 10830. 1 + A is a positive real (expressed in a way that will help apply seqf 10265 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 10810*	Lemma for resqrex 10830. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10265 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 10811*	Lemma for resqrex 10830. 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 10812*	Lemma for resqrex 10830. 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 10813*	Lemma for resqrex 10830. 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 10814*	Lemma for resqrex 10830. 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 10815*	Lemma for resqrex 10830. 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 10816*	Lemma for resqrex 10830. 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 10817*	Lemma for resqrex 10830. 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 10818*	Lemma for resqrex 10830. 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 10819*	Lemma for resqrex 10830. 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 10820*	Lemma for resqrex 10830. 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 10821*	Lemma for resqrex 10830. 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 10822*	Lemma for resqrex 10830. 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 10823*	Lemma for resqrex 10830. 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 10824*	Lemma for resqrex 10830. 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 10825*	Lemma for resqrex 10830. 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 10826*	Lemma for resqrex 10830. 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 10827*	Lemma for resqrex 10830. 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 10828*	Lemma for resqrex 10830. 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 10829*	Lemma for resqrex 10830. 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 10830*	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 10831*	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 10832*	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 10833	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR )
Theorem	rersqrtthlem 10834	Lemma for resqrtth 10835. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( sqr ` A ) ) )
Theorem	resqrtth 10835	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 10836	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtge0 10837	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 10838	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 10839	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 10840	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 10841	Square root is strictly monotonic. Closed form of sqrtlti 10941. (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 10842	Analogue to sqrt11 10843 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 10843	The square root function is one-to-one. Also see sqrt11ap 10842 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 10844	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 10845	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 10846	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 10847	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 10848	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 10849	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 10850	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|- ( sqr ` 1 ) = 1
Theorem	sqrt4 10851	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|- ( sqr ` 4 ) = 2
Theorem	sqrt9 10852	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|- ( sqr ` 9 ) = 3
Theorem	sqrt2gt1lt2 10853	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 10854	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscl 10855	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|- ( A e. CC -> ( abs ` A ) e. RR )
Theorem	abscj 10856	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 10857	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2 10858	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 10859	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 10860	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 10861	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 10862	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( abs ` 0 ) = 0
Theorem	absi 10863	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( abs ` _i ) = 1
Theorem	absge0 10864	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 10865	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 10866	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 10867	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 10868	The absolute value of a number is zero iff the number is zero. Also see abs00ap 10866 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 10869	A complex number is zero iff its absolute value is zero. Deduction form of abs00 10868. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) = 0 <-> A = 0 ) )
Theorem	abs00bd 10870	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 10871	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 10872	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 10873	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 10874	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 10875	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 10876	The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- ( abs ` 1 ) = 1
Theorem	absnid 10877	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 10878	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 10879	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 10880	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 10881	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|- ( A e. RR -> ( abs ` A ) = ( sqr ` ( A ^ 2 ) ) )
Theorem	absresq 10882	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 10883	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 10884	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 10885	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 10886	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 10887	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 10888	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 10889	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 10890	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 10891	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 10892	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 10893	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 10894	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 10895	If the absolute value of a complex number is less than a real, its difference from the real is nonzero. See also abssubap0 10894 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 10896	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 10897	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 10898	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 10899	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 10900	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 ) )