P. 256 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25501-25600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reust 25501	The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (UnifSt‘ℝfld) = (metUnif‘((dist‘ℝfld) ↾ (ℝ × ℝ)))
Theorem	recusp 25502	The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ ℝfld ∈ CUnifSp
12.5.8  Euclidean spaces
Syntax	crrx 25503	Extend class notation with generalized real Euclidean spaces.
class ℝ^
Syntax	cehl 25504	Extend class notation with real Euclidean spaces.
class 𝔼hil
Definition	df-rrx 25505	Define the function associating with a set the free real vector space on that set, equipped with the natural inner product and norm. This is the direct sum of copies of the field of real numbers indexed by that set. We call it here a "generalized real Euclidean space", but note that it need not be complete (for instance if the given set is infinite countable). (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ ℝ^ = (𝑖 ∈ V ↦ (toℂPreHil‘(ℝfld freeLMod 𝑖)))
Definition	df-ehl 25506	Define a function generating the real Euclidean spaces of finite dimension. The case 𝑛 = 0 corresponds to a space of dimension 0, that is, limited to a neutral element (see ehl0 25537). Members of this family of spaces are Hilbert spaces, as shown in - ehlhl . (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
Theorem	rrxval 25507	Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝfld freeLMod 𝐼)))
Theorem	rrxbase 25508*	The base of the generalized real Euclidean space is the set of functions with finite support. (Contributed by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {𝑓 ∈ (ℝ ↑m 𝐼) ∣ 𝑓 finSupp 0})
Theorem	rrxprds 25509	Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)})) ↾s 𝐵)))
Theorem	rrxip 25510*	The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) = (·𝑖‘𝐻))
Theorem	rrxnm 25511*	The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (norm‘𝐻))
Theorem	rrxcph 25512	Generalized Euclidean real spaces are subcomplex pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil)
Theorem	rrxds 25513*	The distance over generalized Euclidean spaces. Compare with df-rrn 38337. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻))
Theorem	rrxvsca 25514	The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ ∙ = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))    ⇒   ⊢ (𝜑 → ((𝐴 ∙ 𝑋)‘𝐽) = (𝐴 · (𝑋‘𝐽)))
Theorem	rrxplusgvscavalb 25515*	The result of the addition combined with scalar multiplication in a generalized Euclidean space is defined by its coordinate-wise operations. (Contributed by AV, 21-Jan-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ ∙ = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ ✚ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑍 = ((𝐴 ∙ 𝑋) ✚ (𝐶 ∙ 𝑌)) ↔ ∀𝑖 ∈ 𝐼 (𝑍‘𝑖) = ((𝐴 · (𝑋‘𝑖)) + (𝐶 · (𝑌‘𝑖)))))
Theorem	rrxsca 25516	The field of real numbers is the scalar field of the generalized real Euclidean space. (Contributed by AV, 15-Jan-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (Scalar‘𝐻) = ℝfld)
Theorem	rrx0 25517	The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 0 = (𝐼 × {0})    ⇒   ⊢ (𝐼 ∈ 𝑉 → (0g‘𝐻) = 0 )
Theorem	rrx0el 25518	The zero ("origin") in a generalized real Euclidean space is an element of its base set. (Contributed by AV, 11-Feb-2023.)
⊢ 0 = (𝐼 × {0})    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 0 ∈ 𝑃)
Theorem	csbren 25519*	Cauchy-Schwarz-Bunjakovsky inequality for R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶)↑2) ≤ (Σ𝑘 ∈ 𝐴 (𝐵↑2) · Σ𝑘 ∈ 𝐴 (𝐶↑2)))
Theorem	trirn 25520*	Triangle inequality in R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (√‘Σ𝑘 ∈ 𝐴 ((𝐵 + 𝐶)↑2)) ≤ ((√‘Σ𝑘 ∈ 𝐴 (𝐵↑2)) + (√‘Σ𝑘 ∈ 𝐴 (𝐶↑2))))
Theorem	rrxf 25521*	Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐹:𝐼⟶ℝ)
Theorem	rrxfsupp 25522*	Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 supp 0) ∈ Fin)
Theorem	rrxsuppss 25523*	Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 supp 0) ⊆ 𝐼)
Theorem	rrxmvallem 25524*	Support of the function used for building the distance . (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑘 ∈ 𝐼 ↦ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) supp 0) ⊆ ((𝐹 supp 0) ∪ (𝐺 supp 0)))
Theorem	rrxmval 25525*	The value of the Euclidean metric. Compare with rrnmval 38339. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	rrxmfval 25526*	The value of the Euclidean metric. Compare with rrnval 38338. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑓 supp 0) ∪ (𝑔 supp 0))(((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))
Theorem	rrxmetlem 25527*	Lemma for rrxmet 25528. (Contributed by Thierry Arnoux, 5-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ⊆ 𝐴)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ 𝐴 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
Theorem	rrxmet 25528*	Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) (Revised by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋))
Theorem	rrxdstprj1 25529*	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹𝐷𝐺))
Theorem	rrxbasefi 25530	The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of (ℝ ↑m 𝑋) for the development of the Lebesgue measure theory for n-dimensional real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐻 = (ℝ^‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝜑 → 𝐵 = (ℝ ↑m 𝑋))
Theorem	rrxdsfi 25531*	The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (dist‘𝐻) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))
Theorem	rrxmetfi 25532	Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ ↑m 𝐼)))
Theorem	rrxdsfival 25533*	The value of the Euclidean distance function in a generalized real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	ehlval 25534	Value of the Euclidean space of dimension 𝑁. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐸 = (𝔼hil‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐸 = (ℝ^‘(1...𝑁)))
Theorem	ehlbase 25535	The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐸 = (𝔼hil‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (ℝ ↑m (1...𝑁)) = (Base‘𝐸))
Theorem	ehl0base 25536	The base of the Euclidean space of dimension 0 consists only of one element, the empty set. (Contributed by AV, 12-Feb-2023.)
⊢ 𝐸 = (𝔼hil‘0)    ⇒   ⊢ (Base‘𝐸) = {∅}
Theorem	ehl0 25537	The Euclidean space of dimension 0 consists of the neutral element only. (Contributed by AV, 12-Feb-2023.)
⊢ 𝐸 = (𝔼hil‘0)    &   ⊢ 0 = (0g‘𝐸)    ⇒   ⊢ (Base‘𝐸) = { 0 }
Theorem	ehleudis 25538*	The Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.)
⊢ 𝐼 = (1...𝑁)    &   ⊢ 𝐸 = (𝔼hil‘𝑁)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))
Theorem	ehleudisval 25539*	The value of the Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.)
⊢ 𝐼 = (1...𝑁)    &   ⊢ 𝐸 = (𝔼hil‘𝑁)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	ehl1eudis 25540*	The Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘1)    &   ⊢ 𝑋 = (ℝ ↑m {1})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (abs‘((𝑓‘1) − (𝑔‘1))))
Theorem	ehl1eudisval 25541	The value of the Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘1)    &   ⊢ 𝑋 = (ℝ ↑m {1})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (abs‘((𝐹‘1) − (𝐺‘1))))
Theorem	ehl2eudis 25542*	The Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘2)    &   ⊢ 𝑋 = (ℝ ↑m {1, 2})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2))))
Theorem	ehl2eudisval 25543	The value of the Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘2)    &   ⊢ 𝑋 = (ℝ ↑m {1, 2})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘((((𝐹‘1) − (𝐺‘1))↑2) + (((𝐹‘2) − (𝐺‘2))↑2))))
12.5.9  Minimizing Vector Theorem
Theorem	minveclem1 25544*	Lemma for minvec 25556. The set of all distances from points of 𝑌 to 𝐴 are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
Theorem	minveclem4c 25545*	Lemma for minvec 25556. The infimum of the distances to 𝐴 is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑆 ∈ ℝ)
Theorem	minveclem2 25546*	Lemma for minvec 25556. Any two points 𝐾 and 𝐿 in 𝑌 are close to each other if they are close to the infimum of distance to 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑌)    &   ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))    &   ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))    ⇒   ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))
Theorem	minveclem3a 25547*	Lemma for minvec 25556. 𝐷 is a complete metric when restricted to 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌))
Theorem	minveclem3b 25548*	Lemma for minvec 25556. The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    ⇒   ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
Theorem	minveclem3 25549*	Lemma for minvec 25556. The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    ⇒   ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))
Theorem	minveclem4a 25550*	Lemma for minvec 25556. 𝐹 converges to a point 𝑃 in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    ⇒   ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
Theorem	minveclem4b 25551*	Lemma for minvec 25556. The convergent point of the Cauchy sequence 𝐹 is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑋)
Theorem	minveclem4 25552*	Lemma for minvec 25556. The convergent point of the Cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    &   ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minveclem5 25553*	Lemma for minvec 25556. Discharge the assumptions in minveclem4 25552. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minveclem6 25554*	Lemma for minvec 25556. Any minimal point is less than 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))))
Theorem	minveclem7 25555*	Lemma for minvec 25556. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minvec 25556*	Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace 𝑊 that minimizes the distance to an arbitrary vector 𝐴 in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
12.5.10  Projection Theorem
Theorem	pjthlem1 25557*	Lemma for pjth 25559. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.) (Proof shortened by AV, 10-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂHil)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑁‘𝐴) ≤ (𝑁‘(𝐴 − 𝑥)))    &   ⊢ 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))    ⇒   ⊢ (𝜑 → (𝐴 , 𝐵) = 0)
Theorem	pjthlem2 25558	Lemma for pjth 25559. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂHil)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))
Theorem	pjth 25559	Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed uniquely into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑈 ⊕ (𝑂‘𝑈)) = 𝑉)
Theorem	pjth2 25560	Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐾 = (proj‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ∈ dom 𝐾)
Theorem	cldcss 25561	Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂHil → (𝑈 ∈ 𝐶 ↔ (𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽))))
Theorem	cldcss2 25562	Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂHil → 𝐶 = (𝐿 ∩ (Clsd‘𝐽)))
Theorem	hlhil 25563	Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ Hil)
PART 13  BASIC REAL AND COMPLEX ANALYSIS
13.1  Continuity
Theorem	addcncf 25564*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	subcncf 25565*	The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	mulcncf 25566*	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) Avoid ax-mulf 11168. (Revised by GG, 16-Mar-2025.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	divcncf 25567*	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→(ℂ ∖ {0})))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵)) ∈ (𝑋–cn→ℂ))
13.1.1  Intermediate value theorem
Theorem	pmltpclem1 25568*	Lemma for pmltpc 25570. (Contributed by Mario Carneiro, 1-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    &   ⊢ (𝜑 → (((𝐹‘𝐴) < (𝐹‘𝐵) ∧ (𝐹‘𝐶) < (𝐹‘𝐵)) ∨ ((𝐹‘𝐵) < (𝐹‘𝐴) ∧ (𝐹‘𝐵) < (𝐹‘𝐶))))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐)))))
Theorem	pmltpclem2 25569*	Lemma for pmltpc 25570. (Contributed by Mario Carneiro, 1-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (ℝ ↑pm ℝ))    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ≤ 𝑉)    &   ⊢ (𝜑 → 𝑊 ≤ 𝑋)    &   ⊢ (𝜑 → ¬ (𝐹‘𝑈) ≤ (𝐹‘𝑉))    &   ⊢ (𝜑 → ¬ (𝐹‘𝑋) ≤ (𝐹‘𝑊))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐)))))
Theorem	pmltpc 25570*	Any function on the reals is either increasing, decreasing, or has a triple of points in a vee formation. (This theorem was created on demand by Mario Carneiro for the 6PCM conference in Bialystok, 1-Jul-2014.) (Contributed by Mario Carneiro, 1-Jul-2014.)
⊢ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ∨ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ∨ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))))
Theorem	ivthlem1 25571*	Lemma for ivth 25574. The set 𝑆 of all 𝑥 values with (𝐹‘𝑥) less than 𝑈 is lower bounded by 𝐴 and upper bounded by 𝐵. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
Theorem	ivthlem2 25572*	Lemma for ivth 25574. Show that the supremum of 𝑆 cannot be less than 𝑈. If it was, continuity of 𝐹 implies that there are points just above the supremum that are also less than 𝑈, a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}    &   ⊢ 𝐶 = sup(𝑆, ℝ, < )    ⇒   ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)
Theorem	ivthlem3 25573*	Lemma for ivth 25574, the intermediate value theorem. Show that (𝐹‘𝐶) cannot be greater than 𝑈, and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 17-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}    &   ⊢ 𝐶 = sup(𝑆, ℝ, < )    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈))
Theorem	ivth 25574*	The intermediate value theorem, increasing case. This is Metamath 100 proof #79. (Contributed by Paul Chapman, 22-Jan-2008.) (Proof shortened by Mario Carneiro, 30-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivth2 25575*	The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthle 25576*	The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐵)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthle2 25577*	The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐵) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐴)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthicc 25578*	The interval between any two points of a continuous real function is contained in the range of the function. Equivalently, the range of a continuous real function is convex. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ran 𝐹)
Theorem	evthicc 25579*	Specialization of the Extreme Value Theorem to a closed interval of ℝ. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑥) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(𝐹‘𝑧) ≤ (𝐹‘𝑤)))
Theorem	evthicc2 25580*	Combine ivthicc 25578 with evthicc 25579 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran 𝐹 = (𝑥[,]𝑦))
Theorem	cniccbdd 25581*	A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥)
13.2  Integrals
13.2.1  Lebesgue measure
Syntax	covol 25582	Extend class notation with the outer Lebesgue measure.
class vol*
Syntax	cvol 25583	Extend class notation with the Lebesgue measure.
class vol
Definition	df-ovol 25584*	Define the outer Lebesgue measure for subsets of the reals. Here 𝑓 is a function from the positive integers to pairs ⟨𝑎, 𝑏⟩ with 𝑎 ≤ 𝑏, and the outer volume of the set 𝑥 is the infimum over all such functions such that the union of the open intervals (𝑎, 𝑏) covers 𝑥 of the sum of 𝑏 − 𝑎. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.)
⊢ vol* = (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
Definition	df-vol 25585*	Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as 𝐴 ∈ dom vol. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ vol = (vol* ↾ {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))})
Theorem	ovolfcl 25586	Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑁)) ≤ (2nd ‘(𝐹‘𝑁))))
Theorem	ovolfioo 25587*	Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛)))))
Theorem	ovolficc 25588*	Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ([,] ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))
Theorem	ovolficcss 25589	Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
Theorem	ovolfsval 25590	The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐺‘𝑁) = ((2nd ‘(𝐹‘𝑁)) − (1st ‘(𝐹‘𝑁))))
Theorem	ovolfsf 25591	Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    ⇒   ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺:ℕ⟶(0[,)+∞))
Theorem	ovolsf 25592	Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    &   ⊢ 𝑆 = seq1( + , 𝐺)    ⇒   ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
Theorem	ovolval 25593*	The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) = inf(𝑀, ℝ*, < ))
Theorem	elovolmlem 25594	Lemma for elovolm 25595 and related theorems. (Contributed by BJ, 23-Jul-2022.)
⊢ (𝐹 ∈ ((𝐴 ∩ (ℝ × ℝ)) ↑m ℕ) ↔ 𝐹:ℕ⟶(𝐴 ∩ (ℝ × ℝ)))
Theorem	elovolm 25595*	Elementhood in the set 𝑀 of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )))
Theorem	elovolmr 25596*	Sufficient condition for elementhood in the set 𝑀. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Theorem	ovolmge0 25597*	The set 𝑀 is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵)
Theorem	ovolcl 25598	The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*)
Theorem	ovollb 25599	The outer volume is a lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolgelb 25600*	The outer volume is the greatest lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝑔))    ⇒   ⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵)))