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
Theorem	sqrtneglem 15201	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((i · (√‘𝐴))↑2) = -𝐴 ∧ 0 ≤ (ℜ‘(i · (√‘𝐴))) ∧ (i · (i · (√‘𝐴))) ∉ ℝ+))
Theorem	sqrtneg 15202	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘-𝐴) = (i · (√‘𝐴)))
Theorem	sqrtsq2 15203	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2)))
Theorem	sqrtsq 15204	Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqrtmsq 15205	Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrt1 15206	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
⊢ (√‘1) = 1
Theorem	sqrt4 15207	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
⊢ (√‘4) = 2
Theorem	sqrt9 15208	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
⊢ (√‘9) = 3
Theorem	sqrt2gt1lt2 15209	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 15210	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 15170 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 11106 or i2 14137 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 15211	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 15212	Absolute value of the negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
Theorem	abscl 15213	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
Theorem	abscj 15214	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 15215	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
Theorem	absvalsq2 15216	Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	sqabsadd 15217	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 15218	Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))
Theorem	absval2 15219	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
Theorem	abs0 15220	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (abs‘0) = 0
Theorem	absi 15221	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (abs‘i) = 1
Theorem	absge0 15222	Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
Theorem	absrpcl 15223	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 15224	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 15225	A complex number is zero iff its absolute value is zero. Deduction form of abs00 15224. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	abs00bd 15226	If a complex number is zero, its absolute value is zero. Converse of abs00d 15384. One-way deduction form of abs00 15224. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = 0)
Theorem	absreimsq 15227	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 15228	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 15229	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 15230	Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	absid 15231	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 15232	The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.)
⊢ (abs‘1) = 1
Theorem	absnid 15233	For a negative number, its absolute value is its negation. (Contributed by NM, 27-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
Theorem	leabs 15234	A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴))
Theorem	absor 15235	The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))
Theorem	absre 15236	Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2)))
Theorem	absresq 15237	Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
Theorem	absmod0 15238	𝐴 is divisible by 𝐵 iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ ((abs‘𝐴) mod 𝐵) = 0))
Theorem	absexp 15239	Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	absexpz 15240	Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	abssq 15241	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 15242	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 15243	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 15244	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 15245	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 15246	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 15247	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 15248	The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ)
Theorem	zabs0b 15249	An integer has an absolute value less than 1 iff it is 0. (Contributed by AV, 21-Nov-2025.)
⊢ (𝑋 ∈ ℤ → ((abs‘𝑋) < 1 ↔ 𝑋 = 0))
Theorem	abslt 15250	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	absle 15251	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 15252	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 15253	The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶))))
Theorem	absdifle 15254	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶))))
Theorem	elicc4abs 15255	Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵))
Theorem	lenegsq 15256	Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2)))
Theorem	releabs 15257	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 15258	Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2)))
Theorem	absidm 15259	The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.)
⊢ (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴))
Theorem	absgt0 15260	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 15261	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 15262	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 15263	Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴))
Theorem	abssuble0 15264	Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴))
Theorem	absmax 15265	The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))
Theorem	abstri 15266	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 15267	Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))))
Theorem	abs2dif 15268	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs2dif2 15269	Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
Theorem	abs2difabs 15270	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs1m 15271*	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 15272*	Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∀𝑥 ∈ ℂ (ℜ‘(𝑥 · 𝐴)) = (ℜ‘(𝑥 · 𝐵)) ↔ 𝐴 = 𝐵))
Theorem	absf 15273	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 15274	Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ)) → (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷))
Theorem	abslem2 15275	Lemma involving absolute values. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (((∗‘(𝐴 / (abs‘𝐴))) · 𝐴) + ((𝐴 / (abs‘𝐴)) · (∗‘𝐴))) = (2 · (abs‘𝐴)))
Theorem	rddif 15276	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 15277	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 15278	Lemma for fzomaxdif 15279. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) ∈ (0..^(𝐷 − 𝐶)))
Theorem	fzomaxdif 15279	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 15280	The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥) → (𝐴 ∩ 𝐵) ∈ ran ℤ≥)
Theorem	rexanuz 15281*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.)
⊢ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
Theorem	rexanre 15282*	Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.)
⊢ (𝐴 ⊆ ℝ → (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (𝜑 ∧ 𝜓)) ↔ (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ∧ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜓))))
Theorem	rexfiuz 15283*	Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ (𝐴 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐴 𝜑 ↔ ∀𝑛 ∈ 𝐴 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑))
Theorem	rexuz3 15284*	Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑))
Theorem	rexanuz2 15285*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
Theorem	r19.29uz 15286*	A version of 19.29 1875 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((∀𝑘 ∈ 𝑍 𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓))
Theorem	r19.2uz 15287*	A version of r19.2z 4454 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∃𝑘 ∈ 𝑍 𝜑)
Theorem	rexuzre 15288*	Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑)))
Theorem	rexico 15289*	Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑)))
Theorem	cau3lem 15290*	Lemma for cau3 15291. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝑍 ⊆ ℤ    &   ⊢ (𝜏 → 𝜓)    &   ⊢ ((𝐹‘𝑘) = (𝐹‘𝑗) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝐹‘𝑘) = (𝐹‘𝑚) → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑘))) = (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))))    &   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → (𝐺‘((𝐹‘𝑚)𝐷(𝐹‘𝑗))) = (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))))    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝑥 ∈ ℝ)) → (((𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥)))
Theorem	cau3 15291*	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 15281 and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥))
Theorem	cau4 15292*	Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))
Theorem	caubnd2 15293*	A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑦)
Theorem	caubnd 15294*	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 15295	Lemma for sqreu 15296: 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 15296*	Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
Theorem	sqrtcl 15297	Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) ∈ ℂ)
Theorem	sqrtthlem 15298	Lemma for sqrtth 15300. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+))
Theorem	sqrtf 15299	Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ √:ℂ⟶ℂ
Theorem	sqrtth 15300	Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑2) = 𝐴)