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 ⊢ Ⅎ 𝑡 𝐹
stoweidlem61.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem61.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem61.4 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem61.5 ⊢ 𝑇 = ∪ 𝐽
stoweidlem61.6 ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
stoweidlem61.7 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
stoweidlem61.8 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
stoweidlem61.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem61.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem61.11 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem61.12 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
stoweidlem61.13 ⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
stoweidlem61.14 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 0 ≤ ( 𝐹 ‘ 𝑡 ) )
stoweidlem61.15 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem61.16 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
Assertion stoweidlem61 ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < ( 2 · 𝐸 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem61.1 ⊢ Ⅎ 𝑡 𝐹
2 stoweidlem61.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem61.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 stoweidlem61.4 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
5 stoweidlem61.5 ⊢ 𝑇 = ∪ 𝐽
6 stoweidlem61.6 ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
7 stoweidlem61.7 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
8 stoweidlem61.8 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
9 stoweidlem61.9 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10 stoweidlem61.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11 stoweidlem61.11 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
12 stoweidlem61.12 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
13 stoweidlem61.13 ⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
14 stoweidlem61.14 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 0 ≤ ( 𝐹 ‘ 𝑡 ) )
15 stoweidlem61.15 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
16 stoweidlem61.16 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
17 eqid ⊢ ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ) = ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
18 eqid ⊢ ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ) = ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
19 1 2 3 5 7 17 18 4 6 8 9 10 11 12 13 14 15 16 stoweidlem60 ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) )
20 nfv ⊢ Ⅎ 𝑡 𝑔 ∈ 𝐴
21 2 20 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑔 ∈ 𝐴 )
22 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐸 ∈ ℝ+ )
23 3 5 7 13 fcnre ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
24 23 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
25 24 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
26 8 sselda ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ∈ 𝐶 )
27 3 5 7 26 fcnre ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → 𝑔 : 𝑇 ⟶ ℝ )
28 27 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ )
29 simpll1 ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → 𝐸 ∈ ℝ+ )
30 simpll2 ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
31 simpll3 ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ )
32 simplr ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → 𝑗 ∈ ℝ )
33 simprll ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) )
34 simprlr ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) )
35 simprrr ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) )
36 simprrl ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
37 29 30 31 32 33 34 35 36 stoweidlem13 ⊢ ( ( ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) → ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < ( 2 · 𝐸 ) )
38 37 rexlimdva2 ⊢ ( ( 𝐸 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℝ ) → ( ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < ( 2 · 𝐸 ) ) )
39 22 25 28 38 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < ( 2 · 𝐸 ) ) )
40 21 39 ralimdaa ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐴 ) → ( ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < ( 2 · 𝐸 ) ) )
41 40 reximdva ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < ( 2 · 𝐸 ) ) )
42 19 41 mpd ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑔 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < ( 2 · 𝐸 ) )