Metamath Proof Explorer


Theorem stoweidlem17

Description: This lemma proves that the function g (as defined in BrosowskiDeutsh p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem17.1 t φ
stoweidlem17.2 φ N
stoweidlem17.3 φ X : 0 N A
stoweidlem17.4 φ f A g A t T f t + g t A
stoweidlem17.5 φ f A g A t T f t g t A
stoweidlem17.6 φ x t T x A
stoweidlem17.7 φ E
stoweidlem17.8 φ f A f : T
Assertion stoweidlem17 φ t T i = 0 N E X i t A

Proof

Step Hyp Ref Expression
1 stoweidlem17.1 t φ
2 stoweidlem17.2 φ N
3 stoweidlem17.3 φ X : 0 N A
4 stoweidlem17.4 φ f A g A t T f t + g t A
5 stoweidlem17.5 φ f A g A t T f t g t A
6 stoweidlem17.6 φ x t T x A
7 stoweidlem17.7 φ E
8 stoweidlem17.8 φ f A f : T
9 2 nnnn0d φ N 0
10 nn0uz 0 = 0
11 9 10 eleqtrdi φ N 0
12 eluzfz2 N 0 N 0 N
13 11 12 syl φ N 0 N
14 13 ancli φ φ N 0 N
15 eleq1 n = 0 n 0 N 0 0 N
16 15 anbi2d n = 0 φ n 0 N φ 0 0 N
17 oveq2 n = 0 0 n = 0 0
18 17 sumeq1d n = 0 i = 0 n E X i t = i = 0 0 E X i t
19 18 mpteq2dv n = 0 t T i = 0 n E X i t = t T i = 0 0 E X i t
20 19 eleq1d n = 0 t T i = 0 n E X i t A t T i = 0 0 E X i t A
21 16 20 imbi12d n = 0 φ n 0 N t T i = 0 n E X i t A φ 0 0 N t T i = 0 0 E X i t A
22 eleq1 n = m n 0 N m 0 N
23 22 anbi2d n = m φ n 0 N φ m 0 N
24 oveq2 n = m 0 n = 0 m
25 24 sumeq1d n = m i = 0 n E X i t = i = 0 m E X i t
26 25 mpteq2dv n = m t T i = 0 n E X i t = t T i = 0 m E X i t
27 26 eleq1d n = m t T i = 0 n E X i t A t T i = 0 m E X i t A
28 23 27 imbi12d n = m φ n 0 N t T i = 0 n E X i t A φ m 0 N t T i = 0 m E X i t A
29 eleq1 n = m + 1 n 0 N m + 1 0 N
30 29 anbi2d n = m + 1 φ n 0 N φ m + 1 0 N
31 oveq2 n = m + 1 0 n = 0 m + 1
32 31 sumeq1d n = m + 1 i = 0 n E X i t = i = 0 m + 1 E X i t
33 32 mpteq2dv n = m + 1 t T i = 0 n E X i t = t T i = 0 m + 1 E X i t
34 33 eleq1d n = m + 1 t T i = 0 n E X i t A t T i = 0 m + 1 E X i t A
35 30 34 imbi12d n = m + 1 φ n 0 N t T i = 0 n E X i t A φ m + 1 0 N t T i = 0 m + 1 E X i t A
36 eleq1 n = N n 0 N N 0 N
37 36 anbi2d n = N φ n 0 N φ N 0 N
38 oveq2 n = N 0 n = 0 N
39 38 sumeq1d n = N i = 0 n E X i t = i = 0 N E X i t
40 39 mpteq2dv n = N t T i = 0 n E X i t = t T i = 0 N E X i t
41 40 eleq1d n = N t T i = 0 n E X i t A t T i = 0 N E X i t A
42 37 41 imbi12d n = N φ n 0 N t T i = 0 n E X i t A φ N 0 N t T i = 0 N E X i t A
43 0z 0
44 fzsn 0 0 0 = 0
45 43 44 ax-mp 0 0 = 0
46 45 sumeq1i i = 0 0 E X i t = i 0 E X i t
47 46 mpteq2i t T i = 0 0 E X i t = t T i 0 E X i t
48 7 adantr φ t T E
49 48 recnd φ t T E
50 nnz N N
51 nngt0 N 0 < N
52 0re 0
53 nnre N N
54 ltle 0 N 0 < N 0 N
55 52 53 54 sylancr N 0 < N 0 N
56 51 55 mpd N 0 N
57 50 56 jca N N 0 N
58 2 57 syl φ N 0 N
59 43 eluz1i N 0 N 0 N
60 58 59 sylibr φ N 0
61 eluzfz1 N 0 0 0 N
62 60 61 syl φ 0 0 N
63 3 62 ffvelrnd φ X 0 A
64 feq1 f = X 0 f : T X 0 : T
65 64 imbi2d f = X 0 φ f : T φ X 0 : T
66 8 expcom f A φ f : T
67 65 66 vtoclga X 0 A φ X 0 : T
68 63 67 mpcom φ X 0 : T
69 68 ffvelrnda φ t T X 0 t
70 69 recnd φ t T X 0 t
71 49 70 mulcld φ t T E X 0 t
72 fveq2 i = 0 X i = X 0
73 72 fveq1d i = 0 X i t = X 0 t
74 73 oveq2d i = 0 E X i t = E X 0 t
75 74 sumsn 0 E X 0 t i 0 E X i t = E X 0 t
76 43 71 75 sylancr φ t T i 0 E X i t = E X 0 t
77 1 76 mpteq2da φ t T i 0 E X i t = t T E X 0 t
78 47 77 syl5eq φ t T i = 0 0 E X i t = t T E X 0 t
79 1 5 6 8 7 63 stoweidlem2 φ t T E X 0 t A
80 78 79 eqeltrd φ t T i = 0 0 E X i t A
81 80 adantr φ 0 0 N t T i = 0 0 E X i t A
82 eqidd r = t E = E
83 82 cbvmptv r T E = t T E
84 83 eqcomi t T E = r T E
85 simpr φ t T t T
86 84 82 85 48 fvmptd3 φ t T t T E t = E
87 86 oveq1d φ t T t T E t X m + 1 t = E X m + 1 t
88 1 87 mpteq2da φ t T t T E t X m + 1 t = t T E X m + 1 t
89 88 adantr φ m + 1 0 N t T t T E t X m + 1 t = t T E X m + 1 t
90 3 ffvelrnda φ m + 1 0 N X m + 1 A
91 simpl φ m + 1 0 N φ
92 id x = E x = E
93 92 mpteq2dv x = E t T x = t T E
94 93 eleq1d x = E t T x A t T E A
95 94 imbi2d x = E φ t T x A φ t T E A
96 6 expcom x φ t T x A
97 95 96 vtoclga E φ t T E A
98 7 97 mpcom φ t T E A
99 98 adantr φ m + 1 0 N t T E A
100 fveq1 g = X m + 1 g t = X m + 1 t
101 100 oveq2d g = X m + 1 t T E t g t = t T E t X m + 1 t
102 101 mpteq2dv g = X m + 1 t T t T E t g t = t T t T E t X m + 1 t
103 102 eleq1d g = X m + 1 t T t T E t g t A t T t T E t X m + 1 t A
104 103 imbi2d g = X m + 1 φ t T E A t T t T E t g t A φ t T E A t T t T E t X m + 1 t A
105 83 eleq1i r T E A t T E A
106 fveq1 f = r T E f t = r T E t
107 83 fveq1i r T E t = t T E t
108 106 107 syl6eq f = r T E f t = t T E t
109 108 oveq1d f = r T E f t g t = t T E t g t
110 109 mpteq2dv f = r T E t T f t g t = t T t T E t g t
111 110 eleq1d f = r T E t T f t g t A t T t T E t g t A
112 111 imbi2d f = r T E φ g A t T f t g t A φ g A t T t T E t g t A
113 5 3com12 f A φ g A t T f t g t A
114 113 3expib f A φ g A t T f t g t A
115 112 114 vtoclga r T E A φ g A t T t T E t g t A
116 105 115 sylbir t T E A φ g A t T t T E t g t A
117 116 3impib t T E A φ g A t T t T E t g t A
118 117 3com13 g A φ t T E A t T t T E t g t A
119 118 3expib g A φ t T E A t T t T E t g t A
120 104 119 vtoclga X m + 1 A φ t T E A t T t T E t X m + 1 t A
121 120 3impib X m + 1 A φ t T E A t T t T E t X m + 1 t A
122 90 91 99 121 syl3anc φ m + 1 0 N t T t T E t X m + 1 t A
123 89 122 eqeltrrd φ m + 1 0 N t T E X m + 1 t A
124 123 ad2antll m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N t T E X m + 1 t A
125 simprrl m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N φ
126 simpl m 0 φ m + 1 0 N m 0
127 simprl m 0 φ m + 1 0 N φ
128 2 ad2antrl m 0 φ m + 1 0 N N
129 128 nnnn0d m 0 φ m + 1 0 N N 0
130 nn0re m 0 m
131 130 adantr m 0 φ m + 1 0 N m
132 peano2nn0 m 0 m + 1 0
133 132 nn0red m 0 m + 1
134 133 adantr m 0 φ m + 1 0 N m + 1
135 2 nnred φ N
136 135 ad2antrl m 0 φ m + 1 0 N N
137 lep1 m m m + 1
138 126 130 137 3syl m 0 φ m + 1 0 N m m + 1
139 elfzle2 m + 1 0 N m + 1 N
140 139 ad2antll m 0 φ m + 1 0 N m + 1 N
141 131 134 136 138 140 letrd m 0 φ m + 1 0 N m N
142 elfz2nn0 m 0 N m 0 N 0 m N
143 126 129 141 142 syl3anbrc m 0 φ m + 1 0 N m 0 N
144 126 127 143 jca32 m 0 φ m + 1 0 N m 0 φ m 0 N
145 144 adantl m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N m 0 φ m 0 N
146 pm3.31 m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m 0 N t T i = 0 m E X i t A
147 146 adantr m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N m 0 φ m 0 N t T i = 0 m E X i t A
148 145 147 mpd m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N t T i = 0 m E X i t A
149 fveq2 r = t X m + 1 r = X m + 1 t
150 149 oveq2d r = t E X m + 1 r = E X m + 1 t
151 150 cbvmptv r T E X m + 1 r = t T E X m + 1 t
152 151 eleq1i r T E X m + 1 r A t T E X m + 1 t A
153 fveq1 g = r T E X m + 1 r g t = r T E X m + 1 r t
154 151 fveq1i r T E X m + 1 r t = t T E X m + 1 t t
155 153 154 syl6eq g = r T E X m + 1 r g t = t T E X m + 1 t t
156 155 oveq2d g = r T E X m + 1 r t T i = 0 m E X i t t + g t = t T i = 0 m E X i t t + t T E X m + 1 t t
157 156 mpteq2dv g = r T E X m + 1 r t T t T i = 0 m E X i t t + g t = t T t T i = 0 m E X i t t + t T E X m + 1 t t
158 157 eleq1d g = r T E X m + 1 r t T t T i = 0 m E X i t t + g t A t T t T i = 0 m E X i t t + t T E X m + 1 t t A
159 158 imbi2d g = r T E X m + 1 r φ t T i = 0 m E X i t A t T t T i = 0 m E X i t t + g t A φ t T i = 0 m E X i t A t T t T i = 0 m E X i t t + t T E X m + 1 t t A
160 fveq2 r = t X i r = X i t
161 160 oveq2d r = t E X i r = E X i t
162 161 sumeq2sdv r = t i = 0 m E X i r = i = 0 m E X i t
163 162 cbvmptv r T i = 0 m E X i r = t T i = 0 m E X i t
164 163 eleq1i r T i = 0 m E X i r A t T i = 0 m E X i t A
165 fveq1 f = r T i = 0 m E X i r f t = r T i = 0 m E X i r t
166 163 fveq1i r T i = 0 m E X i r t = t T i = 0 m E X i t t
167 165 166 syl6eq f = r T i = 0 m E X i r f t = t T i = 0 m E X i t t
168 167 oveq1d f = r T i = 0 m E X i r f t + g t = t T i = 0 m E X i t t + g t
169 168 mpteq2dv f = r T i = 0 m E X i r t T f t + g t = t T t T i = 0 m E X i t t + g t
170 169 eleq1d f = r T i = 0 m E X i r t T f t + g t A t T t T i = 0 m E X i t t + g t A
171 170 imbi2d f = r T i = 0 m E X i r φ g A t T f t + g t A φ g A t T t T i = 0 m E X i t t + g t A
172 4 3com12 f A φ g A t T f t + g t A
173 172 3expib f A φ g A t T f t + g t A
174 171 173 vtoclga r T i = 0 m E X i r A φ g A t T t T i = 0 m E X i t t + g t A
175 164 174 sylbir t T i = 0 m E X i t A φ g A t T t T i = 0 m E X i t t + g t A
176 175 3impib t T i = 0 m E X i t A φ g A t T t T i = 0 m E X i t t + g t A
177 176 3com13 g A φ t T i = 0 m E X i t A t T t T i = 0 m E X i t t + g t A
178 177 3expib g A φ t T i = 0 m E X i t A t T t T i = 0 m E X i t t + g t A
179 159 178 vtoclga r T E X m + 1 r A φ t T i = 0 m E X i t A t T t T i = 0 m E X i t t + t T E X m + 1 t t A
180 152 179 sylbir t T E X m + 1 t A φ t T i = 0 m E X i t A t T t T i = 0 m E X i t t + t T E X m + 1 t t A
181 180 3impib t T E X m + 1 t A φ t T i = 0 m E X i t A t T t T i = 0 m E X i t t + t T E X m + 1 t t A
182 124 125 148 181 syl3anc m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N t T t T i = 0 m E X i t t + t T E X m + 1 t t A
183 3anass m 0 φ m + 1 0 N m 0 φ m + 1 0 N
184 183 biimpri m 0 φ m + 1 0 N m 0 φ m + 1 0 N
185 184 adantl m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N m 0 φ m + 1 0 N
186 nfv t m 0
187 nfv t m + 1 0 N
188 186 1 187 nf3an t m 0 φ m + 1 0 N
189 simpr m 0 φ m + 1 0 N t T t T
190 fzfid m 0 φ m + 1 0 N t T 0 m Fin
191 7 3ad2ant2 m 0 φ m + 1 0 N E
192 191 adantr m 0 φ m + 1 0 N t T E
193 192 adantr m 0 φ m + 1 0 N t T i 0 m E
194 fzelp1 i 0 m i 0 m + 1
195 194 anim2i m 0 φ m + 1 0 N t T i 0 m m 0 φ m + 1 0 N t T i 0 m + 1
196 an32 m 0 φ m + 1 0 N t T i 0 m + 1 m 0 φ m + 1 0 N i 0 m + 1 t T
197 195 196 sylib m 0 φ m + 1 0 N t T i 0 m m 0 φ m + 1 0 N i 0 m + 1 t T
198 3 3ad2ant2 m 0 φ m + 1 0 N X : 0 N A
199 198 adantr m 0 φ m + 1 0 N i 0 m + 1 X : 0 N A
200 elfzuz3 m + 1 0 N N m + 1
201 fzss2 N m + 1 0 m + 1 0 N
202 200 201 syl m + 1 0 N 0 m + 1 0 N
203 202 sselda m + 1 0 N i 0 m + 1 i 0 N
204 203 3ad2antl3 m 0 φ m + 1 0 N i 0 m + 1 i 0 N
205 199 204 ffvelrnd m 0 φ m + 1 0 N i 0 m + 1 X i A
206 simpl2 m 0 φ m + 1 0 N i 0 m + 1 φ
207 feq1 f = X i f : T X i : T
208 207 imbi2d f = X i φ f : T φ X i : T
209 208 66 vtoclga X i A φ X i : T
210 205 206 209 sylc m 0 φ m + 1 0 N i 0 m + 1 X i : T
211 210 ffvelrnda m 0 φ m + 1 0 N i 0 m + 1 t T X i t
212 197 211 syl m 0 φ m + 1 0 N t T i 0 m X i t
213 193 212 remulcld m 0 φ m + 1 0 N t T i 0 m E X i t
214 190 213 fsumrecl m 0 φ m + 1 0 N t T i = 0 m E X i t
215 eqid t T i = 0 m E X i t = t T i = 0 m E X i t
216 215 fvmpt2 t T i = 0 m E X i t t T i = 0 m E X i t t = i = 0 m E X i t
217 189 214 216 syl2anc m 0 φ m + 1 0 N t T t T i = 0 m E X i t t = i = 0 m E X i t
218 217 oveq1d m 0 φ m + 1 0 N t T t T i = 0 m E X i t t + E X m + 1 t = i = 0 m E X i t + E X m + 1 t
219 3simpc m 0 φ m + 1 0 N φ m + 1 0 N
220 219 adantr m 0 φ m + 1 0 N t T φ m + 1 0 N
221 feq1 f = X m + 1 f : T X m + 1 : T
222 221 imbi2d f = X m + 1 φ f : T φ X m + 1 : T
223 222 66 vtoclga X m + 1 A φ X m + 1 : T
224 90 91 223 sylc φ m + 1 0 N X m + 1 : T
225 220 224 syl m 0 φ m + 1 0 N t T X m + 1 : T
226 225 189 ffvelrnd m 0 φ m + 1 0 N t T X m + 1 t
227 192 226 remulcld m 0 φ m + 1 0 N t T E X m + 1 t
228 eqid t T E X m + 1 t = t T E X m + 1 t
229 228 fvmpt2 t T E X m + 1 t t T E X m + 1 t t = E X m + 1 t
230 189 227 229 syl2anc m 0 φ m + 1 0 N t T t T E X m + 1 t t = E X m + 1 t
231 230 oveq2d m 0 φ m + 1 0 N t T t T i = 0 m E X i t t + t T E X m + 1 t t = t T i = 0 m E X i t t + E X m + 1 t
232 elfzuz m + 1 0 N m + 1 0
233 232 3ad2ant3 m 0 φ m + 1 0 N m + 1 0
234 233 adantr m 0 φ m + 1 0 N t T m + 1 0
235 192 adantr m 0 φ m + 1 0 N t T i 0 m + 1 E
236 211 an32s m 0 φ m + 1 0 N t T i 0 m + 1 X i t
237 remulcl E X i t E X i t
238 237 recnd E X i t E X i t
239 235 236 238 syl2anc m 0 φ m + 1 0 N t T i 0 m + 1 E X i t
240 fveq2 i = m + 1 X i = X m + 1
241 240 fveq1d i = m + 1 X i t = X m + 1 t
242 241 oveq2d i = m + 1 E X i t = E X m + 1 t
243 234 239 242 fsumm1 m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t = i = 0 m + 1 - 1 E X i t + E X m + 1 t
244 nn0cn m 0 m
245 244 3ad2ant1 m 0 φ m + 1 0 N m
246 245 adantr m 0 φ m + 1 0 N t T m
247 1cnd m 0 φ m + 1 0 N t T 1
248 246 247 pncand m 0 φ m + 1 0 N t T m + 1 - 1 = m
249 248 oveq2d m 0 φ m + 1 0 N t T 0 m + 1 - 1 = 0 m
250 249 sumeq1d m 0 φ m + 1 0 N t T i = 0 m + 1 - 1 E X i t = i = 0 m E X i t
251 250 oveq1d m 0 φ m + 1 0 N t T i = 0 m + 1 - 1 E X i t + E X m + 1 t = i = 0 m E X i t + E X m + 1 t
252 243 251 eqtrd m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t = i = 0 m E X i t + E X m + 1 t
253 218 231 252 3eqtr4rd m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t = t T i = 0 m E X i t t + t T E X m + 1 t t
254 188 253 mpteq2da m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t = t T t T i = 0 m E X i t t + t T E X m + 1 t t
255 254 eleq1d m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t A t T t T i = 0 m E X i t t + t T E X m + 1 t t A
256 185 255 syl m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t A t T t T i = 0 m E X i t t + t T E X m + 1 t t A
257 182 256 mpbird m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t A
258 257 exp32 m 0 φ m 0 N t T i = 0 m E X i t A m 0 φ m + 1 0 N t T i = 0 m + 1 E X i t A
259 258 pm2.86i m 0 φ m 0 N t T i = 0 m E X i t A φ m + 1 0 N t T i = 0 m + 1 E X i t A
260 21 28 35 42 81 259 nn0ind N 0 φ N 0 N t T i = 0 N E X i t A
261 9 14 260 sylc φ t T i = 0 N E X i t A