Metamath Proof Explorer

Theorem stoweidlem61

Description: This lemma proves that there exists a function g as in the proof in BrosowskiDeutsh p. 92: g is in the subalgebra, and for all t in T , abs( f(t) - g(t) ) < 2*ε. Here F is used to represent f in the paper, and E is used to represent ε. For this lemma there's the further assumption that the function F to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem61.1 ⊢ Ⅎ _ t F
stoweidlem61.2 ⊢ Ⅎ t φ
stoweidlem61.3 ⊢ K = topGen ⁡ ran ⁡ .
stoweidlem61.4 ⊢ φ → J ∈ Comp
stoweidlem61.5 ⊢ T = ⋃ J
stoweidlem61.6 ⊢ φ → T ≠ ∅
stoweidlem61.7 ⊢ C = J Cn K
stoweidlem61.8 ⊢ φ → A ⊆ C
stoweidlem61.9 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A
stoweidlem61.10 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A
stoweidlem61.11 ⊢ φ ∧ x ∈ ℝ → t ∈ T ⟼ x ∈ A
stoweidlem61.12 ⊢ φ ∧ r ∈ T ∧ t ∈ T ∧ r ≠ t → ∃ q ∈ A q ⁡ r ≠ q ⁡ t
stoweidlem61.13 ⊢ φ → F ∈ C
stoweidlem61.14 ⊢ φ → ∀ t ∈ T 0 ≤ F ⁡ t
stoweidlem61.15 ⊢ φ → E ∈ ℝ +
stoweidlem61.16 ⊢ φ → E < 1 3
Assertion stoweidlem61 ⊢ φ → ∃ g ∈ A ∀ t ∈ T g ⁡ t − F ⁡ t < 2 ⁢ E

Proof

Step Hyp Ref Expression
1 stoweidlem61.1 ⊢ Ⅎ _ t F
2 stoweidlem61.2 ⊢ Ⅎ t φ
3 stoweidlem61.3 ⊢ K = topGen ⁡ ran ⁡ .
4 stoweidlem61.4 ⊢ φ → J ∈ Comp
5 stoweidlem61.5 ⊢ T = ⋃ J
6 stoweidlem61.6 ⊢ φ → T ≠ ∅
7 stoweidlem61.7 ⊢ C = J Cn K
8 stoweidlem61.8 ⊢ φ → A ⊆ C
9 stoweidlem61.9 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A
10 stoweidlem61.10 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A
11 stoweidlem61.11 ⊢ φ ∧ x ∈ ℝ → t ∈ T ⟼ x ∈ A
12 stoweidlem61.12 ⊢ φ ∧ r ∈ T ∧ t ∈ T ∧ r ≠ t → ∃ q ∈ A q ⁡ r ≠ q ⁡ t
13 stoweidlem61.13 ⊢ φ → F ∈ C
14 stoweidlem61.14 ⊢ φ → ∀ t ∈ T 0 ≤ F ⁡ t
15 stoweidlem61.15 ⊢ φ → E ∈ ℝ +
16 stoweidlem61.16 ⊢ φ → E < 1 3
17 eqid ⊢ j ∈ 0 … n ⟼ t ∈ T | F ⁡ t ≤ j − 1 3 ⁢ E = j ∈ 0 … n ⟼ t ∈ T | F ⁡ t ≤ j − 1 3 ⁢ E
18 eqid ⊢ j ∈ 0 … n ⟼ t ∈ T | j + 1 3 ⁢ E ≤ F ⁡ t = j ∈ 0 … n ⟼ t ∈ T | j + 1 3 ⁢ E ≤ F ⁡ t
19 1 2 3 5 7 17 18 4 6 8 9 10 11 12 13 14 15 16 stoweidlem60 ⊢ φ → ∃ g ∈ A ∀ t ∈ T ∃ j ∈ ℝ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t
20 nfv ⊢ Ⅎ t g ∈ A
21 2 20 nfan ⊢ Ⅎ t φ ∧ g ∈ A
22 15 ad2antrr ⊢ φ ∧ g ∈ A ∧ t ∈ T → E ∈ ℝ +
23 3 5 7 13 fcnre ⊢ φ → F : T ⟶ ℝ
24 23 ffvelcdmda ⊢ φ ∧ t ∈ T → F ⁡ t ∈ ℝ
25 24 adantlr ⊢ φ ∧ g ∈ A ∧ t ∈ T → F ⁡ t ∈ ℝ
26 8 sselda ⊢ φ ∧ g ∈ A → g ∈ C
27 3 5 7 26 fcnre ⊢ φ ∧ g ∈ A → g : T ⟶ ℝ
28 27 ffvelcdmda ⊢ φ ∧ g ∈ A ∧ t ∈ T → g ⁡ t ∈ ℝ
29 simpll1 ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → E ∈ ℝ +
30 simpll2 ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → F ⁡ t ∈ ℝ
31 simpll3 ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → g ⁡ t ∈ ℝ
32 simplr ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → j ∈ ℝ
33 simprll ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → j − 4 3 ⁢ E < F ⁡ t
34 simprlr ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → F ⁡ t ≤ j − 1 3 ⁢ E
35 simprrr ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → j − 4 3 ⁢ E < g ⁡ t
36 simprrl ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → g ⁡ t < j + 1 3 ⁢ E
37 29 30 31 32 33 34 35 36 stoweidlem13 ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ ∧ j ∈ ℝ ∧ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → g ⁡ t − F ⁡ t < 2 ⁢ E
38 37 rexlimdva2 ⊢ E ∈ ℝ + ∧ F ⁡ t ∈ ℝ ∧ g ⁡ t ∈ ℝ → ∃ j ∈ ℝ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → g ⁡ t − F ⁡ t < 2 ⁢ E
39 22 25 28 38 syl3anc ⊢ φ ∧ g ∈ A ∧ t ∈ T → ∃ j ∈ ℝ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → g ⁡ t − F ⁡ t < 2 ⁢ E
40 21 39 ralimdaa ⊢ φ ∧ g ∈ A → ∀ t ∈ T ∃ j ∈ ℝ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → ∀ t ∈ T g ⁡ t − F ⁡ t < 2 ⁢ E
41 40 reximdva ⊢ φ → ∃ g ∈ A ∀ t ∈ T ∃ j ∈ ℝ j − 4 3 ⁢ E < F ⁡ t ∧ F ⁡ t ≤ j − 1 3 ⁢ E ∧ g ⁡ t < j + 1 3 ⁢ E ∧ j − 4 3 ⁢ E < g ⁡ t → ∃ g ∈ A ∀ t ∈ T g ⁡ t − F ⁡ t < 2 ⁢ E
42 19 41 mpd ⊢ φ → ∃ g ∈ A ∀ t ∈ T g ⁡ t − F ⁡ t < 2 ⁢ E