P. 154 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15301-15400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	readdd 15301	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))
Theorem	imaddd 15302	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))
Theorem	resubd 15303	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))
Theorem	imsubd 15304	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))
Theorem	remuld 15305	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	immuld 15306	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))
Theorem	cjaddd 15307	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)))
Theorem	cjmuld 15308	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))
Theorem	ipcnd 15309	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))
Theorem	cjdivd 15310	Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	rered 15311	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴)
Theorem	reim0d 15312	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) = 0)
Theorem	cjred 15313	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) = 𝐴)
Theorem	remul2d 15314	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	immul2d 15315	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	redivd 15316	Real part of a division. Related to remul2 15217. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴))
Theorem	imdivd 15317	Imaginary part of a division. Related to remul2 15217. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴))
Theorem	crred 15318	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
Theorem	crimd 15319	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
5.9.4  Square root; absolute value
Syntax	csqrt 15320	Extend class notation to include square root of a complex number.
class √
Syntax	cabs 15321	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-sqrt 15322*	Define a function whose value is the square root of a complex number. For example, (√‘25) = 5 (ex-sqrt 30934). 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 30934. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15449 for its closure, sqrtval 15324 for its value, sqrtth 15452 and sqsqrti 15463 for its relationship to squares, and sqrt11i 15472 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)
⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
Definition	df-abs 15323	Define the function for the absolute value (modulus) of a complex number. See abscli 15483 for its closure and absval 15325 or absval2i 15485 for its value. For example, (abs‘-2) = 2 (ex-abs 30935). (Contributed by NM, 27-Jul-1999.)
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
Theorem	sqrtval 15324*	Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)))
Theorem	absval 15325	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 15326	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+)
Theorem	cnpart 15327	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 15328	The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (√‘0) = 0
Theorem	01sqrexlem1 15329*	Lemma for 01sqrex 15336. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1)
Theorem	01sqrexlem2 15330*	Lemma for 01sqrex 15336. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → 𝐴 ∈ 𝑆)
Theorem	01sqrexlem3 15331*	Lemma for 01sqrex 15336. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧))
Theorem	01sqrexlem4 15332*	Lemma for 01sqrex 15336. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1))
Theorem	01sqrexlem5 15333*	Lemma for 01sqrex 15336. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < )))
Theorem	01sqrexlem6 15334*	Lemma for 01sqrex 15336. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) ≤ 𝐴)
Theorem	01sqrexlem7 15335*	Lemma for 01sqrex 15336. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.)
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴}    &   ⊢ 𝐵 = sup(𝑆, ℝ, < )    &   ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)}    ⇒   ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) = 𝐴)
Theorem	01sqrex 15336*	Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∃𝑥 ∈ ℝ+ (𝑥 ≤ 1 ∧ (𝑥↑2) = 𝐴))
Theorem	resqrex 15337*	Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴))
Theorem	sqrmo 15338*	Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.)
⊢ (𝐴 ∈ ℂ → ∃*𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
Theorem	resqreu 15339*	Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
Theorem	resqrtcl 15340	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
Theorem	resqrtthlem 15341	Lemma for resqrtth 15342. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+))
Theorem	resqrtth 15342	Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
Theorem	remsqsqrt 15343	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴)
Theorem	sqrtge0 15344	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 15345	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 15346	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))
Theorem	sqrtle 15347	Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))
Theorem	sqrtlt 15348	Square root is strictly monotonic. Closed form of sqrtlti 15477. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))
Theorem	sqrt11 15349	The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	sqrt00 15350	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 15351	The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.)
⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+)
Theorem	sqrtdiv 15352	Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵)))
Theorem	sqrtneglem 15353	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((i · (√‘𝐴))↑2) = -𝐴 ∧ 0 ≤ (ℜ‘(i · (√‘𝐴))) ∧ (i · (i · (√‘𝐴))) ∉ ℝ+))
Theorem	sqrtneg 15354	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘-𝐴) = (i · (√‘𝐴)))
Theorem	sqrtsq2 15355	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2)))
Theorem	sqrtsq 15356	Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqrtmsq 15357	Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrt1 15358	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
⊢ (√‘1) = 1
Theorem	sqrt4 15359	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
⊢ (√‘4) = 2
Theorem	sqrt9 15360	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
⊢ (√‘9) = 3
Theorem	sqrt2gt1lt2 15361	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 15362	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 15322 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 11192 or i2 14266 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 15363	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 15364	Absolute value of the negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
Theorem	abscl 15365	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
Theorem	abscj 15366	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 15367	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
Theorem	absvalsq2 15368	Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	sqabsadd 15369	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 15370	Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))
Theorem	absval2 15371	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
Theorem	abs0 15372	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (abs‘0) = 0
Theorem	absi 15373	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (abs‘i) = 1
Theorem	absge0 15374	Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
Theorem	absrpcl 15375	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 15376	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 15377	A complex number is zero iff its absolute value is zero. Deduction form of abs00 15376. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	abs00bd 15378	If a complex number is zero, its absolute value is zero. Converse of abs00d 15536. One-way deduction form of abs00 15376. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = 0)
Theorem	absreimsq 15379	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 15380	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 15381	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 15382	Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	absid 15383	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 15384	The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.)
⊢ (abs‘1) = 1
Theorem	absnid 15385	For a negative number, its absolute value is its negation. (Contributed by NM, 27-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
Theorem	leabs 15386	A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴))
Theorem	absor 15387	The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))
Theorem	absre 15388	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2)))
Theorem	absresq 15389	Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
Theorem	absmod0 15390	𝐴 is divisible by 𝐵 iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ ((abs‘𝐴) mod 𝐵) = 0))
Theorem	absexp 15391	Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	absexpz 15392	Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	abssq 15393	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 15394	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 15395	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 15396	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 15397	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 15398	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 15399	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 15400	The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ)