stoweidlem41

Description: 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 - q_n". Here E is used to represent ε in the paper, and y to represent q_n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem41.1	$⊢ Ⅎ t φ$
	stoweidlem41.2	$⊢ X = (t \in T ⟼ 1 - y (t))$
	stoweidlem41.3	$⊢ F = (t \in T ⟼ 1)$
	stoweidlem41.4	$⊢ V \subseteq T$
	stoweidlem41.5	$⊢ φ \to y \in A$
	stoweidlem41.6	$⊢ φ \to y : T ⟶ ℝ$
	stoweidlem41.7	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem41.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem41.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem41.10	$⊢ (φ \land w \in ℝ) \to (t \in T ⟼ w) \in A$
	stoweidlem41.11	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem41.12	$⊢ φ \to \forall t \in T (0 \leq y (t) \land y (t) \leq 1)$
	stoweidlem41.13	$⊢ φ \to \forall t \in V 1 - E < y (t)$
	stoweidlem41.14	$⊢ φ \to \forall t \in (T ∖ U) y (t) < E$
Assertion	stoweidlem41	$⊢ φ \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < E \land \forall t \in (T ∖ U) 1 - E < x (t))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem41.1	$⊢ Ⅎ t φ$
2		stoweidlem41.2	$⊢ X = (t \in T ⟼ 1 - y (t))$
3		stoweidlem41.3	$⊢ F = (t \in T ⟼ 1)$
4		stoweidlem41.4	$⊢ V \subseteq T$
5		stoweidlem41.5	$⊢ φ \to y \in A$
6		stoweidlem41.6	$⊢ φ \to y : T ⟶ ℝ$
7		stoweidlem41.7	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
8		stoweidlem41.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
9		stoweidlem41.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
10		stoweidlem41.10	$⊢ (φ \land w \in ℝ) \to (t \in T ⟼ w) \in A$
11		stoweidlem41.11	$⊢ φ \to E \in ℝ^{+}$
12		stoweidlem41.12	$⊢ φ \to \forall t \in T (0 \leq y (t) \land y (t) \leq 1)$
13		stoweidlem41.13	$⊢ φ \to \forall t \in V 1 - E < y (t)$
14		stoweidlem41.14	$⊢ φ \to \forall t \in (T ∖ U) y (t) < E$
15		1re	$⊢ 1 \in ℝ$
16	3	fvmpt2	$⊢ (t \in T \land 1 \in ℝ) \to F (t) = 1$
17	15 16	mpan2	$⊢ t \in T \to F (t) = 1$
18	17	adantl	$⊢ (φ \land t \in T) \to F (t) = 1$
19	18	oveq1d	$⊢ (φ \land t \in T) \to F (t) - y (t) = 1 - y (t)$
20	1 19	mpteq2da	$⊢ φ \to (t \in T ⟼ F (t) - y (t)) = (t \in T ⟼ 1 - y (t))$
21	20 2	eqtr4di	$⊢ φ \to (t \in T ⟼ F (t) - y (t)) = X$
22	10	stoweidlem4	$⊢ (φ \land 1 \in ℝ) \to (t \in T ⟼ 1) \in A$
23	15 22	mpan2	$⊢ φ \to (t \in T ⟼ 1) \in A$
24	3 23	eqeltrid	$⊢ φ \to F \in A$
25		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ 1)$
26	3 25	nfcxfr	$⊢ \underline{Ⅎ} t F$
27		nfcv	$⊢ \underline{Ⅎ} t y$
28	26 27 1 7 8 9 10	stoweidlem33	$⊢ (φ \land F \in A \land y \in A) \to (t \in T ⟼ F (t) - y (t)) \in A$
29	24 5 28	mpd3an23	$⊢ φ \to (t \in T ⟼ F (t) - y (t)) \in A$
30	21 29	eqeltrrd	$⊢ φ \to X \in A$
31	6	ffvelrnda	$⊢ (φ \land t \in T) \to y (t) \in ℝ$
32		1red	$⊢ (φ \land t \in T) \to 1 \in ℝ$
33		0red	$⊢ (φ \land t \in T) \to 0 \in ℝ$
34	12	r19.21bi	$⊢ (φ \land t \in T) \to (0 \leq y (t) \land y (t) \leq 1)$
35	34	simprd	$⊢ (φ \land t \in T) \to y (t) \leq 1$
36		1m0e1	$⊢ 1 - 0 = 1$
37	35 36	breqtrrdi	$⊢ (φ \land t \in T) \to y (t) \leq 1 - 0$
38	31 32 33 37	lesubd	$⊢ (φ \land t \in T) \to 0 \leq 1 - y (t)$
39		simpr	$⊢ (φ \land t \in T) \to t \in T$
40	32 31	resubcld	$⊢ (φ \land t \in T) \to 1 - y (t) \in ℝ$
41	2	fvmpt2	$⊢ (t \in T \land 1 - y (t) \in ℝ) \to X (t) = 1 - y (t)$
42	39 40 41	syl2anc	$⊢ (φ \land t \in T) \to X (t) = 1 - y (t)$
43	38 42	breqtrrd	$⊢ (φ \land t \in T) \to 0 \leq X (t)$
44	34	simpld	$⊢ (φ \land t \in T) \to 0 \leq y (t)$
45	33 31 32 44	lesub2dd	$⊢ (φ \land t \in T) \to 1 - y (t) \leq 1 - 0$
46	45 36	breqtrdi	$⊢ (φ \land t \in T) \to 1 - y (t) \leq 1$
47	42 46	eqbrtrd	$⊢ (φ \land t \in T) \to X (t) \leq 1$
48	43 47	jca	$⊢ (φ \land t \in T) \to (0 \leq X (t) \land X (t) \leq 1)$
49	48	ex	$⊢ φ \to (t \in T \to (0 \leq X (t) \land X (t) \leq 1))$
50	1 49	ralrimi	$⊢ φ \to \forall t \in T (0 \leq X (t) \land X (t) \leq 1)$
51	4	sseli	$⊢ t \in V \to t \in T$
52	51 42	sylan2	$⊢ (φ \land t \in V) \to X (t) = 1 - y (t)$
53		1red	$⊢ (φ \land t \in V) \to 1 \in ℝ$
54	11	rpred	$⊢ φ \to E \in ℝ$
55	54	adantr	$⊢ (φ \land t \in V) \to E \in ℝ$
56	51 31	sylan2	$⊢ (φ \land t \in V) \to y (t) \in ℝ$
57	13	r19.21bi	$⊢ (φ \land t \in V) \to 1 - E < y (t)$
58	53 55 56 57	ltsub23d	$⊢ (φ \land t \in V) \to 1 - y (t) < E$
59	52 58	eqbrtrd	$⊢ (φ \land t \in V) \to X (t) < E$
60	59	ex	$⊢ φ \to (t \in V \to X (t) < E)$
61	1 60	ralrimi	$⊢ φ \to \forall t \in V X (t) < E$
62		eldifi	$⊢ t \in (T ∖ U) \to t \in T$
63	62 31	sylan2	$⊢ (φ \land t \in (T ∖ U)) \to y (t) \in ℝ$
64	54	adantr	$⊢ (φ \land t \in (T ∖ U)) \to E \in ℝ$
65		1red	$⊢ (φ \land t \in (T ∖ U)) \to 1 \in ℝ$
66	14	r19.21bi	$⊢ (φ \land t \in (T ∖ U)) \to y (t) < E$
67	63 64 65 66	ltsub2dd	$⊢ (φ \land t \in (T ∖ U)) \to 1 - E < 1 - y (t)$
68	62 42	sylan2	$⊢ (φ \land t \in (T ∖ U)) \to X (t) = 1 - y (t)$
69	67 68	breqtrrd	$⊢ (φ \land t \in (T ∖ U)) \to 1 - E < X (t)$
70	69	ex	$⊢ φ \to (t \in (T ∖ U) \to 1 - E < X (t))$
71	1 70	ralrimi	$⊢ φ \to \forall t \in (T ∖ U) 1 - E < X (t)$
72		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ 1 - y (t))$
73	2 72	nfcxfr	$⊢ \underline{Ⅎ} t X$
74	73	nfeq2	$⊢ Ⅎ t x = X$
75		fveq1	$⊢ x = X \to x (t) = X (t)$
76	75	breq2d	$⊢ x = X \to (0 \leq x (t) \leftrightarrow 0 \leq X (t))$
77	75	breq1d	$⊢ x = X \to (x (t) \leq 1 \leftrightarrow X (t) \leq 1)$
78	76 77	anbi12d	$⊢ x = X \to ((0 \leq x (t) \land x (t) \leq 1) \leftrightarrow (0 \leq X (t) \land X (t) \leq 1))$
79	74 78	ralbid	$⊢ x = X \to (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq X (t) \land X (t) \leq 1))$
80	75	breq1d	$⊢ x = X \to (x (t) < E \leftrightarrow X (t) < E)$
81	74 80	ralbid	$⊢ x = X \to (\forall t \in V x (t) < E \leftrightarrow \forall t \in V X (t) < E)$
82	75	breq2d	$⊢ x = X \to (1 - E < x (t) \leftrightarrow 1 - E < X (t))$
83	74 82	ralbid	$⊢ x = X \to (\forall t \in (T ∖ U) 1 - E < x (t) \leftrightarrow \forall t \in (T ∖ U) 1 - E < X (t))$
84	79 81 83	3anbi123d	$⊢ x = X \to ((\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < E \land \forall t \in (T ∖ U) 1 - E < x (t)) \leftrightarrow (\forall t \in T (0 \leq X (t) \land X (t) \leq 1) \land \forall t \in V X (t) < E \land \forall t \in (T ∖ U) 1 - E < X (t)))$
85	84	rspcev	$⊢ (X \in A \land (\forall t \in T (0 \leq X (t) \land X (t) \leq 1) \land \forall t \in V X (t) < E \land \forall t \in (T ∖ U) 1 - E < X (t))) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < E \land \forall t \in (T ∖ U) 1 - E < x (t))$
86	30 50 61 71 85	syl13anc	$⊢ φ \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in V x (t) < E \land \forall t \in (T ∖ U) 1 - E < x (t))$

Metamath Proof Explorer

Theorem stoweidlem41

Proof