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	$⊢ \underline{Ⅎ} t F$
	stoweidlem61.2	$⊢ Ⅎ t φ$
	stoweidlem61.3	$⊢ K = topGen (ran (.))$
	stoweidlem61.4	$⊢ φ \to J \in Comp$
	stoweidlem61.5	$⊢ T = ⋃ J$
	stoweidlem61.6	$⊢ φ \to T \neq \emptyset$
	stoweidlem61.7	$⊢ C = J Cn K$
	stoweidlem61.8	$⊢ φ \to A \subseteq C$
	stoweidlem61.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem61.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem61.11	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem61.12	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem61.13	$⊢ φ \to F \in C$
	stoweidlem61.14	$⊢ φ \to \forall t \in T 0 \leq F (t)$
	stoweidlem61.15	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem61.16	$⊢ φ \to E < \frac{1}{3}$
Assertion	stoweidlem61	$⊢ φ \to \exists g \in A \forall t \in T \|g (t) - F (t)\| < 2 E$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem61.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem61.2	$⊢ Ⅎ t φ$
3		stoweidlem61.3	$⊢ K = topGen (ran (.))$
4		stoweidlem61.4	$⊢ φ \to J \in Comp$
5		stoweidlem61.5	$⊢ T = ⋃ J$
6		stoweidlem61.6	$⊢ φ \to T \neq \emptyset$
7		stoweidlem61.7	$⊢ C = J Cn K$
8		stoweidlem61.8	$⊢ φ \to A \subseteq C$
9		stoweidlem61.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
10		stoweidlem61.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
11		stoweidlem61.11	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
12		stoweidlem61.12	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
13		stoweidlem61.13	$⊢ φ \to F \in C$
14		stoweidlem61.14	$⊢ φ \to \forall t \in T 0 \leq F (t)$
15		stoweidlem61.15	$⊢ φ \to E \in ℝ^{+}$
16		stoweidlem61.16	$⊢ φ \to E < \frac{1}{3}$
17		eqid	$⊢ (j \in (0 \dots n) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}) = (j \in (0 \dots n) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
18		eqid	$⊢ (j \in (0 \dots n) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}) = (j \in (0 \dots n) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
19	1 2 3 5 7 17 18 4 6 8 9 10 11 12 13 14 15 16	stoweidlem60	$⊢ φ \to \exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))$
20		nfv	$⊢ Ⅎ t g \in A$
21	2 20	nfan	$⊢ Ⅎ t (φ \land g \in A)$
22	15	ad2antrr	$⊢ ((φ \land g \in A) \land t \in T) \to E \in ℝ^{+}$
23	3 5 7 13	fcnre	$⊢ φ \to F : T ⟶ ℝ$
24	23	ffvelcdmda	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
25	24	adantlr	$⊢ ((φ \land g \in A) \land t \in T) \to F (t) \in ℝ$
26	8	sselda	$⊢ (φ \land g \in A) \to g \in C$
27	3 5 7 26	fcnre	$⊢ (φ \land g \in A) \to g : T ⟶ ℝ$
28	27	ffvelcdmda	$⊢ ((φ \land g \in A) \land t \in T) \to g (t) \in ℝ$
29		simpll1	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to E \in ℝ^{+}$
30		simpll2	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to F (t) \in ℝ$
31		simpll3	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to g (t) \in ℝ$
32		simplr	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to j \in ℝ$
33		simprll	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to (j - (\frac{4}{3})) E < F (t)$
34		simprlr	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to F (t) \leq (j - (\frac{1}{3})) E$
35		simprrr	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to (j - (\frac{4}{3})) E < g (t)$
36		simprrl	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to g (t) < (j + (\frac{1}{3})) E$
37	29 30 31 32 33 34 35 36	stoweidlem13	$⊢ (((E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \land j \in ℝ) \land (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t)))) \to \|g (t) - F (t)\| < 2 E$
38	37	rexlimdva2	$⊢ (E \in ℝ^{+} \land F (t) \in ℝ \land g (t) \in ℝ) \to (\exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \|g (t) - F (t)\| < 2 E)$
39	22 25 28 38	syl3anc	$⊢ ((φ \land g \in A) \land t \in T) \to (\exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \|g (t) - F (t)\| < 2 E)$
40	21 39	ralimdaa	$⊢ (φ \land g \in A) \to (\forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \forall t \in T \|g (t) - F (t)\| < 2 E)$
41	40	reximdva	$⊢ φ \to (\exists g \in A \forall t \in T \exists j \in ℝ (((j - (\frac{4}{3})) E < F (t) \land F (t) \leq (j - (\frac{1}{3})) E) \land (g (t) < (j + (\frac{1}{3})) E \land (j - (\frac{4}{3})) E < g (t))) \to \exists g \in A \forall t \in T \|g (t) - F (t)\| < 2 E)$
42	19 41	mpd	$⊢ φ \to \exists g \in A \forall t \in T \|g (t) - F (t)\| < 2 E$

Metamath Proof Explorer

Theorem stoweidlem61

Proof