![]() |
Metamath
Proof Explorer Theorem List (p. 460 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvnprodlem1 45901* | 𝐷 is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡 ∈ 𝑠 (𝑐‘𝑡) = 𝑛})) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ 〈(𝐽 − (𝑐‘𝑍)), (𝑐 ↾ 𝑅)〉) & ⊢ (𝜑 → 𝑇 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑇) & ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑅) & ⊢ (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇) ⇒ ⊢ (𝜑 → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto→∪ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶‘𝑅)‘𝑘))) | ||
Theorem | dvnprodlem2 45902* | Induction step for dvnprodlem2 45902. (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 45903* | 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 45904* | 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𝑛 (𝐻‘𝑡))‘(𝑐‘𝑡))‘𝑥)))) | ||
Theorem | itgsin0pilem1 45905* | 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 45906* | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1) | ||
Theorem | itgsin0pi 45907 | Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ∫(0(,)π)(sin‘𝑥) d𝑥 = 2 | ||
Theorem | iblioosinexp 45908* | sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((sin‘𝑥)↑𝑁)) ∈ 𝐿1) | ||
Theorem | itgsinexplem1 45909* | 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 45910* | 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 45911* | A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) | ||
Theorem | itgeq1d 45912* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥) | ||
Theorem | mbfres2cn 45913 | 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 25693 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ MblFn) & ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ MblFn) & ⊢ (𝜑 → (𝐵 ∪ 𝐶) = 𝐴) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
Theorem | vol0 45914 | The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (vol‘∅) = 0 | ||
Theorem | ditgeqiooicc 45915* | 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 45916 | The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ dom vol → 0 ≤ (vol‘𝐴)) | ||
Theorem | cnbdibl 45917* | A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ (𝜑 → (vol‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐿1) | ||
Theorem | snmbl 45918 | A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → {𝐴} ∈ dom vol) | ||
Theorem | ditgeq3d 45919* | Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐷 = 𝐸) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥) | ||
Theorem | iblempty 45920 | The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ∅ ∈ 𝐿1 | ||
Theorem | iblsplit 45921* | The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈ 𝐿1) | ||
Theorem | volsn 45922 | A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (vol‘{𝐴}) = 0) | ||
Theorem | itgvol0 45923* | 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 45924* | Exercise: the integral of 𝑥 ↦ cos𝑎𝑥 on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → ∫(𝐵(,)𝐶)(cos‘(𝐴 · 𝑥)) d𝑥 = (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴)) | ||
Theorem | iblsplitf 45925* | A version of iblsplit 45921 using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) & ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈ 𝐿1) | ||
Theorem | ibliooicc 45926* | 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 45927 | The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,]𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | iblspltprt 45928* | 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 45929* | Exercise: the integral of 𝑥 ↦ sin𝑎𝑥 on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → ∫(𝐵(,)𝐶)(sin‘(𝐴 · 𝑥)) d𝑥 = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) | ||
Theorem | itgsubsticclem 45930* | lemma for itgsubsticc 45931. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑢 ∈ (𝐾[,]𝐿) ↦ 𝐶) & ⊢ 𝐺 = (𝑢 ∈ ℝ ↦ if(𝑢 ∈ (𝐾[,]𝐿), (𝐹‘𝑢), if(𝑢 < 𝐾, (𝐹‘𝐾), (𝐹‘𝐿)))) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝐾[,]𝐿))) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾[,]𝐿)–cn→ℂ)) & ⊢ (𝜑 → 𝐾 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → 𝐾 ≤ 𝐿) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) & ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) & ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) ⇒ ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) | ||
Theorem | itgsubsticc 45931* | Integration by u-substitution. The main difference with respect to itgsubst 26104 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 45932* | 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 45933 | 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 45934* | The ∫ integral splits on a given partition 𝑃. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ (𝜑 → 𝑃:(𝑀...𝑁)⟶ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) & ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ⇒ ⊢ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) | ||
Theorem | itgiccshift 45935* | 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 45936* | 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 45937* | Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) ⇒ ⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡) | ||
Theorem | volico 45938 | The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0)) | ||
Theorem | sublevolico 45939 | 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 45940 | Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ dom vol ⊆ 𝒫 ℝ | ||
Theorem | ismbl3 45941* | The predicate "𝐴 is Lebesgue-measurable". Similar to ismbl2 25575, 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 45942 | The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (vol ∘ (,)):(ℝ* × ℝ*)⟶(0[,]+∞) | ||
Theorem | ovolsplit 45943 | 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 45944 | 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 45945 | The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) = if(𝐴 ≤ 𝐵, (𝐵 − 𝐴), 0)) | ||
Theorem | fvvolicof 45946 | 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 45947 | 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 45948* | The predicate "𝐴 is Lebesgue-measurable". Similar to ismbl 25574, 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 45949* | ((vol ∘ (,)) ∘ 𝐹) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶(ℝ* × ℝ*)) ⇒ ⊢ (𝜑 → ((vol ∘ (,)) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (vol‘((1st ‘(𝐹‘𝑥))(,)(2nd ‘(𝐹‘𝑥)))))) | ||
Theorem | volicoff 45950 | ((vol ∘ [,)) ∘ 𝐹) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶(ℝ × ℝ*)) ⇒ ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹):𝐴⟶(0[,]+∞)) | ||
Theorem | voliooicof 45951 | 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 45952* | ((vol ∘ [,)) ∘ 𝐹) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶(ℝ × ℝ*)) ⇒ ⊢ (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (vol‘((1st ‘(𝐹‘𝑥))[,)(2nd ‘(𝐹‘𝑥)))))) | ||
Theorem | volicc 45953 | The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | voliccico 45954 | 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 45955 | The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝐹 ∈ MblFn → dom 𝐹 ⊆ ℝ) | ||
Theorem | stoweidlem1 45956 | Lemma for stoweid 46018. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 14264. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 1) & ⊢ (𝜑 → 𝐷 ≤ 𝐴) ⇒ ⊢ (𝜑 → ((1 − (𝐴↑𝑁))↑(𝐾↑𝑁)) ≤ (1 / ((𝐾 · 𝐷)↑𝑁))) | ||
Theorem | stoweidlem2 45957* | lemma for stoweid 46018: 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 45958* | Lemma for stoweid 46018: 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 45959* | Lemma for stoweid 46018: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝐵) ∈ 𝐴) | ||
Theorem | stoweidlem5 45960* | 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 45961* | Lemma for stoweid 46018: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ Ⅎ𝑡 𝑓 = 𝐹 & ⊢ Ⅎ𝑡 𝑔 = 𝐺 & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) · (𝐺‘𝑡))) ∈ 𝐴) | ||
Theorem | stoweidlem7 45962* | 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 45963* | Lemma for stoweid 46018: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) & ⊢ Ⅎ𝑡𝐹 & ⊢ Ⅎ𝑡𝐺 ⇒ ⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) + (𝐺‘𝑡))) ∈ 𝐴) | ||
Theorem | stoweidlem9 45964* | Lemma for stoweid 46018: 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 45965 | Lemma for stoweid 46018. 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 45966* | 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 45967* | Lemma for stoweid 46018. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) & ⊢ (𝜑 → 𝑃:𝑇⟶ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑄‘𝑡) = ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | ||
Theorem | stoweidlem13 45968 | Lemma for stoweid 46018. 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 45969* | 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 45970* | 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 45971* | Lemma for stoweid 46018. 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 45972* | 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 45973* | 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 45974* | 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 45975* | 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 45976* | 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 45977* | 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 45978* | 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 45979* | 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 45980* | 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 45981* | 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 45982* | 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 45983* | 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 45984* | 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 45985* | 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 45986* | 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 45987* | 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 45988* | 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 45989* | 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 45990* | 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 45991* | 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 45992* | 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 45993* | 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 45994* | 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 45995* | 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 45996* | 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 45997* | 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 45998* | 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 45999* | 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 46000* | 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 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |