P. 155 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15401-15500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sqrtthlem 15401	Lemma for sqrtth 15403. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+))
Theorem	sqrtf 15402	Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ √:ℂ⟶ℂ
Theorem	sqrtth 15403	Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑2) = 𝐴)
Theorem	sqrtrege0 15404	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 𝐴 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.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘(√‘𝐴)))
Theorem	eqsqrtor 15405	Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) = 𝐵 ↔ (𝐴 = (√‘𝐵) ∨ 𝐴 = -(√‘𝐵))))
Theorem	eqsqrtd 15406	A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴↑2) = 𝐵)    &   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐴))    &   ⊢ (𝜑 → ¬ (i · 𝐴) ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 = (√‘𝐵))
Theorem	eqsqrt2d 15407	A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴↑2) = 𝐵)    &   ⊢ (𝜑 → 0 < (ℜ‘𝐴))    ⇒   ⊢ (𝜑 → 𝐴 = (√‘𝐵))
Theorem	amgm2 15408	Arithmetic-geometric mean inequality for 𝑛 = 2. (Contributed by Mario Carneiro, 2-Jul-2014.) (Proof shortened by AV, 9-Jul-2022.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵) / 2))
Theorem	sqrtthi 15409	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → ((√‘𝐴) · (√‘𝐴)) = 𝐴)
Theorem	sqrtcli 15410	The square root of a nonnegative real is a real. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → (√‘𝐴) ∈ ℝ)
Theorem	sqrtgt0i 15411	The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 → 0 < (√‘𝐴))
Theorem	sqrtmsqi 15412	Square root of square. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrtsqi 15413	Square root of square. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqsqrti 15414	Square of square root. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → ((√‘𝐴)↑2) = 𝐴)
Theorem	sqrtge0i 15415	The square root of a nonnegative real is nonnegative. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → 0 ≤ (√‘𝐴))
Theorem	absidi 15416	A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → (abs‘𝐴) = 𝐴)
Theorem	absnidi 15417	A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 0 → (abs‘𝐴) = -𝐴)
Theorem	leabsi 15418	A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ≤ (abs‘𝐴)
Theorem	absori 15419	The absolute value of a real number is either that number or its negative. (Contributed by NM, 30-Sep-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴)
Theorem	absrei 15420	Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (abs‘𝐴) = (√‘(𝐴↑2))
Theorem	sqrtpclii 15421	The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ (√‘𝐴) ∈ ℝ
Theorem	sqrtgt0ii 15422	The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 0 < (√‘𝐴)
Theorem	sqrt11i 15423	The square root function is one-to-one. (Contributed by NM, 27-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	sqrtmuli 15424	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))
Theorem	sqrtmulii 15425	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 ≤ 𝐴    &   ⊢ 0 ≤ 𝐵    ⇒   ⊢ (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))
Theorem	sqrtmsq2i 15426	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐵)))
Theorem	sqrtlei 15427	Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))
Theorem	sqrtlti 15428	Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))
Theorem	abslti 15429	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))
Theorem	abslei 15430	Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))
Theorem	cnsqrt00 15431	A square root of a complex number is zero iff its argument is 0. Version of sqrt00 15302 for complex numbers. (Contributed by AV, 26-Jan-2023.)
⊢ (𝐴 ∈ ℂ → ((√‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	absvalsqi 15432	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))
Theorem	absvalsq2i 15433	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))
Theorem	abscli 15434	Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (abs‘𝐴) ∈ ℝ
Theorem	absge0i 15435	Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 0 ≤ (abs‘𝐴)
Theorem	absval2i 15436	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	abs00i 15437	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.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) = 0 ↔ 𝐴 = 0)
Theorem	absgt0i 15438	The absolute value of a nonzero number is positive. Remark in [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 ↔ 0 < (abs‘𝐴))
Theorem	absnegi 15439	Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (abs‘-𝐴) = (abs‘𝐴)
Theorem	abscji 15440	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.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (abs‘(∗‘𝐴)) = (abs‘𝐴)
Theorem	releabsi 15441	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.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (ℜ‘𝐴) ≤ (abs‘𝐴)
Theorem	abssubi 15442	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴))
Theorem	absmuli 15443	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵))
Theorem	sqabsaddi 15444	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘(𝐴 + 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) + (2 · (ℜ‘(𝐴 · (∗‘𝐵)))))
Theorem	sqabssubi 15445	Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵)))))
Theorem	absdivzi 15446	Absolute value distributes over division. (Contributed by NM, 26-Mar-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	abstrii 15447	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.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))
Theorem	abs3difi 15448	Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))
Theorem	abs3lemi 15449	Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷)
Theorem	rpsqrtcld 15450	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (√‘𝐴) ∈ ℝ+)
Theorem	sqrtgt0d 15451	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 < (√‘𝐴))
Theorem	absnidd 15452	A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = -𝐴)
Theorem	leabsd 15453	A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (abs‘𝐴))
Theorem	absord 15454	The absolute value of a real number is either that number or its negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))
Theorem	absred 15455	Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = (√‘(𝐴↑2)))
Theorem	resqrtcld 15456	The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (√‘𝐴) ∈ ℝ)
Theorem	sqrtmsqd 15457	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrtsqd 15458	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqrtge0d 15459	The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ (√‘𝐴))
Theorem	sqrtnegd 15460	The square root of a negative number. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (√‘-𝐴) = (i · (√‘𝐴)))
Theorem	absidd 15461	A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = 𝐴)
Theorem	sqrtdivd 15462	Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵)))
Theorem	sqrtmuld 15463	Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))
Theorem	sqrtsq2d 15464	Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2)))
Theorem	sqrtled 15465	Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))
Theorem	sqrtltd 15466	Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))
Theorem	sqr11d 15467	The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → (√‘𝐴) = (√‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	absltd 15468	Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	absled 15469	Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)))
Theorem	abssubge0d 15470	Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴))
Theorem	abssuble0d 15471	Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴))
Theorem	absdifltd 15472	The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶))))
Theorem	absdifled 15473	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶))))
Theorem	icodiamlt 15474	Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ 𝐷 ∈ (𝐴[,)𝐵))) → (abs‘(𝐶 − 𝐷)) < (𝐵 − 𝐴))
Theorem	abscld 15475	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)
Theorem	sqrtcld 15476	Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (√‘𝐴) ∈ ℂ)
Theorem	sqrtrege0d 15477	The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 0 ≤ (ℜ‘(√‘𝐴)))
Theorem	sqsqrtd 15478	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((√‘𝐴)↑2) = 𝐴)
Theorem	msqsqrtd 15479	Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((√‘𝐴) · (√‘𝐴)) = 𝐴)
Theorem	sqr00d 15480	A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (√‘𝐴) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	absvalsqd 15481	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
Theorem	absvalsq2d 15482	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	absge0d 15483	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 0 ≤ (abs‘𝐴))
Theorem	absval2d 15484	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
Theorem	abs00d 15485	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.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐴) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	absne0d 15486	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.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) ≠ 0)
Theorem	absrpcld 15487	The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ+)
Theorem	absnegd 15488	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘-𝐴) = (abs‘𝐴))
Theorem	abscjd 15489	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(∗‘𝐴)) = (abs‘𝐴))
Theorem	releabsd 15490	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 Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) ≤ (abs‘𝐴))
Theorem	absexpd 15491	Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	abssubd 15492	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴)))
Theorem	absmuld 15493	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵)))
Theorem	absdivd 15494	Absolute value distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	abstrid 15495	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
Theorem	abs2difd 15496	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs2dif2d 15497	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
Theorem	abs2difabsd 15498	Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs3difd 15499	Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))))
Theorem	abs3lemd 15500	Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < (𝐷 / 2))    &   ⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) < (𝐷 / 2))    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < 𝐷)