P. 153 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15201-15300   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-sqrt 15201*	Define a function whose value is the square root of a complex number. For example, (√‘25) = 5 (ex-sqrt 30383). Since (𝑦↑2) = 𝑥 iff (-𝑦↑2) = 𝑥, we ensure uniqueness by restricting the range to numbers with positive real part, or numbers with 0 real part and nonnegative imaginary part. A description can be found under "Principal square root of a complex number" at http://en.wikipedia.org/wiki/Square_root 30383. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15328 for its closure, sqrtval 15203 for its value, sqrtth 15331 and sqsqrti 15342 for its relationship to squares, and sqrt11i 15351 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)
⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
Definition	df-abs 15202	Define the function for the absolute value (modulus) of a complex number. See abscli 15362 for its closure and absval 15204 or absval2i 15364 for its value. For example, (abs‘-2) = 2 (ex-abs 30384). (Contributed by NM, 27-Jul-1999.)
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
Theorem	sqrtval 15203*	Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)))
Theorem	absval 15204	The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(𝐴 · (∗‘𝐴))))
Theorem	rennim 15205	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+)
Theorem	cnpart 15206	The specification of restriction to the right half-plane partitions the complex plane without 0 into two disjoint pieces, which are related by a reflection about the origin (under the map 𝑥 ↦ -𝑥). (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((0 ≤ (ℜ‘𝐴) ∧ (i · 𝐴) ∉ ℝ+) ↔ ¬ (0 ≤ (ℜ‘-𝐴) ∧ (i · -𝐴) ∉ ℝ+)))
Theorem	sqrt0 15207	The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (√‘0) = 0
Theorem	01sqrexlem1 15208*	Lemma for 01sqrex 15215. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1)
Theorem	01sqrexlem2 15209*	Lemma for 01sqrex 15215. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → 𝐴 ∈ 𝑆)
Theorem	01sqrexlem3 15210*	Lemma for 01sqrex 15215. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧))
Theorem	01sqrexlem4 15211*	Lemma for 01sqrex 15215. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1))
Theorem	01sqrexlem5 15212*	Lemma for 01sqrex 15215. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < )))
Theorem	01sqrexlem6 15213*	Lemma for 01sqrex 15215. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) ≤ 𝐴)
Theorem	01sqrexlem7 15214*	Lemma for 01sqrex 15215. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) = 𝐴)
Theorem	01sqrex 15215*	Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∃𝑥 ∈ ℝ+ (𝑥 ≤ 1 ∧ (𝑥↑2) = 𝐴))
Theorem	resqrex 15216*	Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴))
Theorem	sqrmo 15217*	Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.)
⊢ (𝐴 ∈ ℂ → ∃*𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
Theorem	resqreu 15218*	Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
Theorem	resqrtcl 15219	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
Theorem	resqrtthlem 15220	Lemma for resqrtth 15221. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+))
Theorem	resqrtth 15221	Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
Theorem	remsqsqrt 15222	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴)
Theorem	sqrtge0 15223	The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (√‘𝐴))
Theorem	sqrtgt0 15224	The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (√‘𝐴))
Theorem	sqrtmul 15225	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))
Theorem	sqrtle 15226	Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))
Theorem	sqrtlt 15227	Square root is strictly monotonic. Closed form of sqrtlti 15356. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))
Theorem	sqrt11 15228	The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	sqrt00 15229	A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	rpsqrtcl 15230	The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.)
⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+)
Theorem	sqrtdiv 15231	Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵)))
Theorem	sqrtneglem 15232	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((i · (√‘𝐴))↑2) = -𝐴 ∧ 0 ≤ (ℜ‘(i · (√‘𝐴))) ∧ (i · (i · (√‘𝐴))) ∉ ℝ+))
Theorem	sqrtneg 15233	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘-𝐴) = (i · (√‘𝐴)))
Theorem	sqrtsq2 15234	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2)))
Theorem	sqrtsq 15235	Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqrtmsq 15236	Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrt1 15237	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
⊢ (√‘1) = 1
Theorem	sqrt4 15238	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
⊢ (√‘4) = 2
Theorem	sqrt9 15239	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
⊢ (√‘9) = 3
Theorem	sqrt2gt1lt2 15240	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 < (√‘2) ∧ (√‘2) < 2)
Theorem	sqrtm1 15241	The imaginary unit is the square root of negative 1. A lot of people like to call this the "definition" of i, but the definition of √ df-sqrt 15201 has already been crafted with i being mentioned explicitly, and in any case it doesn't make too much sense to define a value based on a function evaluated outside its domain. A more appropriate view is to take ax-i2m1 11136 or i2 14167 as the "definition", and simply postulate the existence of a number satisfying this property. This is the approach we take here. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ i = (√‘-1)
Theorem	nn0sqeq1 15242	A natural number with square one is equal to one. (Contributed by Thierry Arnoux, 2-Feb-2020.) (Proof shortened by Thierry Arnoux, 6-Jun-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁↑2) = 1) → 𝑁 = 1)
Theorem	absneg 15243	Absolute value of the negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
Theorem	abscl 15244	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
Theorem	abscj 15245	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.)
⊢ (𝐴 ∈ ℂ → (abs‘(∗‘𝐴)) = (abs‘𝐴))
Theorem	absvalsq 15246	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
Theorem	absvalsq2 15247	Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	sqabsadd 15248	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 + 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) + (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))
Theorem	sqabssub 15249	Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))
Theorem	absval2 15250	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
Theorem	abs0 15251	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (abs‘0) = 0
Theorem	absi 15252	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (abs‘i) = 1
Theorem	absge0 15253	Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
Theorem	absrpcl 15254	The absolute value of a nonzero number is a positive real. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℝ+)
Theorem	abs00 15255	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, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	abs00ad 15256	A complex number is zero iff its absolute value is zero. Deduction form of abs00 15255. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	abs00bd 15257	If a complex number is zero, its absolute value is zero. Converse of abs00d 15415. One-way deduction form of abs00 15255. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = 0)
Theorem	absreimsq 15258	Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
Theorem	absreim 15259	Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴 + (i · 𝐵))) = (√‘((𝐴↑2) + (𝐵↑2))))
Theorem	absmul 15260	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.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵)))
Theorem	absdiv 15261	Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	absid 15262	A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = 𝐴)
Theorem	abs1 15263	The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.)
⊢ (abs‘1) = 1
Theorem	absnid 15264	For a negative number, its absolute value is its negation. (Contributed by NM, 27-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
Theorem	leabs 15265	A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴))
Theorem	absor 15266	The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))
Theorem	absre 15267	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2)))
Theorem	absresq 15268	Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
Theorem	absmod0 15269	𝐴 is divisible by 𝐵 iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ ((abs‘𝐴) mod 𝐵) = 0))
Theorem	absexp 15270	Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	absexpz 15271	Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	abssq 15272	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.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (abs‘(𝐴↑2)))
Theorem	sqabs 15273	The squares of two reals are equal iff their absolute values are equal. (Contributed by NM, 6-Mar-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴↑2) = (𝐵↑2) ↔ (abs‘𝐴) = (abs‘𝐵)))
Theorem	absrele 15274	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.)
⊢ (𝐴 ∈ ℂ → (abs‘(ℜ‘𝐴)) ≤ (abs‘𝐴))
Theorem	absimle 15275	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.)
⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) ≤ (abs‘𝐴))
Theorem	max0add 15276	The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Mario Carneiro, 24-Aug-2014.)
⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) + if(0 ≤ -𝐴, -𝐴, 0)) = (abs‘𝐴))
Theorem	absz 15277	A real number is an integer iff its absolute value is an integer. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (abs‘𝐴) ∈ ℤ))
Theorem	nn0abscl 15278	The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℕ0)
Theorem	zabscl 15279	The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ)
Theorem	zabs0b 15280	An integer has an absolute value less than 1 iff it is 0. (Contributed by AV, 21-Nov-2025.)
⊢ (𝑋 ∈ ℤ → ((abs‘𝑋) < 1 ↔ 𝑋 = 0))
Theorem	abslt 15281	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	absle 15282	Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)))
Theorem	abssubne0 15283	If the absolute value of a complex number is less than a real, its difference from the real is nonzero. (Contributed by NM, 2-Nov-2007.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ (abs‘𝐴) < 𝐵) → (𝐵 − 𝐴) ≠ 0)
Theorem	absdiflt 15284	The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶))))
Theorem	absdifle 15285	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶))))
Theorem	elicc4abs 15286	Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵))
Theorem	lenegsq 15287	Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2)))
Theorem	releabs 15288	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.)
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ≤ (abs‘𝐴))
Theorem	recval 15289	Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2)))
Theorem	absidm 15290	The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.)
⊢ (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴))
Theorem	absgt0 15291	The absolute value of a nonzero number is positive. (Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ 0 < (abs‘𝐴)))
Theorem	nnabscl 15292	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.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
Theorem	abssub 15293	Swapping order of subtraction doesn't change the absolute value. (Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴)))
Theorem	abssubge0 15294	Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴))
Theorem	abssuble0 15295	Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴))
Theorem	absmax 15296	The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))
Theorem	abstri 15297	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.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
Theorem	abs3dif 15298	Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))))
Theorem	abs2dif 15299	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs2dif2 15300	Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))