P. 111 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11001-11100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sqrtlt 11001	Square root is strictly monotonic. Closed form of sqrtlti 11101. (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 11002	Analogue to sqrt11 11003 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 11003	The square root function is one-to-one. Also see sqrt11ap 11002 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 11004	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 11005	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 11006	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 11007	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 11008	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 11009	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 11010	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|- ( sqr ` 1 ) = 1
Theorem	sqrt4 11011	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|- ( sqr ` 4 ) = 2
Theorem	sqrt9 11012	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|- ( sqr ` 9 ) = 3
Theorem	sqrt2gt1lt2 11013	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 11014	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscl 11015	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|- ( A e. CC -> ( abs ` A ) e. RR )
Theorem	abscj 11016	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 11017	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2 11018	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 11019	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 11020	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 11021	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 11022	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( abs ` 0 ) = 0
Theorem	absi 11023	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( abs ` _i ) = 1
Theorem	absge0 11024	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 11025	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 11026	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 11027	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 11028	The absolute value of a number is zero iff the number is zero. Also see abs00ap 11026 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 11029	A complex number is zero iff its absolute value is zero. Deduction form of abs00 11028. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) = 0 <-> A = 0 ) )
Theorem	abs00bd 11030	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 11031	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 11032	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 11033	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 11034	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 11035	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 11036	The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- ( abs ` 1 ) = 1
Theorem	absnid 11037	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 11038	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 11039	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 11040	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 11041	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|- ( A e. RR -> ( abs ` A ) = ( sqr ` ( A ^ 2 ) ) )
Theorem	absresq 11042	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 11043	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 11044	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 11045	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 11046	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 11047	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 11048	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 11049	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 11050	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 11051	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 11052	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 11053	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 11054	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 11055	If the absolute value of a complex number is less than a real, its difference from the real is nonzero. See also abssubap0 11054 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 11056	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 11057	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 11058	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 11059	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 11060	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 11061	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 11062	The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.)
|- ( A e. CC -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
Theorem	absgt0ap 11063	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 11064	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 11065	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 11066	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 11067	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 11068	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by NM, 7-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs3dif 11069	Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
Theorem	abs2dif 11070	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs2dif2 11071	Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difabs 11072	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) )
Theorem	recan 11073*	Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( A. x e. CC ( Re ` ( x x. A ) ) = ( Re ` ( x x. B ) ) <-> A = B ) )
Theorem	absf 11074	Mapping domain and codomain of the absolute value function. (Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- abs : CC --> RR
Theorem	abs3lem 11075	Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) -> ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D ) )
Theorem	fzomaxdiflem 11076	Lemma for fzomaxdif 11077. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( ( A e. ( C..^ D ) /\ B e. ( C..^ D ) ) /\ A <_ B ) -> ( abs ` ( B - A ) ) e. ( 0..^ ( D - C ) ) )
Theorem	fzomaxdif 11077	A bound on the separation of two points in a half-open range. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( A e. ( C..^ D ) /\ B e. ( C..^ D ) ) -> ( abs ` ( A - B ) ) e. ( 0..^ ( D - C ) ) )
Theorem	cau3lem 11078*	Lemma for cau3 11079. (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 11079*	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 10952 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 11080*	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 11081*	A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. y e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( F ` k ) ) < y )
Theorem	amgm2 11082	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 11083	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 11084	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 11085	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 11086	Square root of square. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrtsqi 11087	Square root of square. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqsqrti 11088	Square of square root. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	sqrtge0i 11089	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 11090	A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   =>    |- ( 0 <_ A -> ( abs ` A ) = A )
Theorem	absnidi 11091	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 11092	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	absrei 11093	Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   =>    |- ( abs ` A ) = ( sqr ` ( A ^ 2 ) )
Theorem	sqrtpclii 11094	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 11095	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 11096	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 11097	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 11098	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 11099	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 11100	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 ) ) )