P. 97 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9601-9700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sqrt0rlem 9601	Lemma for sqrt0 9602. (Contributed by Jim Kingdon, 26-Aug-2020.)
|- ( ( A e. RR /\ ( ( A ^ 2 ) = 0 /\ 0 <_ A ) ) <-> A = 0 )
Theorem	sqrt0 9602	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( sqr ` 0 ) = 0
Theorem	resqrexlem1arp 9603*	Lemma for resqrex 9624. 1 + A is a positive real (expressed in a way that will help apply iseqf 9224 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( NN X. { ( 1 + A ) } ) ` N ) e. RR+ )
Theorem	resqrexlemp1rp 9604*	Lemma for resqrex 9624. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqf 9224 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) , RR+ )   &    |- ( 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 9605*	Lemma for resqrex 9624. The sequence is a function. (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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> F : NN --> RR+ )
Theorem	resqrexlemf1 9606*	Lemma for resqrex 9624. 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.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( F ` 1 ) = ( 1 + A ) )
Theorem	resqrexlemfp1 9607*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( F ` ( N + 1 ) ) = ( ( ( F ` N ) + ( A / ( F ` N ) ) ) / 2 ) )
Theorem	resqrexlemover 9608*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> A < ( ( F ` N ) ^ 2 ) )
Theorem	resqrexlemdec 9609*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( F ` ( N + 1 ) ) < ( F ` N ) )
Theorem	resqrexlemdecn 9610*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9611*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( 1 / ( 2 ^ N ) ) < ( F ` N ) )
Theorem	resqrexlemcalc1 9612*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9613*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( ( F ` ( N + 1 ) ) ^ 2 ) - A ) <_ ( ( ( ( F ` N ) ^ 2 ) - A ) / 4 ) )
Theorem	resqrexlemcalc3 9614*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( ( F ` N ) ^ 2 ) - A ) <_ ( ( ( F ` 1 ) ^ 2 ) / ( 4 ^ ( N - 1 ) ) ) )
Theorem	resqrexlemnmsq 9615*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9616*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9617*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9618*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9619*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9620*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9621*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9622*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( 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 9623*	Lemma for resqrex 9624. 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 ) } ) , RR+ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
Theorem	resqrex 9624*	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 9625*	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 9626*	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 9627	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR )
Theorem	rersqrtthlem 9628	Lemma for resqrtth 9629. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( sqr ` A ) ) )
Theorem	resqrtth 9629	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 9630	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtge0 9631	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 9632	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 9633	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 9634	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 9635	Square root is strictly monotonic. Closed form of sqrtlti 9733. (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 9636	Analogue to sqrt11 9637 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 9637	The square root function is one-to-one. Also see sqrt11ap 9636 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 9638	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 9639	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 9640	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 9641	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 9642	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 9643	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 9644	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|- ( sqr ` 1 ) = 1
Theorem	sqrt4 9645	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|- ( sqr ` 4 ) = 2
Theorem	sqrt9 9646	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|- ( sqr ` 9 ) = 3
Theorem	sqrt2gt1lt2 9647	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 9648	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscl 9649	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|- ( A e. CC -> ( abs ` A ) e. RR )
Theorem	abscj 9650	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 9651	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2 9652	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 9653	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 9654	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 9655	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 9656	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( abs ` 0 ) = 0
Theorem	absi 9657	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( abs ` _i ) = 1
Theorem	absge0 9658	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 9659	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 9660	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 9661	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 9662	The absolute value of a number is zero iff the number is zero. Also see abs00ap 9660 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 9663	A complex number is zero iff its absolute value is zero. Deduction form of abs00 9662. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) = 0 <-> A = 0 ) )
Theorem	abs00bd 9664	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 9665	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 9666	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 9667	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 9668	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 9669	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 9670	The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- ( abs ` 1 ) = 1
Theorem	absnid 9671	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 9672	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	absre 9673	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|- ( A e. RR -> ( abs ` A ) = ( sqr ` ( A ^ 2 ) ) )
Theorem	absresq 9674	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 9675	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 9676	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 9677	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 9678	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 9679	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 9680	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 9681	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 9682	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 9683	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 9684	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 9685	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 9686	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 9687	If the absolute value of a complex number is less than a real, its difference from the real is nonzero. See also abssubap0 9686 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 9688	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 9689	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 9690	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 9691	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 9692	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 9693	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 9694	The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.)
|- ( A e. CC -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
Theorem	absgt0ap 9695	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 9696	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 9697	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 9698	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 9699	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 9700	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 ) ) )