P. 133 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rexfiuz 13201*	Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- ( A e. Fin -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. A ph <-> A. n e. A E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )
Theorem	rexuz3 13202*	Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )
Theorem	rexanuz2 13203*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.)
|- Z = ( ZZ>= ` M )   =>    |- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) )
Theorem	r19.29uz 13204*	A version of 19.29 1698 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( A. k e. Z ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
Theorem	r19.2uz 13205*	A version of r19.2z 3847 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( E. j e. Z A. k e. ( ZZ>= ` j ) ph -> E. k e. Z ph )
Theorem	rexuzre 13206*	Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. RR A. k e. Z ( j <_ k -> ph ) ) )
Theorem	rexico 13207*	Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( ( A C_ RR /\ B e. RR ) -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) <-> E. j e. RR A. k e. A ( j <_ k -> ph ) ) )
Theorem	cau3lem 13208*	Lemma for cau3 13209. (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 13209*	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 13199 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 13210*	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 13211*	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	caubnd 13212*	A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 14-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( A. k e. Z ( F ` k ) e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. y e. RR A. k e. Z ( abs ` ( F ` k ) ) < y )
Theorem	sqreulem 13213	Lemma for sqreu 13214: write a general complex square root in terms of the square root function over nonnegative reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- B = ( ( sqr ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) )   =>    |- ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( ( B ^ 2 ) = A /\ 0 <_ ( Re ` B ) /\ ( _i x. B ) e/ RR+ ) )
Theorem	sqreu 13214*	Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( A e. CC -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
Theorem	sqrtcl 13215	Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( A e. CC -> ( sqr ` A ) e. CC )
Theorem	sqrtthlem 13216	Lemma for sqrtth 13218. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( A e. CC -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqr ` A ) ) /\ ( _i x. ( sqr ` A ) ) e/ RR+ ) )
Theorem	sqrtf 13217	Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.)
|- sqr : CC --> CC
Theorem	sqrtth 13218	Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( A e. CC -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	sqrtrege0 13219	The square root function must make a choice between the two roots, which differ by a sign change. In the general complex case, the choice of "positive" and "negative" is not so clear. The convention we use is to take the root with positive real part, unless A is a nonpositive real (in which case both roots have 0 real part); in this case we take the one in the positive imaginary direction. Another way to look at this is that we choose the root that is largest with respect to lexicographic order on the complex numbers (sorting by real part first, then by imaginary part as tie-breaker). (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( A e. CC -> 0 <_ ( Re ` ( sqr ` A ) ) )
Theorem	eqsqrtor 13220	Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = B <-> ( A = ( sqr ` B ) \/ A = -u ( sqr ` B ) ) ) )
Theorem	eqsqrtd 13221	A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A ^ 2 ) = B )   &    |- ( ph -> 0 <_ ( Re ` A ) )   &    |- ( ph -> -. ( _i x. A ) e. RR+ )   =>    |- ( ph -> A = ( sqr ` B ) )
Theorem	eqsqrt2d 13222	A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A ^ 2 ) = B )   &    |- ( ph -> 0 < ( Re ` A ) )   =>    |- ( ph -> A = ( sqr ` B ) )
Theorem	amgm2 13223	Arithmetic-geometric mean inequality for n = 2. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) <_ ( ( A + B ) / 2 ) )
Theorem	sqrtthi 13224	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 <_ A -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtcli 13225	The square root of a nonnegative real is a real. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` A ) e. RR )
Theorem	sqrtgt0i 13226	The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 < A -> 0 < ( sqr ` A ) )
Theorem	sqrtmsqi 13227	Square root of square. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrtsqi 13228	Square root of square. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqsqrti 13229	Square of square root. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	sqrtge0i 13230	The square root of a nonnegative real is nonnegative. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   =>    |- ( 0 <_ A -> 0 <_ ( sqr ` A ) )
Theorem	absidi 13231	A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( abs ` A ) = A )
Theorem	absnidi 13232	A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( A <_ 0 -> ( abs ` A ) = -u A )
Theorem	leabsi 13233	A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- A <_ ( abs ` A )
Theorem	absori 13234	The absolute value of a real number is either that number or its negative. (Contributed by NM, 30-Sep-1999.)
|- A e. RR   =>    |- ( ( abs ` A ) = A \/ ( abs ` A ) = -u A )
Theorem	absrei 13235	Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- ( abs ` A ) = ( sqr ` ( A ^ 2 ) )
Theorem	sqrtpclii 13236	The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   &    |- 0 < A   =>    |- ( sqr ` A ) e. RR
Theorem	sqrtgt0ii 13237	The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- A e. RR   &    |- 0 < A   =>    |- 0 < ( sqr ` A )
Theorem	sqrt11i 13238	The square root function is one-to-one. (Contributed by NM, 27-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) )
Theorem	sqrtmuli 13239	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) )
Theorem	sqrtmulii 13240	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 <_ A   &    |- 0 <_ B   =>    |- ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) )
Theorem	sqrtmsq2i 13241	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = B <-> A = ( B x. B ) ) )
Theorem	sqrtlei 13242	Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) )
Theorem	sqrtlti 13243	Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) )
Theorem	abslti 13244	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) )
Theorem	abslei 13245	Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) )
Theorem	absvalsqi 13246	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) )
Theorem	absvalsq2i 13247	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) )
Theorem	abscli 13248	Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` A ) e. RR
Theorem	absge0i 13249	Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- 0 <_ ( abs ` A )
Theorem	absval2i 13250	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	abs00i 13251	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   =>    |- ( ( abs ` A ) = 0 <-> A = 0 )
Theorem	absgt0i 13252	The absolute value of a nonzero number is positive. Remark in [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   =>    |- ( A =/= 0 <-> 0 < ( abs ` A ) )
Theorem	absnegi 13253	Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( abs ` -u A ) = ( abs ` A )
Theorem	abscji 13254	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( abs ` ( * ` A ) ) = ( abs ` A )
Theorem	releabsi 13255	The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Re ` A ) <_ ( abs ` A )
Theorem	abssubi 13256	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( abs ` ( A - B ) ) = ( abs ` ( B - A ) )
Theorem	absmuli 13257	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) )
Theorem	sqabsaddi 13258	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )
Theorem	sqabssubi 13259	Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )
Theorem	absdivzi 13260	Absolute value distributes over division. (Contributed by NM, 26-Mar-2005.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )
Theorem	abstrii 13261	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. This is Metamath 100 proof #91. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) )
Theorem	abs3difi 13262	Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) )
Theorem	abs3lemi 13263	Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. RR   =>    |- ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D )
Theorem	rpsqrtcld 13264	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( sqr ` A ) e. RR+ )
Theorem	sqrtgt0d 13265	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 < ( sqr ` A ) )
Theorem	absnidd 13266	A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A <_ 0 )   =>    |- ( ph -> ( abs ` A ) = -u A )
Theorem	leabsd 13267	A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ ( abs ` A ) )
Theorem	absord 13268	The absolute value of a real number is either that number or its negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )
Theorem	absred 13269	Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( abs ` A ) = ( sqr ` ( A ^ 2 ) ) )
Theorem	resqrtcld 13270	The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` A ) e. RR )
Theorem	sqrtmsqd 13271	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrtsqd 13272	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqrtge0d 13273	The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> 0 <_ ( sqr ` A ) )
Theorem	sqrtnegd 13274	The square root of a negative number. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( sqr ` -u A ) = ( _i x. ( sqr ` A ) ) )
Theorem	absidd 13275	A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( abs ` A ) = A )
Theorem	sqrtdivd 13276	Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) )
Theorem	sqrtmuld 13277	Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) )
Theorem	sqrtsq2d 13278	Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) )
Theorem	sqrtled 13279	Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) )
Theorem	sqrtltd 13280	Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) )
Theorem	sqr11d 13281	The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> ( sqr ` A ) = ( sqr ` B ) )   =>    |- ( ph -> A = B )
Theorem	absltd 13282	Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) ) )
Theorem	absled 13283	Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) )
Theorem	abssubge0d 13284	Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( B - A ) ) = ( B - A ) )
Theorem	abssuble0d 13285	Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( A - B ) ) = ( B - A ) )
Theorem	absdifltd 13286	The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) < C <-> ( ( B - C ) < A /\ A < ( B + C ) ) ) )
Theorem	absdifled 13287	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) <_ C <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )
Theorem	abscld 13288	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) e. RR )
Theorem	sqrtcld 13289	Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( sqr ` A ) e. CC )
Theorem	sqrtrege0d 13290	The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( Re ` ( sqr ` A ) ) )
Theorem	sqsqrtd 13291	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	msqsqrtd 13292	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqr00d 13293	A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( sqr ` A ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	absvalsqd 13294	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2d 13295	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	absge0d 13296	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( abs ` A ) )
Theorem	absval2d 13297	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
Theorem	abs00d 13298	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	absne0d 13299	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( abs ` A ) =/= 0 )
Theorem	absrpcld 13300	The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( abs ` A ) e. RR+ )