P. 120 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sqrtmuli 11901	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))
Theorem	sqrtmulii 11902	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 ≤ 𝐴    &   ⊢ 0 ≤ 𝐵    ⇒   ⊢ (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))
Theorem	sqrtmsq2i 11903	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐵)))
Theorem	sqrtlei 11904	Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))
Theorem	sqrtlti 11905	Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))
Theorem	abslti 11906	Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))
Theorem	abslei 11907	Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))
Theorem	absvalsqi 11908	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))
Theorem	absvalsq2i 11909	Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))
Theorem	abscli 11910	Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (abs‘𝐴) ∈ ℝ
Theorem	absge0i 11911	Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ 0 ≤ (abs‘𝐴)
Theorem	absval2i 11912	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	abs00i 11913	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	absgt0api 11914	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 11915	Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (abs‘-𝐴) = (abs‘𝐴)
Theorem	abscji 11916	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 11917	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 11918	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 11919	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 11920	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 11921	Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵)))))
Theorem	absdivapzi 11922	Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	abstrii 11923	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 11924	Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))
Theorem	abs3lemi 11925	Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷)
Theorem	rpsqrtcld 11926	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (√‘𝐴) ∈ ℝ+)
Theorem	sqrtgt0d 11927	The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 < (√‘𝐴))
Theorem	absnidd 11928	A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = -𝐴)
Theorem	leabsd 11929	A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (abs‘𝐴))
Theorem	absred 11930	Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = (√‘(𝐴↑2)))
Theorem	resqrtcld 11931	The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (√‘𝐴) ∈ ℝ)
Theorem	sqrtmsqd 11932	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrtsqd 11933	Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqrtge0d 11934	The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ (√‘𝐴))
Theorem	absidd 11935	A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = 𝐴)
Theorem	sqrtdivd 11936	Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵)))
Theorem	sqrtmuld 11937	Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))
Theorem	sqrtsq2d 11938	Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2)))
Theorem	sqrtled 11939	Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))
Theorem	sqrtltd 11940	Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))
Theorem	sqr11d 11941	The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → (√‘𝐴) = (√‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	absltd 11942	Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	absled 11943	Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)))
Theorem	abssubge0d 11944	Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴))
Theorem	abssuble0d 11945	Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴))
Theorem	absdifltd 11946	The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶))))
Theorem	absdifled 11947	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶))))
Theorem	icodiamlt 11948	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 11949	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)
Theorem	absvalsqd 11950	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
Theorem	absvalsq2d 11951	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	absge0d 11952	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → 0 ≤ (abs‘𝐴))
Theorem	absval2d 11953	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
Theorem	abs00d 11954	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 11955	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	absrpclapd 11956	The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ+)
Theorem	absnegd 11957	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘-𝐴) = (abs‘𝐴))
Theorem	abscjd 11958	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 11959	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 11960	Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))
Theorem	abssubd 11961	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 11962	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	absdivapd 11963	Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))
Theorem	abstrid 11964	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 11965	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs2dif2d 11966	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)))
Theorem	abs2difabsd 11967	Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵)))
Theorem	abs3difd 11968	Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))))
Theorem	abs3lemd 11969	Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < (𝐷 / 2))    &   ⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) < (𝐷 / 2))    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < 𝐷)
Theorem	qdenre 11970*	The rational numbers are dense in ℝ: any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 10693. (Contributed by BJ, 15-Oct-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (abs‘(𝑥 − 𝐴)) < 𝐵)
4.8.5  The maximum of two real numbers
Theorem	maxcom 11971	The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ sup({𝐴, 𝐵}, ℝ, < ) = sup({𝐵, 𝐴}, ℝ, < )
Theorem	maxabsle 11972	An upper bound for {𝐴, 𝐵}. (Contributed by Jim Kingdon, 20-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))
Theorem	maxleim 11973	Value of maximum when we know which number is larger. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
Theorem	maxabslemab 11974	Lemma for maxabs 11977. A variation of maxleim 11973- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) = 𝐵)
Theorem	maxabslemlub 11975	Lemma for maxabs 11977. A least upper bound for {𝐴, 𝐵}. (Contributed by Jim Kingdon, 20-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
Theorem	maxabslemval 11976*	Lemma for maxabs 11977. Value of the supremum. (Contributed by Jim Kingdon, 22-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) ∈ ℝ ∧ ∀𝑥 ∈ {𝐴, 𝐵} ¬ (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2) → ∃𝑧 ∈ {𝐴, 𝐵}𝑥 < 𝑧)))
Theorem	maxabs 11977	Maximum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 20-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2))
Theorem	maxcl 11978	The maximum of two real numbers is a real number. (Contributed by Jim Kingdon, 22-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℝ)
Theorem	maxle1 11979	The maximum of two reals is no smaller than the first real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ, < ))
Theorem	maxle2 11980	The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ, < ))
Theorem	maxleast 11981	The maximum of two reals is a least upper bound. Lemma 3.11 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 22-Dec-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)) → sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶)
Theorem	maxleastb 11982	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)))
Theorem	maxleastlt 11983	The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐶 < sup({𝐴, 𝐵}, ℝ, < ))) → (𝐶 < 𝐴 ∨ 𝐶 < 𝐵))
Theorem	maxleb 11984	Equivalence of ≤ and being equal to the maximum of two reals. Lemma 3.12 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
Theorem	dfabsmax 11985	Absolute value of a real number in terms of maximum. Definition 3.13 of [Geuvers], p. 11. (Contributed by BJ and Jim Kingdon, 21-Dec-2021.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = sup({𝐴, -𝐴}, ℝ, < ))
Theorem	maxltsup 11986	Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	max0addsup 11987	The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)
⊢ (𝐴 ∈ ℝ → (sup({𝐴, 0}, ℝ, < ) + sup({-𝐴, 0}, ℝ, < )) = (abs‘𝐴))
Theorem	rexanre 11988*	Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.)
⊢ (𝐴 ⊆ ℝ → (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (𝜑 ∧ 𝜓)) ↔ (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ∧ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜓))))
Theorem	rexico 11989*	Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑)))
Theorem	maxclpr 11990	The maximum of two real numbers is one of those numbers if and only if dichotomy (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴) holds. For example, this can be combined with zletric 9690 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 1-Feb-2022.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) ∈ {𝐴, 𝐵} ↔ (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)))
Theorem	rpmaxcl 11991	The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℝ+)
Theorem	zmaxcl 11992	The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℤ)
Theorem	nn0maxcl 11993	The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℕ0)
Theorem	2zsupmax 11994	Two ways to express the maximum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 22-Jan-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	fimaxre2 11995*	A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
Theorem	negfi 11996*	The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∈ Fin)
4.8.6  The minimum of two real numbers
Theorem	mincom 11997	The minimum of two reals is commutative. (Contributed by Jim Kingdon, 8-Feb-2021.)
⊢ inf({𝐴, 𝐵}, ℝ, < ) = inf({𝐵, 𝐴}, ℝ, < )
Theorem	minmax 11998	Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 8-Feb-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) = -sup({-𝐴, -𝐵}, ℝ, < ))
Theorem	mincl 11999	The minumum of two real numbers is a real number. (Contributed by Jim Kingdon, 25-Apr-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) ∈ ℝ)
Theorem	min1inf 12000	The minimum of two numbers is less than or equal to the first. (Contributed by Jim Kingdon, 8-Feb-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → inf({𝐴, 𝐵}, ℝ, < ) ≤ 𝐴)