Metamath Proof Explorer

Theorem stoweidlem51

Description: There exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent A in the paper, because here A is used for the subalgebra of functions. E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem51.1 ⊢ Ⅎ i φ
stoweidlem51.2 ⊢ Ⅎ t φ
stoweidlem51.3 ⊢ Ⅎ w φ
stoweidlem51.4 ⊢ Ⅎ _ w V
stoweidlem51.5 ⊢ Y = h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
stoweidlem51.6 ⊢ P = f ∈ Y , g ∈ Y ⟼ t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
stoweidlem51.7 ⊢ X = seq 1 P U ⁡ M
stoweidlem51.8 ⊢ F = t ∈ T ⟼ i ∈ 1 … M ⟼ U ⁡ i ⁡ t
stoweidlem51.9 ⊢ Z = t ∈ T ⟼ seq 1 × F ⁡ t ⁡ M
stoweidlem51.10 ⊢ φ → M ∈ ℕ
stoweidlem51.11 ⊢ φ → W : 1 … M ⟶ V
stoweidlem51.12 ⊢ φ → U : 1 … M ⟶ Y
stoweidlem51.13 ⊢ φ ∧ w ∈ V → w ⊆ T
stoweidlem51.14 ⊢ φ → D ⊆ ⋃ ran ⁡ W
stoweidlem51.15 ⊢ φ → D ⊆ T
stoweidlem51.16 ⊢ φ → B ⊆ T
stoweidlem51.17 ⊢ φ ∧ i ∈ 1 … M → ∀ t ∈ W ⁡ i U ⁡ i ⁡ t < E M
stoweidlem51.18 ⊢ φ ∧ i ∈ 1 … M → ∀ t ∈ B 1 − E M < U ⁡ i ⁡ t
stoweidlem51.19 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A
stoweidlem51.20 ⊢ φ ∧ f ∈ A → f : T ⟶ ℝ
stoweidlem51.21 ⊢ φ → T ∈ V
stoweidlem51.22 ⊢ φ → E ∈ ℝ +
stoweidlem51.23 ⊢ φ → E < 1 3
Assertion stoweidlem51 ⊢ φ → ∃ x x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t

Proof

Step Hyp Ref Expression
1 stoweidlem51.1 ⊢ Ⅎ i φ
2 stoweidlem51.2 ⊢ Ⅎ t φ
3 stoweidlem51.3 ⊢ Ⅎ w φ
4 stoweidlem51.4 ⊢ Ⅎ _ w V
5 stoweidlem51.5 ⊢ Y = h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
6 stoweidlem51.6 ⊢ P = f ∈ Y , g ∈ Y ⟼ t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
7 stoweidlem51.7 ⊢ X = seq 1 P U ⁡ M
8 stoweidlem51.8 ⊢ F = t ∈ T ⟼ i ∈ 1 … M ⟼ U ⁡ i ⁡ t
9 stoweidlem51.9 ⊢ Z = t ∈ T ⟼ seq 1 × F ⁡ t ⁡ M
10 stoweidlem51.10 ⊢ φ → M ∈ ℕ
11 stoweidlem51.11 ⊢ φ → W : 1 … M ⟶ V
12 stoweidlem51.12 ⊢ φ → U : 1 … M ⟶ Y
13 stoweidlem51.13 ⊢ φ ∧ w ∈ V → w ⊆ T
14 stoweidlem51.14 ⊢ φ → D ⊆ ⋃ ran ⁡ W
15 stoweidlem51.15 ⊢ φ → D ⊆ T
16 stoweidlem51.16 ⊢ φ → B ⊆ T
17 stoweidlem51.17 ⊢ φ ∧ i ∈ 1 … M → ∀ t ∈ W ⁡ i U ⁡ i ⁡ t < E M
18 stoweidlem51.18 ⊢ φ ∧ i ∈ 1 … M → ∀ t ∈ B 1 − E M < U ⁡ i ⁡ t
19 stoweidlem51.19 ⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A
20 stoweidlem51.20 ⊢ φ ∧ f ∈ A → f : T ⟶ ℝ
21 stoweidlem51.21 ⊢ φ → T ∈ V
22 stoweidlem51.22 ⊢ φ → E ∈ ℝ +
23 stoweidlem51.23 ⊢ φ → E < 1 3
24 ssrab2 ⊢ h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ⊆ A
25 5 24 eqsstri ⊢ Y ⊆ A
26 1zzd ⊢ φ → 1 ∈ ℤ
27 10 nnzd ⊢ φ → M ∈ ℤ
28 26 27 27 3jca ⊢ φ → 1 ∈ ℤ ∧ M ∈ ℤ ∧ M ∈ ℤ
29 10 nnge1d ⊢ φ → 1 ≤ M
30 10 nnred ⊢ φ → M ∈ ℝ
31 30 leidd ⊢ φ → M ≤ M
32 29 31 jca ⊢ φ → 1 ≤ M ∧ M ≤ M
33 elfz2 ⊢ M ∈ 1 … M ↔ 1 ∈ ℤ ∧ M ∈ ℤ ∧ M ∈ ℤ ∧ 1 ≤ M ∧ M ≤ M
34 28 32 33 sylanbrc ⊢ φ → M ∈ 1 … M
35 eqid ⊢ t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t = t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
36 2 5 35 20 19 stoweidlem16 ⊢ φ ∧ f ∈ Y ∧ g ∈ Y → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ Y
37 6 7 34 12 36 21 fmulcl ⊢ φ → X ∈ Y
38 25 37 sseldi ⊢ φ → X ∈ A
39 5 eleq2i ⊢ X ∈ Y ↔ X ∈ h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
40 nfcv ⊢ Ⅎ _ h 1
41 nfrab1 ⊢ Ⅎ _ h h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
42 5 41 nfcxfr ⊢ Ⅎ _ h Y
43 nfcv ⊢ Ⅎ _ h t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
44 42 42 43 nfmpo ⊢ Ⅎ _ h f ∈ Y , g ∈ Y ⟼ t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
45 6 44 nfcxfr ⊢ Ⅎ _ h P
46 nfcv ⊢ Ⅎ _ h U
47 40 45 46 nfseq ⊢ Ⅎ _ h seq 1 P U
48 nfcv ⊢ Ⅎ _ h M
49 47 48 nffv ⊢ Ⅎ _ h seq 1 P U ⁡ M
50 7 49 nfcxfr ⊢ Ⅎ _ h X
51 nfcv ⊢ Ⅎ _ h A
52 nfcv ⊢ Ⅎ _ h T
53 nfcv ⊢ Ⅎ _ h 0
54 nfcv ⊢ Ⅎ _ h ≤
55 nfcv ⊢ Ⅎ _ h t
56 50 55 nffv ⊢ Ⅎ _ h X ⁡ t
57 53 54 56 nfbr ⊢ Ⅎ h 0 ≤ X ⁡ t
58 56 54 40 nfbr ⊢ Ⅎ h X ⁡ t ≤ 1
59 57 58 nfan ⊢ Ⅎ h 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
60 52 59 nfralw ⊢ Ⅎ h ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
61 nfcv ⊢ Ⅎ _ t 1
62 nfra1 ⊢ Ⅎ t ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
63 nfcv ⊢ Ⅎ _ t A
64 62 63 nfrabw ⊢ Ⅎ _ t h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
65 5 64 nfcxfr ⊢ Ⅎ _ t Y
66 nfmpt1 ⊢ Ⅎ _ t t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
67 65 65 66 nfmpo ⊢ Ⅎ _ t f ∈ Y , g ∈ Y ⟼ t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t
68 6 67 nfcxfr ⊢ Ⅎ _ t P
69 nfcv ⊢ Ⅎ _ t U
70 61 68 69 nfseq ⊢ Ⅎ _ t seq 1 P U
71 nfcv ⊢ Ⅎ _ t M
72 70 71 nffv ⊢ Ⅎ _ t seq 1 P U ⁡ M
73 7 72 nfcxfr ⊢ Ⅎ _ t X
74 73 nfeq2 ⊢ Ⅎ t h = X
75 fveq1 ⊢ h = X → h ⁡ t = X ⁡ t
76 75 breq2d ⊢ h = X → 0 ≤ h ⁡ t ↔ 0 ≤ X ⁡ t
77 75 breq1d ⊢ h = X → h ⁡ t ≤ 1 ↔ X ⁡ t ≤ 1
78 76 77 anbi12d ⊢ h = X → 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
79 74 78 ralbid ⊢ h = X → ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
80 50 51 60 79 elrabf ⊢ X ∈ h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ X ∈ A ∧ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
81 39 80 bitri ⊢ X ∈ Y ↔ X ∈ A ∧ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
82 37 81 sylib ⊢ φ → X ∈ A ∧ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
83 82 simprd ⊢ φ → ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
84 nfv ⊢ Ⅎ t i ∈ 1 … M
85 2 84 nfan ⊢ Ⅎ t φ ∧ i ∈ 1 … M
86 12 ffvelrnda ⊢ φ ∧ i ∈ 1 … M → U ⁡ i ∈ Y
87 fveq1 ⊢ h = U ⁡ i → h ⁡ t = U ⁡ i ⁡ t
88 87 breq2d ⊢ h = U ⁡ i → 0 ≤ h ⁡ t ↔ 0 ≤ U ⁡ i ⁡ t
89 87 breq1d ⊢ h = U ⁡ i → h ⁡ t ≤ 1 ↔ U ⁡ i ⁡ t ≤ 1
90 88 89 anbi12d ⊢ h = U ⁡ i → 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ 0 ≤ U ⁡ i ⁡ t ∧ U ⁡ i ⁡ t ≤ 1
91 90 ralbidv ⊢ h = U ⁡ i → ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ ∀ t ∈ T 0 ≤ U ⁡ i ⁡ t ∧ U ⁡ i ⁡ t ≤ 1
92 91 5 elrab2 ⊢ U ⁡ i ∈ Y ↔ U ⁡ i ∈ A ∧ ∀ t ∈ T 0 ≤ U ⁡ i ⁡ t ∧ U ⁡ i ⁡ t ≤ 1
93 92 simplbi ⊢ U ⁡ i ∈ Y → U ⁡ i ∈ A
94 86 93 syl ⊢ φ ∧ i ∈ 1 … M → U ⁡ i ∈ A
95 eleq1 ⊢ f = U ⁡ i → f ∈ A ↔ U ⁡ i ∈ A
96 95 anbi2d ⊢ f = U ⁡ i → φ ∧ f ∈ A ↔ φ ∧ U ⁡ i ∈ A
97 feq1 ⊢ f = U ⁡ i → f : T ⟶ ℝ ↔ U ⁡ i : T ⟶ ℝ
98 96 97 imbi12d ⊢ f = U ⁡ i → φ ∧ f ∈ A → f : T ⟶ ℝ ↔ φ ∧ U ⁡ i ∈ A → U ⁡ i : T ⟶ ℝ
99 20 a1i ⊢ f ∈ A → φ ∧ f ∈ A → f : T ⟶ ℝ
100 98 99 vtoclga ⊢ U ⁡ i ∈ A → φ ∧ U ⁡ i ∈ A → U ⁡ i : T ⟶ ℝ
101 100 anabsi7 ⊢ φ ∧ U ⁡ i ∈ A → U ⁡ i : T ⟶ ℝ
102 94 101 syldan ⊢ φ ∧ i ∈ 1 … M → U ⁡ i : T ⟶ ℝ
103 102 adantr ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → U ⁡ i : T ⟶ ℝ
104 11 ffvelrnda ⊢ φ ∧ i ∈ 1 … M → W ⁡ i ∈ V
105 simpl ⊢ φ ∧ i ∈ 1 … M → φ
106 105 104 jca ⊢ φ ∧ i ∈ 1 … M → φ ∧ W ⁡ i ∈ V
107 4 nfel2 ⊢ Ⅎ w W ⁡ i ∈ V
108 3 107 nfan ⊢ Ⅎ w φ ∧ W ⁡ i ∈ V
109 nfv ⊢ Ⅎ w W ⁡ i ⊆ T
110 108 109 nfim ⊢ Ⅎ w φ ∧ W ⁡ i ∈ V → W ⁡ i ⊆ T
111 eleq1 ⊢ w = W ⁡ i → w ∈ V ↔ W ⁡ i ∈ V
112 111 anbi2d ⊢ w = W ⁡ i → φ ∧ w ∈ V ↔ φ ∧ W ⁡ i ∈ V
113 sseq1 ⊢ w = W ⁡ i → w ⊆ T ↔ W ⁡ i ⊆ T
114 112 113 imbi12d ⊢ w = W ⁡ i → φ ∧ w ∈ V → w ⊆ T ↔ φ ∧ W ⁡ i ∈ V → W ⁡ i ⊆ T
115 110 114 13 vtoclg1f ⊢ W ⁡ i ∈ V → φ ∧ W ⁡ i ∈ V → W ⁡ i ⊆ T
116 104 106 115 sylc ⊢ φ ∧ i ∈ 1 … M → W ⁡ i ⊆ T
117 116 sselda ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → t ∈ T
118 103 117 ffvelrnd ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → U ⁡ i ⁡ t ∈ ℝ
119 22 rpred ⊢ φ → E ∈ ℝ
120 119 ad2antrr ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → E ∈ ℝ
121 30 ad2antrr ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → M ∈ ℝ
122 10 nnne0d ⊢ φ → M ≠ 0
123 122 ad2antrr ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → M ≠ 0
124 120 121 123 redivcld ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → E M ∈ ℝ
125 17 r19.21bi ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → U ⁡ i ⁡ t < E M
126 1red ⊢ φ → 1 ∈ ℝ
127 0lt1 ⊢ 0 < 1
128 127 a1i ⊢ φ → 0 < 1
129 10 nngt0d ⊢ φ → 0 < M
130 22 rpregt0d ⊢ φ → E ∈ ℝ ∧ 0 < E
131 lediv2 ⊢ 1 ∈ ℝ ∧ 0 < 1 ∧ M ∈ ℝ ∧ 0 < M ∧ E ∈ ℝ ∧ 0 < E → 1 ≤ M ↔ E M ≤ E 1
132 126 128 30 129 130 131 syl221anc ⊢ φ → 1 ≤ M ↔ E M ≤ E 1
133 29 132 mpbid ⊢ φ → E M ≤ E 1
134 22 rpcnd ⊢ φ → E ∈ ℂ
135 134 div1d ⊢ φ → E 1 = E
136 133 135 breqtrd ⊢ φ → E M ≤ E
137 136 ad2antrr ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → E M ≤ E
138 118 124 120 125 137 ltletrd ⊢ φ ∧ i ∈ 1 … M ∧ t ∈ W ⁡ i → U ⁡ i ⁡ t < E
139 138 ex ⊢ φ ∧ i ∈ 1 … M → t ∈ W ⁡ i → U ⁡ i ⁡ t < E
140 85 139 ralrimi ⊢ φ ∧ i ∈ 1 … M → ∀ t ∈ W ⁡ i U ⁡ i ⁡ t < E
141 1 2 5 6 7 8 9 10 11 12 14 15 140 21 20 19 22 stoweidlem48 ⊢ φ → ∀ t ∈ D X ⁡ t < E
142 25 sseli ⊢ f ∈ Y → f ∈ A
143 142 20 sylan2 ⊢ φ ∧ f ∈ Y → f : T ⟶ ℝ
144 1 2 65 6 7 8 9 10 12 18 22 23 143 36 21 16 stoweidlem42 ⊢ φ → ∀ t ∈ B 1 − E < X ⁡ t
145 83 141 144 3jca ⊢ φ → ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1 ∧ ∀ t ∈ D X ⁡ t < E ∧ ∀ t ∈ B 1 − E < X ⁡ t
146 38 145 jca ⊢ φ → X ∈ A ∧ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1 ∧ ∀ t ∈ D X ⁡ t < E ∧ ∀ t ∈ B 1 − E < X ⁡ t
147 eleq1 ⊢ x = X → x ∈ A ↔ X ∈ A
148 73 nfeq2 ⊢ Ⅎ t x = X
149 fveq1 ⊢ x = X → x ⁡ t = X ⁡ t
150 149 breq2d ⊢ x = X → 0 ≤ x ⁡ t ↔ 0 ≤ X ⁡ t
151 149 breq1d ⊢ x = X → x ⁡ t ≤ 1 ↔ X ⁡ t ≤ 1
152 150 151 anbi12d ⊢ x = X → 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ↔ 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
153 148 152 ralbid ⊢ x = X → ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ↔ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1
154 149 breq1d ⊢ x = X → x ⁡ t < E ↔ X ⁡ t < E
155 148 154 ralbid ⊢ x = X → ∀ t ∈ D x ⁡ t < E ↔ ∀ t ∈ D X ⁡ t < E
156 149 breq2d ⊢ x = X → 1 − E < x ⁡ t ↔ 1 − E < X ⁡ t
157 148 156 ralbid ⊢ x = X → ∀ t ∈ B 1 − E < x ⁡ t ↔ ∀ t ∈ B 1 − E < X ⁡ t
158 153 155 157 3anbi123d ⊢ x = X → ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t ↔ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1 ∧ ∀ t ∈ D X ⁡ t < E ∧ ∀ t ∈ B 1 − E < X ⁡ t
159 147 158 anbi12d ⊢ x = X → x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t ↔ X ∈ A ∧ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1 ∧ ∀ t ∈ D X ⁡ t < E ∧ ∀ t ∈ B 1 − E < X ⁡ t
160 159 spcegv ⊢ X ∈ A → X ∈ A ∧ ∀ t ∈ T 0 ≤ X ⁡ t ∧ X ⁡ t ≤ 1 ∧ ∀ t ∈ D X ⁡ t < E ∧ ∀ t ∈ B 1 − E < X ⁡ t → ∃ x x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t
161 38 146 160 sylc ⊢ φ → ∃ x x ∈ A ∧ ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t