P. 468 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46701-46800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvnprodlem1 46701*	𝐷 is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)    &   ⊢ (𝜑 → 𝑇 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    &   ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅)    &   ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)    ⇒   ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘)))
Theorem	dvnprodlem2 46702*	Induction step for dvnprodlem2 46702. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑇 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡):𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻‘𝑡))‘𝑗):𝑋⟶ℂ)    &   ⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑇 ∖ 𝑅))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑅 ((𝐻‘𝑡)‘𝑥)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐶‘𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡 ∈ 𝑅 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑅 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))    &   ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))    &   ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)⟩)    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻‘𝑡)‘𝑥)))‘𝐽) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐‘𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
Theorem	dvnprodlem3 46703*	The multinomial formula for the 𝑘-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑇 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡):𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻‘𝑡))‘𝑗):𝑋⟶ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥))    &   ⊢ 𝐷 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛}))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛})    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
Theorem	dvnprod 46704*	The multinomial formula for the 𝑁-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))    &   ⊢ (𝜑 → 𝑇 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡):𝑋⟶ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻‘𝑡))‘𝑘):𝑋⟶ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ∏𝑡 ∈ 𝑇 ((𝐻‘𝑡)‘𝑥))    &   ⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑇) ∣ Σ𝑡 ∈ 𝑇 (𝑐‘𝑡) = 𝑛})    ⇒   ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ (𝐶‘𝑁)(((!‘𝑁) / ∏𝑡 ∈ 𝑇 (!‘(𝑐‘𝑡))) · ∏𝑡 ∈ 𝑇 (((𝑆 D𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥))))
21.44.11  Integrals
Theorem	itgsin0pilem1 46705*	Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐶 = (𝑡 ∈ (0[,]π) ↦ -(cos‘𝑡))    ⇒   ⊢ ∫(0(,)π)(sin‘𝑥) d𝑥 = 2
Theorem	ibliccsinexp 46706*	sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
Theorem	itgsin0pi 46707	Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ∫(0(,)π)(sin‘𝑥) d𝑥 = 2
Theorem	iblioosinexp 46708*	sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1)
Theorem	itgsinexplem1 46709*	Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ((sin‘𝑥)↑𝑁))    &   ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ -(cos‘𝑥))    &   ⊢ 𝐻 = (𝑥 ∈ ℂ ↦ ((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)))    &   ⊢ 𝐼 = (𝑥 ∈ ℂ ↦ (((sin‘𝑥)↑𝑁) · (sin‘𝑥)))    &   ⊢ 𝐿 = (𝑥 ∈ ℂ ↦ (((𝑁 · ((sin‘𝑥)↑(𝑁 − 1))) · (cos‘𝑥)) · -(cos‘𝑥)))    &   ⊢ 𝑀 = (𝑥 ∈ ℂ ↦ (((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∫(0(,)π)(((sin‘𝑥)↑𝑁) · (sin‘𝑥)) d𝑥 = (𝑁 · ∫(0(,)π)(((cos‘𝑥)↑2) · ((sin‘𝑥)↑(𝑁 − 1))) d𝑥))
Theorem	itgsinexp 46710*	A recursive formula for the integral of sin^N on the interval (0,π) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    ⇒   ⊢ (𝜑 → (𝐼‘𝑁) = (((𝑁 − 1) / 𝑁) · (𝐼‘(𝑁 − 2))))
Theorem	iblconstmpt 46711*	A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
Theorem	itgeq1d 46712*	Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	mbfres2cn 46713	Measurability of a piecewise function: if 𝐹 is measurable on subsets 𝐵 and 𝐶 of its domain, and these pieces make up all of 𝐴, then 𝐹 is measurable on the whole domain. Similar to mbfres2 25841 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ MblFn)    &   ⊢ (𝜑 → (𝐵 ∪ 𝐶) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	vol0 46714	The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (vol‘∅) = 0
Theorem	ditgeqiooicc 46715*	A function 𝐹 on an open interval, has the same directed integral as its extension 𝐺 on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵](𝐹‘𝑥) d𝑥 = ⨜[𝐴 → 𝐵](𝐺‘𝑥) d𝑥)
Theorem	volge0 46716	The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ dom vol → 0 ≤ (vol‘𝐴))
Theorem	cnbdibl 46717*	A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ (𝜑 → (vol‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
Theorem	snmbl 46718	A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → {𝐴} ∈ dom vol)
Theorem	ditgeq3d 46719*	Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐷 = 𝐸)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥)
Theorem	iblempty 46720	The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ∅ ∈ 𝐿1
Theorem	iblsplit 46721*	The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈ 𝐿1)
Theorem	volsn 46722	A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → (vol‘{𝐴}) = 0)
Theorem	itgvol0 46723*	If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ∧ ∫𝐴𝐵 d𝑥 = 0))
Theorem	itgcoscmulx 46724*	Exercise: the integral of 𝑥 ↦ cos𝑎𝑥 on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ∫(𝐵(,)𝐶)(cos‘(𝐴 · 𝑥)) d𝑥 = (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴))
Theorem	iblsplitf 46725*	A version of iblsplit 46721 using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈ 𝐿1)
Theorem	ibliooicc 46726*	If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
Theorem	volioc 46727	The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,]𝐵)) = (𝐵 − 𝐴))
Theorem	iblspltprt 46728*	If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑡𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))    &   ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈ 𝐿1)
Theorem	itgsincmulx 46729*	Exercise: the integral of 𝑥 ↦ sin𝑎𝑥 on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫(𝐵(,)𝐶)(sin‘(𝐴 · 𝑥)) d𝑥 = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴))
Theorem	itgsubsticclem 46730*	lemma for itgsubsticc 46731. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶)    &   ⊢ 𝐺 = (𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿))))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾[,]𝐿)–cn→ℂ))    &   ⊢ (𝜑 → 𝐾 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝐿)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))    &   ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)    ⇒   ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)
Theorem	itgsubsticc 46731*	Integration by u-substitution. The main difference with respect to itgsubst 26245 is that here we consider the range of 𝐴(𝑥) to be in the closed interval (𝐾[,]𝐿). If 𝐴(𝑥) is a continuous, differentiable function from [𝑋, 𝑌] to (𝑍, 𝑊), whose derivative is continuous and integrable, and 𝐶(𝑢) is a continuous function on (𝑍, 𝑊), then the integral of 𝐶(𝑢) from 𝐾 = 𝐴(𝑋) to 𝐿 = 𝐴(𝑌) is equal to the integral of 𝐶(𝐴(𝑥)) D 𝐴(𝑥) from 𝑋 to 𝑌. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿)))    &   ⊢ (𝜑 → (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶) ∈ ((𝐾[,]𝐿)–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))    &   ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    ⇒   ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)
Theorem	itgioocnicc 46732*	The integral of a piecewise continuous function 𝐹 on an open interval is equal to the integral of the continuous function 𝐺, in the corresponding closed interval. 𝐺 is equal to 𝐹 on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)    &   ⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴))    &   ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝐿1 ∧ ∫(𝐴[,]𝐵)(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
Theorem	iblcncfioo 46733	A continuous function 𝐹 on an open interval (𝐴(,)𝐵) with a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵 is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
Theorem	itgspltprt 46734*	The ∫ integral splits on a given partition 𝑃. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))    &   ⊢ (𝜑 → 𝑃:(𝑀...𝑁)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))    &   ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
Theorem	itgiccshift 46735*	The integral of a function, 𝐹 stays the same if its closed interval domain is shifted by 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇)))    ⇒   ⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
Theorem	itgperiod 46736*	The integral of a periodic function, with period 𝑇 stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))    ⇒   ⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
Theorem	itgsbtaddcnst 46737*	Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    ⇒   ⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡)
Theorem	volico 46738	The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0))
Theorem	sublevolico 46739	The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (vol‘(𝐴[,)𝐵)))
Theorem	dmvolss 46740	Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ dom vol ⊆ 𝒫 ℝ
Theorem	ismbl3 46741*	The predicate "𝐴 is Lebesgue-measurable". Similar to ismbl2 25723, but here +𝑒 is used, and the precondition (vol*‘𝑥) ∈ ℝ can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))
Theorem	volioof 46742	The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞)
Theorem	ovolsplit 46743	The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐴) ≤ ((vol*‘(𝐴 ∩ 𝐵)) +𝑒 (vol*‘(𝐴 ∖ 𝐵))))
Theorem	fvvolioof 46744	The function value of the Lebesgue measure of an open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶(ℝ* × ℝ*))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (((vol ∘ (,)) ∘ 𝐹)‘𝑋) = (vol‘((1st ‘(𝐹‘𝑋))(,)(2nd ‘(𝐹‘𝑋)))))
Theorem	volioore 46745	The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) = if(𝐴 ≤ 𝐵, (𝐵 − 𝐴), 0))
Theorem	fvvolicof 46746	The function value of the Lebesgue measure of a left-closed right-open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶(ℝ* × ℝ*))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (((vol ∘ [,)) ∘ 𝐹)‘𝑋) = (vol‘((1st ‘(𝐹‘𝑋))[,)(2nd ‘(𝐹‘𝑋)))))
Theorem	voliooico 46747	An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (vol‘(𝐴[,)𝐵)))
Theorem	ismbl4 46748*	The predicate "𝐴 is Lebesgue-measurable". Similar to ismbl 25722, but here +𝑒 is used, and the precondition (vol*‘𝑥) ∈ ℝ can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ(vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴)))))
Theorem	volioofmpt 46749*	((vol ∘ (,)) ∘ 𝐹) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶(ℝ* × ℝ*))    ⇒   ⊢ (𝜑 → ((vol ∘ (,)) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (vol‘((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥))))))
Theorem	volicoff 46750	((vol ∘ [,)) ∘ 𝐹) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶(ℝ × ℝ*))    ⇒   ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹):𝐴⟶(0[,]+∞))
Theorem	voliooicof 46751	The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right-open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶(ℝ × ℝ))    ⇒   ⊢ (𝜑 → ((vol ∘ (,)) ∘ 𝐹) = ((vol ∘ [,)) ∘ 𝐹))
Theorem	volicofmpt 46752*	((vol ∘ [,)) ∘ 𝐹) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶(ℝ × ℝ*))    ⇒   ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (vol‘((1st ‘(𝐹‘𝑥))[,)(2nd ‘(𝐹‘𝑥))))))
Theorem	volicc 46753	The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
Theorem	voliccico 46754	A closed interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol‘(𝐴[,]𝐵)) = (vol‘(𝐴[,)𝐵)))
Theorem	mbfdmssre 46755	The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝐹 ∈ MblFn → dom 𝐹 ⊆ ℝ)
21.44.12  Stone Weierstrass theorem - real version
Theorem	stoweidlem1 46756	Lemma for stoweid 46818. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 14285. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 1)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((1 − (𝐴↑𝑁))↑(𝐾↑𝑁)) ≤ (1 / ((𝐾 · 𝐷)↑𝑁)))
Theorem	stoweidlem2 46757*	lemma for stoweid 46818: here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (𝐸 · (𝐹‘𝑡))) ∈ 𝐴)
Theorem	stoweidlem3 46758*	Lemma for stoweid 46818: if 𝐴 is positive and all 𝑀 terms of a finite product are larger than 𝐴, then the finite product is larger than 𝐴↑𝑀. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝐹    &   ⊢ Ⅎ𝑖𝜑    &   ⊢ 𝑋 = seq1( · , 𝐹)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 < (𝐹‘𝑖))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴↑𝑀) < (𝑋‘𝑀))
Theorem	stoweidlem4 46759*	Lemma for stoweid 46818: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝐵) ∈ 𝐴)
Theorem	stoweidlem5 46760*	There exists a δ as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: 0 < δ < 1 , p >= δ on 𝑇 ∖ 𝑈. Here 𝐷 is used to represent δ in the paper and 𝑄 to represent 𝑇 ∖ 𝑈 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐷 = if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2))    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑄 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑄 𝐶 ≤ (𝑃‘𝑡))    ⇒   ⊢ (𝜑 → ∃𝑑(𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀𝑡 ∈ 𝑄 𝑑 ≤ (𝑃‘𝑡)))
Theorem	stoweidlem6 46761*	Lemma for stoweid 46818: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡 𝑓 = 𝐹    &   ⊢ Ⅎ𝑡 𝑔 = 𝐺    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐺‘𝑡))) ∈ 𝐴)
Theorem	stoweidlem7 46762*	This lemma is used to prove that qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91, (at the top of page 91), is such that qn < ε on 𝑇 ∖ 𝑈, and qn > 1 - ε on 𝑉. Here it is proven that, for 𝑛 large enough, 1-(k*δ/2)^n > 1 - ε , and 1/(k*δ)^n < ε. The variable 𝐴 is used to represent (k*δ) in the paper, and 𝐵 is used to represent (k*δ/2). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐹 = (𝑖 ∈ ℕ0 ↦ ((1 / 𝐴)↑𝑖))    &   ⊢ 𝐺 = (𝑖 ∈ ℕ0 ↦ (𝐵↑𝑖))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 < 1)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸))
Theorem	stoweidlem8 46763*	Lemma for stoweid 46818: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝐺    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) + (𝐺‘𝑡))) ∈ 𝐴)
Theorem	stoweidlem9 46764*	Lemma for stoweid 46818: here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → 𝑇 = ∅)    &   ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑔‘𝑡) − (𝐹‘𝑡))) < 𝐸)
Theorem	stoweidlem10 46765	Lemma for stoweid 46818. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90, this lemma is an application of Bernoulli's inequality. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ≤ 1) → (1 − (𝑁 · 𝐴)) ≤ ((1 − 𝐴)↑𝑁))
Theorem	stoweidlem11 46766*	This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑡 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑗 ∈ (1...𝑁))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑡) ≤ 1)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    ⇒   ⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
Theorem	stoweidlem12 46767*	Lemma for stoweid 46818. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑄‘𝑡) = ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))
Theorem	stoweidlem13 46768	Lemma for stoweid 46818. This lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon, in the last step of the proof in [BrosowskiDeutsh] p. 92. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑗 ∈ ℝ)    &   ⊢ (𝜑 → ((𝑗 − (4 / 3)) · 𝐸) < 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ ((𝑗 − (1 / 3)) · 𝐸))    &   ⊢ (𝜑 → ((𝑗 − (4 / 3)) · 𝐸) < 𝑌)    &   ⊢ (𝜑 → 𝑌 < ((𝑗 + (1 / 3)) · 𝐸))    ⇒   ⊢ (𝜑 → (abs‘(𝑌 − 𝑋)) < (2 · 𝐸))
Theorem	stoweidlem14 46769*	There exists a 𝑘 as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: 𝑘 is an integer and 1 < k * δ < 2. 𝐷 is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐴 = {𝑗 ∈ ℕ ∣ (1 / 𝐷) < 𝑗}    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 < 1)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℕ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1))
Theorem	stoweidlem15 46770*	This lemma is used to prove the existence of a function 𝑝 as in Lemma 1 from [BrosowskiDeutsh] p. 90: 𝑝 is in the subalgebra, such that 0 ≤ p ≤ 1, p_(t0) = 0, and p > 0 on T - U. Here (𝐺‘𝐼) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ (((𝜑 ∧ 𝐼 ∈ (1...𝑀)) ∧ 𝑆 ∈ 𝑇) → (((𝐺‘𝐼)‘𝑆) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝐼)‘𝑆) ∧ ((𝐺‘𝐼)‘𝑆) ≤ 1))
Theorem	stoweidlem16 46771*	Lemma for stoweid 46818. The subset 𝑌 of functions in the algebra 𝐴, with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → 𝐻 ∈ 𝑌)
Theorem	stoweidlem17 46772*	This lemma proves that the function 𝑔 (as defined in [BrosowskiDeutsh] p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑋:(0...𝑁)⟶𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)
Theorem	stoweidlem18 46773*	This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐷    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ 1)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 = ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))
Theorem	stoweidlem19 46774*	If a set of real functions is closed under multiplication and it contains constants, then it is closed under finite exponentiation. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑁)) ∈ 𝐴)
Theorem	stoweidlem20 46775*	If a set A of real functions from a common domain T is closed under the sum of two functions, then it is closed under the sum of a finite number of functions, indexed by G. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐴)
Theorem	stoweidlem21 46776*	Once the Stone Weierstrass theorem has been proven for approximating nonnegative functions, then this lemma is used to extend the result to functions with (possibly) negative values. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐺    &   ⊢ Ⅎ𝑡𝐻    &   ⊢ Ⅎ𝑡𝑆    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + 𝑆))    &   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 𝑓:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (abs‘((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆))) < 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)
Theorem	stoweidlem22 46777*	If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝐺    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝐺‘𝑡)))    &   ⊢ 𝐼 = (𝑡 ∈ 𝑇 ↦ -1)    &   ⊢ 𝐿 = (𝑡 ∈ 𝑇 ↦ ((𝐼‘𝑡) · (𝐺‘𝑡)))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝐺‘𝑡))) ∈ 𝐴)
Theorem	stoweidlem23 46778*	This lemma is used to prove the existence of a function pt as in the beginning of Lemma 1 [BrosowskiDeutsh] p. 90: for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑡𝐺    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐺‘𝑍)))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺‘𝑆) ≠ (𝐺‘𝑍))    ⇒   ⊢ (𝜑 → (𝐻 ∈ 𝐴 ∧ (𝐻‘𝑆) ≠ (𝐻‘𝑍) ∧ (𝐻‘𝑍) = 0))
Theorem	stoweidlem24 46779*	This lemma proves that for 𝑛 sufficiently large, qn( t ) > ( 1 - epsilon ), for all 𝑡 in 𝑉: see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). 𝑄 is used to represent qn in the paper, 𝑁 to represent 𝑛 in the paper, 𝐾 to represent 𝑘, 𝐷 to represent δ, and 𝐸 to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)}    &   ⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁)))    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (𝑄‘𝑡))
Theorem	stoweidlem25 46780*	This lemma proves that for n sufficiently large, qn( t ) < ε, for all 𝑡 in 𝑇 ∖ 𝑈: see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). 𝑄 is used to represent qn in the paper, 𝑁 to represent n in the paper, 𝐾 to represent k, 𝐷 to represent δ, 𝑃 to represent p, and 𝐸 to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (1 / ((𝐾 · 𝐷)↑𝑁)) < 𝐸)    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (𝑄‘𝑡) < 𝐸)
Theorem	stoweidlem26 46781*	This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here 𝐿 is used to represent j in the paper, 𝐷 is used to represent A in the paper, 𝑆 is used to represent t, and 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})    &   ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))    &   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))    ⇒   ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))
Theorem	stoweidlem27 46782*	This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here (𝑞‘𝑖) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})    &   ⊢ (𝜑 → 𝑄 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 Fn ran 𝐺)    &   ⊢ (𝜑 → ran 𝐺 ∈ V)    &   ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)    &   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎℎ𝑄    ⇒   ⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))
Theorem	stoweidlem28 46783*	There exists a δ as in Lemma 1 [BrosowskiDeutsh] p. 90: 0 < delta < 1 and p >= delta on 𝑇 ∖ 𝑈. Here 𝑑 is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑈    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    ⇒   ⊢ (𝜑 → ∃𝑑(𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝑑 ≤ (𝑃‘𝑡)))
Theorem	stoweidlem29 46784*	When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) (Revised by AV, 13-Sep-2020.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    ⇒   ⊢ (𝜑 → (inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ inf(ran 𝐹, ℝ, < ) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)))
Theorem	stoweidlem30 46785*	This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (𝐺‘𝑖) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (𝑃‘𝑆) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆)))
Theorem	stoweidlem31 46786*	This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that 𝑅 is a finite subset of 𝑉, 𝑥 indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all 𝑖 ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on 𝐵. Here M is used to represent m in the paper, 𝐸 is used to represent ε in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎℎ𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}    &   ⊢ 𝐺 = (𝑤 ∈ 𝑅 ↦ {ℎ ∈ 𝐴 ∣ (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − (𝐸 / 𝑀)) < (ℎ‘𝑡))})    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑣:(1...𝑀)–1-1-onto→𝑅)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ⊆ (𝑇 ∖ 𝑈))    &   ⊢ (𝜑 → 𝑉 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → ran 𝐺 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑥(𝑥:(1...𝑀)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑀)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑀) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑥‘𝑖)‘𝑡))))
Theorem	stoweidlem32 46787*	If a set A of real functions from a common domain T is a subalgebra and it contains constants, then it is closed under the sum of a finite number of functions, indexed by G and finally scaled by a real Y. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ (𝑌 · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝐴)
Theorem	stoweidlem33 46788*	If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝐺    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝐺‘𝑡))) ∈ 𝐴)
Theorem	stoweidlem34 46789*	This lemma proves that for all 𝑡 in 𝑇 there is a 𝑗 as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})    &   ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})    &   ⊢ 𝐽 = (𝑡 ∈ 𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)})    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (𝐹‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) < ((𝑁 − 1) · 𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋‘𝑗):𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑗)‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑗)‘𝑡) ≤ 1)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗)) → ((𝑋‘𝑗)‘𝑡) < (𝐸 / 𝑁))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑗)‘𝑡))    ⇒   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))
Theorem	stoweidlem35 46790*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here (𝑞‘𝑖) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎℎ𝜑    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}    &   ⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑊)    &   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)    &   ⊢ (𝜑 → (𝑇 ∖ 𝑈) ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑚∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞‘𝑖)‘𝑡))))
Theorem	stoweidlem36 46791*	This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Z is used for t0 , S is used for t e. T - U , h is used for pt . G is used for (ht)^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎℎ𝑄    &   ⊢ Ⅎ𝑡𝐻    &   ⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝐺    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐹‘𝑡)))    &   ⊢ 𝑁 = sup(ran 𝐺, ℝ, < )    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) / 𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝑆) ≠ (𝐹‘𝑍))    &   ⊢ (𝜑 → (𝐹‘𝑍) = 0)    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑆)))
Theorem	stoweidlem37 46792*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (𝐺‘𝑖) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝑃‘𝑍) = 0)
Theorem	stoweidlem38 46793*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (𝐺‘𝑖) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (0 ≤ (𝑃‘𝑆) ∧ (𝑃‘𝑆) ≤ 1))
Theorem	stoweidlem39 46794*	This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that 𝑟 is a finite subset of 𝑊, 𝑥 indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on 𝐵. Here 𝐷 is used to represent A in the paper's Lemma 2 (because 𝐴 is used for the subalgebra), 𝑀 is used to represent m in the paper, 𝐸 is used to represent ε, and vi is used to represent V(ti). 𝑊 is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎℎ𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ 𝑈 = (𝑇 ∖ 𝐵)    &   ⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}    &   ⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))}    &   ⊢ (𝜑 → 𝑟 ∈ (𝒫 𝑊 ∩ Fin))    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑟)    &   ⊢ (𝜑 → 𝐷 ≠ ∅)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑇)    &   ⊢ (𝜑 → 𝑊 ∈ V)    &   ⊢ (𝜑 → 𝐴 ∈ V)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑥‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥‘𝑖)‘𝑡)))))
Theorem	stoweidlem40 46795*	This lemma proves that qn is in the subalgebra, as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent qn in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑃    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁)))    &   ⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ 1)    &   ⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝑄 ∈ 𝐴)
Theorem	stoweidlem41 46796*	This lemma is used to prove that there exists x as in Lemma 1 of [BrosowskiDeutsh] p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - qn";. Here 𝐸 is used to represent ε in the paper, and 𝑦 to represent qn in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑋 = (𝑡 ∈ 𝑇 ↦ (1 − (𝑦‘𝑡)))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ 1)    &   ⊢ 𝑉 ⊆ 𝑇    &   ⊢ (𝜑 → 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑦:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑤) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1))    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑥‘𝑡)))
Theorem	stoweidlem42 46797*	This lemma is used to prove that 𝑥 built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x > 1 - ε on B. Here 𝑋 is used to represent 𝑥 in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎ𝑡𝑌    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))    &   ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈‘𝑖)‘𝑡))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐸 < (1 / 3))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑇)    ⇒   ⊢ (𝜑 → ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡))
Theorem	stoweidlem43 46798*	This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function pt in the subalgebra, such that pt( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Hera Z is used for t0 , S is used for t e. T - U , h is used for pt. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑔𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ Ⅎℎ𝑄    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑙‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑙 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑙‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑔 ∈ 𝐴 (𝑔‘𝑟) ≠ (𝑔‘𝑡))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ (𝑇 ∖ 𝑈))    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑆)))
Theorem	stoweidlem44 46799*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}    &   ⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄)    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑗 ∈ (1...𝑀)0 < ((𝐺‘𝑗)‘𝑡))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑇)    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)))
Theorem	stoweidlem45 46800*	This lemma proves that, given an appropriate 𝐾 (in another theorem we prove such a 𝐾 exists), there exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= qn <= 1 , qn < ε on T \ U, and qn > 1 - ε on 𝑉. We use y to represent the final qn in the paper (the one with n large enough), 𝑁 to represent 𝑛 in the paper, 𝐾 to represent 𝑘, 𝐷 to represent δ, 𝐸 to represent ε, and 𝑃 to represent 𝑝. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝑃    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)}    &   ⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 < 1)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑃:𝑇⟶ℝ)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))    &   ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁)))    &   ⊢ (𝜑 → (1 / ((𝐾 · 𝐷)↑𝑁)) < 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸))