Type  Label  Description 
Statement 

Theorem  sqrt0rlem 9601 
Lemma for sqrt0 9602. (Contributed by Jim Kingdon, 26Aug2020.)



Theorem  sqrt0 9602 
Square root of zero. (Contributed by Mario Carneiro, 9Jul2013.)



Theorem  resqrexlem1arp 9603* 
Lemma for resqrex 9624. is a positive real
(expressed in a way
that will help apply iseqf 9224 and similar theorems). (Contributed by
Jim Kingdon, 28Jul2021.)



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, 28Jul2021.)



Theorem  resqrexlemf 9605* 
Lemma for resqrex 9624. The sequence is a function. (Contributed
by
Mario Carneiro and Jim Kingdon, 27Jul2021.)



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, 27Jul2021.)



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, 27Jul2021.)



Theorem  resqrexlemover 9608* 
Lemma for resqrex 9624. Each element of the sequence is an
overestimate. (Contributed by Mario Carneiro and Jim Kingdon,
27Jul2021.)



Theorem  resqrexlemdec 9609* 
Lemma for resqrex 9624. The sequence is decreasing. (Contributed
by
Mario Carneiro and Jim Kingdon, 29Jul2021.)



Theorem  resqrexlemdecn 9610* 
Lemma for resqrex 9624. The sequence is decreasing. (Contributed
by
Jim Kingdon, 31Jul2021.)



Theorem  resqrexlemlo 9611* 
Lemma for resqrex 9624. A (variable) lower bound for each term of
the
sequence. (Contributed by Mario Carneiro and Jim Kingdon,
29Jul2021.)



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, 29Jul2021.)



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, 29Jul2021.)



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, 29Jul2021.)



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,
30Jul2021.)



Theorem  resqrexlemnm 9616* 
Lemma for resqrex 9624. The difference between two terms of the
sequence. (Contributed by Mario Carneiro and Jim Kingdon,
31Jul2021.)



Theorem  resqrexlemcvg 9617* 
Lemma for resqrex 9624. The sequence has a limit. (Contributed by
Jim
Kingdon, 6Aug2021.)



Theorem  resqrexlemgt0 9618* 
Lemma for resqrex 9624. A limit is nonnegative. (Contributed by
Jim
Kingdon, 7Aug2021.)



Theorem  resqrexlemoverl 9619* 
Lemma for resqrex 9624. Every term in the sequence is an
overestimate
compared with the limit . 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,
9Aug2021.)



Theorem  resqrexlemglsq 9620* 
Lemma for resqrex 9624. The sequence formed by squaring each term
of
converges to .
(Contributed by Mario
Carneiro and Jim Kingdon, 8Aug2021.)



Theorem  resqrexlemga 9621* 
Lemma for resqrex 9624. The sequence formed by squaring each term
of
converges to .
(Contributed by Mario Carneiro and
Jim Kingdon, 8Aug2021.)



Theorem  resqrexlemsqa 9622* 
Lemma for resqrex 9624. The square of a limit is .
(Contributed by Jim Kingdon, 7Aug2021.)



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, 27Jul2021.)



Theorem  resqrex 9624* 
Existence of a square root for positive reals. (Contributed by Mario
Carneiro, 9Jul2013.)



Theorem  rsqrmo 9625* 
Uniqueness for the square root function. (Contributed by Jim Kingdon,
10Aug2021.)



Theorem  rersqreu 9626* 
Existence and uniqueness for the real square root function.
(Contributed by Jim Kingdon, 10Aug2021.)



Theorem  resqrtcl 9627 
Closure of the square root function. (Contributed by Mario Carneiro,
9Jul2013.)



Theorem  rersqrtthlem 9628 
Lemma for resqrtth 9629. (Contributed by Jim Kingdon, 10Aug2021.)



Theorem  resqrtth 9629 
Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29.
(Contributed by Mario Carneiro, 9Jul2013.)



Theorem  remsqsqrt 9630 
Square of square root. (Contributed by Mario Carneiro, 10Jul2013.)



Theorem  sqrtge0 9631 
The square root function is nonnegative for nonnegative input.
(Contributed by NM, 26May1999.) (Revised by Mario Carneiro,
9Jul2013.)



Theorem  sqrtgt0 9632 
The square root function is positive for positive input. (Contributed by
Mario Carneiro, 10Jul2013.) (Revised by Mario Carneiro, 6Sep2013.)



Theorem  sqrtmul 9633 
Square root distributes over multiplication. (Contributed by NM,
30Jul1999.) (Revised by Mario Carneiro, 29May2016.)



Theorem  sqrtle 9634 
Square root is monotonic. (Contributed by NM, 17Mar2005.) (Proof
shortened by Mario Carneiro, 29May2016.)



Theorem  sqrtlt 9635 
Square root is strictly monotonic. Closed form of sqrtlti 9733.
(Contributed by Scott Fenton, 17Apr2014.) (Proof shortened by Mario
Carneiro, 29May2016.)



Theorem  sqrt11ap 9636 
Analogue to sqrt11 9637 but for apartness. (Contributed by Jim
Kingdon,
11Aug2021.)

# # 

Theorem  sqrt11 9637 
The square root function is onetoone. 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, 11Jun2013.)



Theorem  sqrt00 9638 
A square root is zero iff its argument is 0. (Contributed by NM,
27Jul1999.) (Proof shortened by Mario Carneiro, 29May2016.)



Theorem  rpsqrtcl 9639 
The square root of a positive real is a positive real. (Contributed by
NM, 22Feb2008.)



Theorem  sqrtdiv 9640 
Square root distributes over division. (Contributed by Mario Carneiro,
5May2016.)



Theorem  sqrtsq2 9641 
Relationship between square root and squares. (Contributed by NM,
31Jul1999.) (Revised by Mario Carneiro, 29May2016.)



Theorem  sqrtsq 9642 
Square root of square. (Contributed by NM, 14Jan2006.) (Revised by
Mario Carneiro, 29May2016.)



Theorem  sqrtmsq 9643 
Square root of square. (Contributed by NM, 2Aug1999.) (Revised by
Mario Carneiro, 29May2016.)



Theorem  sqrt1 9644 
The square root of 1 is 1. (Contributed by NM, 31Jul1999.)



Theorem  sqrt4 9645 
The square root of 4 is 2. (Contributed by NM, 3Aug1999.)



Theorem  sqrt9 9646 
The square root of 9 is 3. (Contributed by NM, 11May2004.)



Theorem  sqrt2gt1lt2 9647 
The square root of 2 is bounded by 1 and 2. (Contributed by Roy F.
Longton, 8Aug2005.) (Revised by Mario Carneiro, 6Sep2013.)



Theorem  absneg 9648 
Absolute value of negative. (Contributed by NM, 27Feb2005.)



Theorem  abscl 9649 
Real closure of absolute value. (Contributed by NM, 3Oct1999.)



Theorem  abscj 9650 
The absolute value of a number and its conjugate are the same.
Proposition 103.7(b) of [Gleason] p. 133.
(Contributed by NM,
28Apr2005.)



Theorem  absvalsq 9651 
Square of value of absolute value function. (Contributed by NM,
16Jan2006.)



Theorem  absvalsq2 9652 
Square of value of absolute value function. (Contributed by NM,
1Feb2007.)



Theorem  sqabsadd 9653 
Square of absolute value of sum. Proposition 103.7(g) of [Gleason]
p. 133. (Contributed by NM, 21Jan2007.)



Theorem  sqabssub 9654 
Square of absolute value of difference. (Contributed by NM,
21Jan2007.)



Theorem  absval2 9655 
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 17Mar2005.)



Theorem  abs0 9656 
The absolute value of 0. (Contributed by NM, 26Mar2005.) (Revised by
Mario Carneiro, 29May2016.)



Theorem  absi 9657 
The absolute value of the imaginary unit. (Contributed by NM,
26Mar2005.)



Theorem  absge0 9658 
Absolute value is nonnegative. (Contributed by NM, 20Nov2004.)
(Revised by Mario Carneiro, 29May2016.)



Theorem  absrpclap 9659 
The absolute value of a number apart from zero is a positive real.
(Contributed by Jim Kingdon, 11Aug2021.)

#


Theorem  abs00ap 9660 
The absolute value of a number is apart from zero iff the number is apart
from zero. (Contributed by Jim Kingdon, 11Aug2021.)

#
#


Theorem  absext 9661 
Strong extensionality for absolute value. (Contributed by Jim Kingdon,
12Aug2021.)

# # 

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 103.7(c) of
[Gleason] p. 133. (Contributed by NM,
26Sep2005.) (Proof shortened by
Mario Carneiro, 29May2016.)



Theorem  abs00ad 9663 
A complex number is zero iff its absolute value is zero. Deduction form
of abs00 9662. (Contributed by David Moews, 28Feb2017.)



Theorem  abs00bd 9664 
If a complex number is zero, its absolute value is zero. (Contributed
by David Moews, 28Feb2017.)



Theorem  absreimsq 9665 
Square of the absolute value of a number that has been decomposed into
real and imaginary parts. (Contributed by NM, 1Feb2007.)



Theorem  absreim 9666 
Absolute value of a number that has been decomposed into real and
imaginary parts. (Contributed by NM, 14Jan2006.)



Theorem  absmul 9667 
Absolute value distributes over multiplication. Proposition 103.7(f) of
[Gleason] p. 133. (Contributed by NM,
11Oct1999.) (Revised by Mario
Carneiro, 29May2016.)



Theorem  absdivap 9668 
Absolute value distributes over division. (Contributed by Jim Kingdon,
11Aug2021.)

# 

Theorem  absid 9669 
A nonnegative number is its own absolute value. (Contributed by NM,
11Oct1999.) (Revised by Mario Carneiro, 29May2016.)



Theorem  abs1 9670 
The absolute value of 1. Common special case. (Contributed by David A.
Wheeler, 16Jul2016.)



Theorem  absnid 9671 
A negative number is the negative of its own absolute value. (Contributed
by NM, 27Feb2005.)



Theorem  leabs 9672 
A real number is less than or equal to its absolute value. (Contributed
by NM, 27Feb2005.)



Theorem  absre 9673 
Absolute value of a real number. (Contributed by NM, 17Mar2005.)



Theorem  absresq 9674 
Square of the absolute value of a real number. (Contributed by NM,
16Jan2006.)



Theorem  absexp 9675 
Absolute value of positive integer exponentiation. (Contributed by NM,
5Jan2006.)



Theorem  absexpzap 9676 
Absolute value of integer exponentiation. (Contributed by Jim Kingdon,
11Aug2021.)

#


Theorem  abssq 9677 
Square can be moved in and out of absolute value. (Contributed by Scott
Fenton, 18Apr2014.) (Proof shortened by Mario Carneiro,
29May2016.)



Theorem  sqabs 9678 
The squares of two reals are equal iff their absolute values are equal.
(Contributed by NM, 6Mar2009.)



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, 1Apr2005.)



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, 17Mar2005.)
(Proof shortened by Mario Carneiro, 29May2016.)



Theorem  nn0abscl 9681 
The absolute value of an integer is a nonnegative integer. (Contributed
by NM, 27Feb2005.)



Theorem  zabscl 9682 
The absolute value of an integer is an integer. (Contributed by Stefan
O'Rear, 24Sep2014.)



Theorem  ltabs 9683 
A number which is less than its absolute value is negative. (Contributed
by Jim Kingdon, 12Aug2021.)



Theorem  abslt 9684 
Absolute value and 'less than' relation. (Contributed by NM, 6Apr2005.)
(Revised by Mario Carneiro, 29May2016.)



Theorem  absle 9685 
Absolute value and 'less than or equal to' relation. (Contributed by NM,
6Apr2005.) (Revised by Mario Carneiro, 29May2016.)



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,
12Aug2021.)

# 

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, 2Nov2007.)



Theorem  absdiflt 9688 
The absolute value of a difference and 'less than' relation. (Contributed
by Paul Chapman, 18Sep2007.)



Theorem  absdifle 9689 
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Paul Chapman, 18Sep2007.)



Theorem  elicc4abs 9690 
Membership in a symmetric closed real interval. (Contributed by Stefan
O'Rear, 16Nov2014.)



Theorem  lenegsq 9691 
Comparison to a nonnegative number based on comparison to squares.
(Contributed by NM, 16Jan2006.)



Theorem  releabs 9692 
The real part of a number is less than or equal to its absolute value.
Proposition 103.7(d) of [Gleason] p. 133.
(Contributed by NM,
1Apr2005.)



Theorem  recvalap 9693 
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13Aug2021.)

#


Theorem  absidm 9694 
The absolute value function is idempotent. (Contributed by NM,
20Nov2004.)



Theorem  absgt0ap 9695 
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13Aug2021.)

# 

Theorem  nnabscl 9696 
The absolute value of a nonzero integer is a positive integer.
(Contributed by Paul Chapman, 21Mar2011.) (Proof shortened by Andrew
Salmon, 25May2011.)



Theorem  abssub 9697 
Swapping order of subtraction doesn't change the absolute value.
(Contributed by NM, 1Oct1999.) (Proof shortened by Mario Carneiro,
29May2016.)



Theorem  abssubge0 9698 
Absolute value of a nonnegative difference. (Contributed by NM,
14Feb2008.)



Theorem  abssuble0 9699 
Absolute value of a nonpositive difference. (Contributed by FL,
3Jan2008.)



Theorem  abstri 9700 
Triangle inequality for absolute value. Proposition 103.7(h) of
[Gleason] p. 133. (Contributed by NM,
7Mar2005.) (Proof shortened by
Mario Carneiro, 29May2016.)

