Type  Label  Description 
Statement 

Theorem  sqrt0rlem 10401 
Lemma for sqrt0 10402. (Contributed by Jim Kingdon, 26Aug2020.)



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



Theorem  resqrexlem1arp 10403 
Lemma for resqrex 10424. is a positive real
(expressed in a way
that will help apply seqf 9845 and similar theorems). (Contributed by
Jim Kingdon, 28Jul2021.) (Revised by Jim Kingdon, 16Oct2022.)



Theorem  resqrexlemp1rp 10404* 
Lemma for resqrex 10424. Applying the recursion rule yields a
positive
real (expressed in a way that will help apply seqf 9845
and similar
theorems). (Contributed by Jim Kingdon, 28Jul2021.) (Revised by
Jim Kingdon, 16Oct2022.)



Theorem  resqrexlemf 10405* 
Lemma for resqrex 10424. The sequence is a function. (Contributed
by
Mario Carneiro and Jim Kingdon, 27Jul2021.) (Revised by Jim
Kingdon, 16Oct2022.)



Theorem  resqrexlemf1 10406* 
Lemma for resqrex 10424. 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.)
(Revised by Jim Kingdon, 16Oct2022.)



Theorem  resqrexlemfp1 10407* 
Lemma for resqrex 10424. 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 10408* 
Lemma for resqrex 10424. Each element of the sequence is an
overestimate. (Contributed by Mario Carneiro and Jim Kingdon,
27Jul2021.)



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



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



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



Theorem  resqrexlemcalc1 10412* 
Lemma for resqrex 10424. Some of the calculations involved in
showing
that the sequence converges. (Contributed by Mario Carneiro and Jim
Kingdon, 29Jul2021.)



Theorem  resqrexlemcalc2 10413* 
Lemma for resqrex 10424. Some of the calculations involved in
showing
that the sequence converges. (Contributed by Mario Carneiro and Jim
Kingdon, 29Jul2021.)



Theorem  resqrexlemcalc3 10414* 
Lemma for resqrex 10424. Some of the calculations involved in
showing
that the sequence converges. (Contributed by Mario Carneiro and Jim
Kingdon, 29Jul2021.)



Theorem  resqrexlemnmsq 10415* 
Lemma for resqrex 10424. The difference between the squares of two
terms
of the sequence. (Contributed by Mario Carneiro and Jim Kingdon,
30Jul2021.)



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



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



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



Theorem  resqrexlemoverl 10419* 
Lemma for resqrex 10424. 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 10420* 
Lemma for resqrex 10424. The sequence formed by squaring each term
of
converges to .
(Contributed by Mario
Carneiro and Jim Kingdon, 8Aug2021.)



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



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



Theorem  resqrexlemex 10423* 
Lemma for resqrex 10424. Existence of square root given a sequence
which
converges to the square root. (Contributed by Mario Carneiro and Jim
Kingdon, 27Jul2021.)



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



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



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



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



Theorem  rersqrtthlem 10428 
Lemma for resqrtth 10429. (Contributed by Jim Kingdon, 10Aug2021.)



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



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



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



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



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



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



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



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

# # 

Theorem  sqrt11 10437 
The square root function is onetoone. Also see sqrt11ap 10436 which would
follow easily from this given excluded middle, but which is proved another
way without it. (Contributed by Scott Fenton, 11Jun2013.)



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  abscj 10450 
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 10451 
Square of value of absolute value function. (Contributed by NM,
16Jan2006.)



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



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



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



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



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



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



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



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

#


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

#
#


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

# # 

Theorem  abs00 10462 
The absolute value of a number is zero iff the number is zero. Also see
abs00ap 10460 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 10463 
A complex number is zero iff its absolute value is zero. Deduction form
of abs00 10462. (Contributed by David Moews, 28Feb2017.)



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



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



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



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



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

# 

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



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



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



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



Theorem  qabsor 10473 
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8Nov2021.)



Theorem  qabsord 10474 
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8Nov2021.)



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



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



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



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

#


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



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



Theorem  absrele 10481 
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 10482 
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 10483 
The absolute value of an integer is a nonnegative integer. (Contributed
by NM, 27Feb2005.)



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



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



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



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



Theorem  abssubap0 10488 
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 10489 
If the absolute value of a complex number is less than a real, its
difference from the real is nonzero. See also abssubap0 10488 which is the
same with not equal changed to apart. (Contributed by NM, 2Nov2007.)



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



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



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



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



Theorem  releabs 10494 
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 10495 
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13Aug2021.)

#


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



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

# 

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



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



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

