P. 151 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	absvalsq 15001	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
Theorem	absvalsq2 15002	Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	sqabsadd 15003	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 15004	Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))
Theorem	absval2 15005	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
Theorem	abs0 15006	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (abs‘0) = 0
Theorem	absi 15007	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (abs‘i) = 1
Theorem	absge0 15008	Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
Theorem	absrpcl 15009	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 15010	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 15011	A complex number is zero iff its absolute value is zero. Deduction form of abs00 15010. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	abs00bd 15012	If a complex number is zero, its absolute value is zero. Converse of abs00d 15167. One-way deduction form of abs00 15010. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = 0)
Theorem	absreimsq 15013	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 15014	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 15015	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 15016	Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	absid 15017	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 15018	The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.)
⊢ (abs‘1) = 1
Theorem	absnid 15019	A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
Theorem	leabs 15020	A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴))
Theorem	absor 15021	The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))
Theorem	absre 15022	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2)))
Theorem	absresq 15023	Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
Theorem	absmod0 15024	𝐴 is divisible by 𝐵 iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ ((abs‘𝐴) mod 𝐵) = 0))
Theorem	absexp 15025	Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	absexpz 15026	Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	abssq 15027	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 15028	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 15029	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 15030	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 15031	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 15032	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 15033	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 15034	The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ)
Theorem	abslt 15035	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	absle 15036	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 15037	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 15038	The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶))))
Theorem	absdifle 15039	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶))))
Theorem	elicc4abs 15040	Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵))
Theorem	lenegsq 15041	Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2)))
Theorem	releabs 15042	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 15043	Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2)))
Theorem	absidm 15044	The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.)
⊢ (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴))
Theorem	absgt0 15045	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 15046	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 15047	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 15048	Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴))
Theorem	abssuble0 15049	Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴))
Theorem	absmax 15050	The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))
Theorem	abstri 15051	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 15052	Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))))
Theorem	abs2dif 15053	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs2dif2 15054	Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
Theorem	abs2difabs 15055	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs1m 15056*	For any complex number, there exists a unit-magnitude multiplier that produces its absolute value. Part of proof of Theorem 13-2.12 of [Gleason] p. 195. (Contributed by NM, 26-Mar-2005.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴)))
Theorem	recan 15057*	Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∀𝑥 ∈ ℂ (ℜ‘(𝑥 · 𝐴)) = (ℜ‘(𝑥 · 𝐵)) ↔ 𝐴 = 𝐵))
Theorem	absf 15058	Mapping domain and codomain of the absolute value function. (Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ abs:ℂ⟶ℝ
Theorem	abs3lem 15059	Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ)) → (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷))
Theorem	abslem2 15060	Lemma involving absolute values. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (((∗‘(𝐴 / (abs‘𝐴))) · 𝐴) + ((𝐴 / (abs‘𝐴)) · (∗‘𝐴))) = (2 · (abs‘𝐴)))
Theorem	rddif 15061	The difference between a real number and its nearest integer is less than or equal to one half. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Sep-2015.)
⊢ (𝐴 ∈ ℝ → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ (1 / 2))
Theorem	absrdbnd 15062	Bound on the absolute value of a real number rounded to the nearest integer. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Sep-2015.)
⊢ (𝐴 ∈ ℝ → (abs‘(⌊‘(𝐴 + (1 / 2)))) ≤ ((⌊‘(abs‘𝐴)) + 1))
Theorem	fzomaxdiflem 15063	Lemma for fzomaxdif 15064. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) ∈ (0..^(𝐷 − 𝐶)))
Theorem	fzomaxdif 15064	A bound on the separation of two points in a half-open range. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (abs‘(𝐴 − 𝐵)) ∈ (0..^(𝐷 − 𝐶)))
Theorem	uzin2 15065	The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥) → (𝐴 ∩ 𝐵) ∈ ran ℤ≥)
Theorem	rexanuz 15066*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.)
⊢ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
Theorem	rexanre 15067*	Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.)
⊢ (𝐴 ⊆ ℝ → (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (𝜑 ∧ 𝜓)) ↔ (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ∧ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜓))))
Theorem	rexfiuz 15068*	Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ (𝐴 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐴 𝜑 ↔ ∀𝑛 ∈ 𝐴 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑))
Theorem	rexuz3 15069*	Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑))
Theorem	rexanuz2 15070*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
Theorem	r19.29uz 15071*	A version of 19.29 1877 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((∀𝑘 ∈ 𝑍 𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓))
Theorem	r19.2uz 15072*	A version of r19.2z 4426 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∃𝑘 ∈ 𝑍 𝜑)
Theorem	rexuzre 15073*	Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑)))
Theorem	rexico 15074*	Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑)))
Theorem	cau3lem 15075*	Lemma for cau3 15076. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝑍 ⊆ ℤ    &   ⊢ (𝜏 → 𝜓)    &   ⊢ ((𝐹‘𝑘) = (𝐹‘𝑗) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝐹‘𝑘) = (𝐹‘𝑚) → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑘))) = (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))))    &   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → (𝐺‘((𝐹‘𝑚)𝐷(𝐹‘𝑗))) = (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))))    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝑥 ∈ ℝ)) → (((𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥)))
Theorem	cau3 15076*	Convert between three-quantifier and four-quantifier versions of the Cauchy criterion. (In particular, the four-quantifier version has no occurrence of 𝑗 in the assertion, so it can be used with rexanuz 15066 and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥))
Theorem	cau4 15077*	Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))
Theorem	caubnd2 15078*	A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑦)
Theorem	caubnd 15079*	A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 14-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)
Theorem	sqreulem 15080	Lemma for sqreu 15081: write a general complex square root in terms of the square root function over nonnegative reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ 𝐵 = ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝐵) ∧ (i · 𝐵) ∉ ℝ+))
Theorem	sqreu 15081*	Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
Theorem	sqrtcl 15082	Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) ∈ ℂ)
Theorem	sqrtthlem 15083	Lemma for sqrtth 15085. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+))
Theorem	sqrtf 15084	Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ √:ℂ⟶ℂ
Theorem	sqrtth 15085	Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑2) = 𝐴)
Theorem	sqrtrege0 15086	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 15087	Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) = 𝐵 ↔ (𝐴 = (√‘𝐵) ∨ 𝐴 = -(√‘𝐵))))
Theorem	eqsqrtd 15088	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 15089	A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴↑2) = 𝐵)    &   ⊢ (𝜑 → 0 < (ℜ‘𝐴))    ⇒   ⊢ (𝜑 → 𝐴 = (√‘𝐵))
Theorem	amgm2 15090	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 15091	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 15092	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 15093	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 15094	Square root of square. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrtsqi 15095	Square root of square. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqsqrti 15096	Square of square root. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → ((√‘𝐴)↑2) = 𝐴)
Theorem	sqrtge0i 15097	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 15098	A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 ≤ 𝐴 → (abs‘𝐴) = 𝐴)
Theorem	absnidi 15099	A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 0 → (abs‘𝐴) = -𝐴)
Theorem	leabsi 15100	A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ≤ (abs‘𝐴)