Metamath Proof Explorer


Theorem breprexplemc

Description: Lemma for breprexp (induction step) (Contributed by Thierry Arnoux, 6-Dec-2021)

Ref Expression
Hypotheses breprexp.n φ N 0
breprexp.s φ S 0
breprexp.z φ Z
breprexp.h φ L : 0 ..^ S
breprexplemc.t φ T 0
breprexplemc.s φ T + 1 S
breprexplemc.1 φ a 0 ..^ T b = 1 N L a b Z b = m = 0 T N d 1 N repr T m a 0 ..^ T L a d a Z m
Assertion breprexplemc φ a 0 ..^ T + 1 b = 1 N L a b Z b = m = 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m

Proof

Step Hyp Ref Expression
1 breprexp.n φ N 0
2 breprexp.s φ S 0
3 breprexp.z φ Z
4 breprexp.h φ L : 0 ..^ S
5 breprexplemc.t φ T 0
6 breprexplemc.s φ T + 1 S
7 breprexplemc.1 φ a 0 ..^ T b = 1 N L a b Z b = m = 0 T N d 1 N repr T m a 0 ..^ T L a d a Z m
8 nn0uz 0 = 0
9 5 8 eleqtrdi φ T 0
10 fzosplitsn T 0 0 ..^ T + 1 = 0 ..^ T T
11 9 10 syl φ 0 ..^ T + 1 = 0 ..^ T T
12 11 prodeq1d φ a 0 ..^ T + 1 b = 1 N L a b Z b = a 0 ..^ T T b = 1 N L a b Z b
13 nfv a φ
14 nfcv _ a b = 1 N L T b Z b
15 fzofi 0 ..^ T Fin
16 15 a1i φ 0 ..^ T Fin
17 fzonel ¬ T 0 ..^ T
18 17 a1i φ ¬ T 0 ..^ T
19 fzfid φ a 0 ..^ T 1 N Fin
20 1 ad2antrr φ a 0 ..^ T b 1 N N 0
21 2 ad2antrr φ a 0 ..^ T b 1 N S 0
22 3 ad2antrr φ a 0 ..^ T b 1 N Z
23 4 adantr φ a 0 ..^ T L : 0 ..^ S
24 23 adantr φ a 0 ..^ T b 1 N L : 0 ..^ S
25 5 nn0zd φ T
26 2 nn0zd φ S
27 5 nn0red φ T
28 1red φ 1
29 27 28 readdcld φ T + 1
30 2 nn0red φ S
31 27 lep1d φ T T + 1
32 27 29 30 31 6 letrd φ T S
33 eluz1 T S T S T S
34 33 biimpar T S T S S T
35 25 26 32 34 syl12anc φ S T
36 fzoss2 S T 0 ..^ T 0 ..^ S
37 35 36 syl φ 0 ..^ T 0 ..^ S
38 37 sselda φ a 0 ..^ T a 0 ..^ S
39 38 adantr φ a 0 ..^ T b 1 N a 0 ..^ S
40 fz1ssnn 1 N
41 40 a1i φ a 0 ..^ T 1 N
42 41 sselda φ a 0 ..^ T b 1 N b
43 20 21 22 24 39 42 breprexplemb φ a 0 ..^ T b 1 N L a b
44 nnssnn0 0
45 40 44 sstri 1 N 0
46 45 a1i φ 1 N 0
47 46 ralrimivw φ a 0 ..^ T 1 N 0
48 47 r19.21bi φ a 0 ..^ T 1 N 0
49 48 sselda φ a 0 ..^ T b 1 N b 0
50 22 49 expcld φ a 0 ..^ T b 1 N Z b
51 43 50 mulcld φ a 0 ..^ T b 1 N L a b Z b
52 19 51 fsumcl φ a 0 ..^ T b = 1 N L a b Z b
53 simpl a = T b 1 N a = T
54 53 fveq2d a = T b 1 N L a = L T
55 54 fveq1d a = T b 1 N L a b = L T b
56 55 oveq1d a = T b 1 N L a b Z b = L T b Z b
57 56 sumeq2dv a = T b = 1 N L a b Z b = b = 1 N L T b Z b
58 fzfid φ 1 N Fin
59 1 adantr φ b 1 N N 0
60 2 adantr φ b 1 N S 0
61 3 adantr φ b 1 N Z
62 4 adantr φ b 1 N L : 0 ..^ S
63 5 nn0ge0d φ 0 T
64 zltp1le T S T < S T + 1 S
65 25 26 64 syl2anc φ T < S T + 1 S
66 6 65 mpbird φ T < S
67 0zd φ 0
68 elfzo T 0 S T 0 ..^ S 0 T T < S
69 25 67 26 68 syl3anc φ T 0 ..^ S 0 T T < S
70 63 66 69 mpbir2and φ T 0 ..^ S
71 70 adantr φ b 1 N T 0 ..^ S
72 40 a1i φ 1 N
73 72 sselda φ b 1 N b
74 59 60 61 62 71 73 breprexplemb φ b 1 N L T b
75 46 sselda φ b 1 N b 0
76 61 75 expcld φ b 1 N Z b
77 74 76 mulcld φ b 1 N L T b Z b
78 58 77 fsumcl φ b = 1 N L T b Z b
79 13 14 16 5 18 52 57 78 fprodsplitsn φ a 0 ..^ T T b = 1 N L a b Z b = a 0 ..^ T b = 1 N L a b Z b b = 1 N L T b Z b
80 7 oveq1d φ a 0 ..^ T b = 1 N L a b Z b b = 1 N L T b Z b = m = 0 T N d 1 N repr T m a 0 ..^ T L a d a Z m b = 1 N L T b Z b
81 fzfid φ 0 T N Fin
82 40 a1i φ m 0 T N 1 N
83 fz0ssnn0 0 T N 0
84 simpr φ m 0 T N m 0 T N
85 83 84 sseldi φ m 0 T N m 0
86 85 nn0zd φ m 0 T N m
87 5 adantr φ m 0 T N T 0
88 58 adantr φ m 0 T N 1 N Fin
89 82 86 87 88 reprfi φ m 0 T N 1 N repr T m Fin
90 15 a1i φ m 0 T N d 1 N repr T m 0 ..^ T Fin
91 1 adantr φ m 0 T N N 0
92 91 ad2antrr φ m 0 T N d 1 N repr T m a 0 ..^ T N 0
93 2 ad3antrrr φ m 0 T N d 1 N repr T m a 0 ..^ T S 0
94 3 ad3antrrr φ m 0 T N d 1 N repr T m a 0 ..^ T Z
95 4 ad3antrrr φ m 0 T N d 1 N repr T m a 0 ..^ T L : 0 ..^ S
96 37 ad2antrr φ m 0 T N d 1 N repr T m 0 ..^ T 0 ..^ S
97 96 sselda φ m 0 T N d 1 N repr T m a 0 ..^ T a 0 ..^ S
98 40 a1i φ m 0 T N d 1 N repr T m a 0 ..^ T 1 N
99 86 ad2antrr φ m 0 T N d 1 N repr T m a 0 ..^ T m
100 87 ad2antrr φ m 0 T N d 1 N repr T m a 0 ..^ T T 0
101 simplr φ m 0 T N d 1 N repr T m a 0 ..^ T d 1 N repr T m
102 98 99 100 101 reprf φ m 0 T N d 1 N repr T m a 0 ..^ T d : 0 ..^ T 1 N
103 simpr φ m 0 T N d 1 N repr T m a 0 ..^ T a 0 ..^ T
104 102 103 ffvelrnd φ m 0 T N d 1 N repr T m a 0 ..^ T d a 1 N
105 40 104 sseldi φ m 0 T N d 1 N repr T m a 0 ..^ T d a
106 92 93 94 95 97 105 breprexplemb φ m 0 T N d 1 N repr T m a 0 ..^ T L a d a
107 90 106 fprodcl φ m 0 T N d 1 N repr T m a 0 ..^ T L a d a
108 3 ad2antrr φ m 0 T N d 1 N repr T m Z
109 85 adantr φ m 0 T N d 1 N repr T m m 0
110 108 109 expcld φ m 0 T N d 1 N repr T m Z m
111 107 110 mulcld φ m 0 T N d 1 N repr T m a 0 ..^ T L a d a Z m
112 89 111 fsumcl φ m 0 T N d 1 N repr T m a 0 ..^ T L a d a Z m
113 81 58 112 77 fsum2mul φ m = 0 T N b = 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b = m = 0 T N d 1 N repr T m a 0 ..^ T L a d a Z m b = 1 N L T b Z b
114 40 a1i φ m 0 T + 1 N b 1 N 1 N
115 fzssz 0 T + 1 N
116 simpr φ m 0 T + 1 N m 0 T + 1 N
117 115 116 sseldi φ m 0 T + 1 N m
118 117 adantr φ m 0 T + 1 N b 1 N m
119 fzssz 1 N
120 simpr φ m 0 T + 1 N b 1 N b 1 N
121 119 120 sseldi φ m 0 T + 1 N b 1 N b
122 118 121 zsubcld φ m 0 T + 1 N b 1 N m b
123 5 adantr φ m 0 T + 1 N T 0
124 123 adantr φ m 0 T + 1 N b 1 N T 0
125 58 adantr φ m 0 T + 1 N 1 N Fin
126 125 adantr φ m 0 T + 1 N b 1 N 1 N Fin
127 114 122 124 126 reprfi φ m 0 T + 1 N b 1 N 1 N repr T m b Fin
128 74 adantlr φ m 0 T + 1 N b 1 N L T b
129 3 adantr φ m 0 T + 1 N Z
130 fz0ssnn0 0 T + 1 N 0
131 130 116 sseldi φ m 0 T + 1 N m 0
132 129 131 expcld φ m 0 T + 1 N Z m
133 132 adantr φ m 0 T + 1 N b 1 N Z m
134 128 133 mulcld φ m 0 T + 1 N b 1 N L T b Z m
135 15 a1i φ m 0 T + 1 N b 1 N d 1 N repr T m b 0 ..^ T Fin
136 1 adantr φ m 0 T + 1 N N 0
137 136 adantr φ m 0 T + 1 N b 1 N N 0
138 137 ad2antrr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T N 0
139 2 ad4antr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T S 0
140 129 ad3antrrr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T Z
141 4 ad4antr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L : 0 ..^ S
142 38 ad5ant15 φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T a 0 ..^ S
143 40 a1i φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T 1 N
144 122 ad2antrr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T m b
145 124 ad2antrr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T T 0
146 simplr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T d 1 N repr T m b
147 143 144 145 146 reprf φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T d : 0 ..^ T 1 N
148 simpr φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T a 0 ..^ T
149 147 148 ffvelrnd φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T d a 1 N
150 40 149 sseldi φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T d a
151 138 139 140 141 142 150 breprexplemb φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a
152 135 151 fprodcl φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a
153 127 134 152 fsummulc1 φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
154 153 sumeq2dv φ m 0 T + 1 N b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
155 elfzle2 m 0 T + 1 N m T + 1 N
156 155 adantl φ m 0 T + 1 N m T + 1 N
157 136 ad2antrr φ m 0 T + 1 N x 0 ..^ T + 1 y N 0
158 2 ad3antrrr φ m 0 T + 1 N x 0 ..^ T + 1 y S 0
159 129 ad2antrr φ m 0 T + 1 N x 0 ..^ T + 1 y Z
160 4 ad3antrrr φ m 0 T + 1 N x 0 ..^ T + 1 y L : 0 ..^ S
161 25 peano2zd φ T + 1
162 eluz T + 1 S S T + 1 T + 1 S
163 162 biimpar T + 1 S T + 1 S S T + 1
164 161 26 6 163 syl21anc φ S T + 1
165 fzoss2 S T + 1 0 ..^ T + 1 0 ..^ S
166 164 165 syl φ 0 ..^ T + 1 0 ..^ S
167 166 ad3antrrr φ m 0 T + 1 N x 0 ..^ T + 1 y 0 ..^ T + 1 0 ..^ S
168 simplr φ m 0 T + 1 N x 0 ..^ T + 1 y x 0 ..^ T + 1
169 167 168 sseldd φ m 0 T + 1 N x 0 ..^ T + 1 y x 0 ..^ S
170 simpr φ m 0 T + 1 N x 0 ..^ T + 1 y y
171 157 158 159 160 169 170 breprexplemb φ m 0 T + 1 N x 0 ..^ T + 1 y L x y
172 136 123 131 156 171 breprexplema φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b
173 172 oveq1d φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
174 128 adantr φ m 0 T + 1 N b 1 N d 1 N repr T m b L T b
175 152 174 mulcld φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b
176 127 175 fsumcl φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b
177 125 132 176 fsummulc1 φ m 0 T + 1 N b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
178 127 133 175 fsummulc1 φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
179 133 adantr φ m 0 T + 1 N b 1 N d 1 N repr T m b Z m
180 152 174 179 mulassd φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = a 0 ..^ T L a d a L T b Z m
181 180 sumeq2dv φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
182 178 181 eqtrd φ m 0 T + 1 N b 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
183 182 sumeq2dv φ m 0 T + 1 N b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
184 173 177 183 3eqtrd φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
185 40 a1i φ m 0 T + 1 N 1 N
186 1nn0 1 0
187 186 a1i φ m 0 T + 1 N 1 0
188 123 187 nn0addcld φ m 0 T + 1 N T + 1 0
189 185 117 188 125 reprfi φ m 0 T + 1 N 1 N repr T + 1 m Fin
190 fzofi 0 ..^ T + 1 Fin
191 190 a1i φ m 0 T + 1 N d 1 N repr T + 1 m 0 ..^ T + 1 Fin
192 136 ad2antrr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 N 0
193 2 ad3antrrr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 S 0
194 129 ad2antrr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 Z
195 4 ad3antrrr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L : 0 ..^ S
196 166 ad2antrr φ m 0 T + 1 N d 1 N repr T + 1 m 0 ..^ T + 1 0 ..^ S
197 196 sselda φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 a 0 ..^ S
198 40 a1i φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 1 N
199 117 ad2antrr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 m
200 188 ad2antrr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 T + 1 0
201 simplr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 d 1 N repr T + 1 m
202 198 199 200 201 reprf φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 d : 0 ..^ T + 1 1 N
203 simpr φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 a 0 ..^ T + 1
204 202 203 ffvelrnd φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 d a 1 N
205 40 204 sseldi φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 d a
206 192 193 194 195 197 205 breprexplemb φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a
207 191 206 fprodcl φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a
208 189 132 207 fsummulc1 φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m = d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m
209 154 184 208 3eqtr2rd φ m 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
210 209 sumeq2dv φ m = 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m = m = 0 T + 1 N b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
211 oveq1 n = m n b = m b
212 211 oveq2d n = m 1 N repr T n b = 1 N repr T m b
213 212 sumeq1d n = m d 1 N repr T n b a 0 ..^ T L a d a = d 1 N repr T m b a 0 ..^ T L a d a
214 oveq2 n = m Z n = Z m
215 214 oveq2d n = m L T b Z n = L T b Z m
216 213 215 oveq12d n = m d 1 N repr T n b a 0 ..^ T L a d a L T b Z n = d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
217 216 adantr n = m b 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n = d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
218 217 sumeq2dv n = m b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n = b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
219 218 cbvsumv n = 0 T + 1 N b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n = m = 0 T + 1 N b = 1 N d 1 N repr T m b a 0 ..^ T L a d a L T b Z m
220 210 219 syl6eqr φ m = 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m = n = 0 T + 1 N b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n
221 5 1 nn0mulcld φ T N 0
222 oveq2 m = n b 1 N repr T m = 1 N repr T n b
223 222 sumeq1d m = n b d 1 N repr T m a 0 ..^ T L a d a = d 1 N repr T n b a 0 ..^ T L a d a
224 oveq1 m = n b m + b = n - b + b
225 224 oveq2d m = n b Z m + b = Z n - b + b
226 225 oveq2d m = n b L T b Z m + b = L T b Z n - b + b
227 223 226 oveq12d m = n b d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b = d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b
228 40 a1i φ m b b 1 N 1 N
229 uzssz b
230 simp2 φ m b b 1 N m b
231 229 230 sseldi φ m b b 1 N m
232 5 3ad2ant1 φ m b b 1 N T 0
233 58 3ad2ant1 φ m b b 1 N 1 N Fin
234 228 231 232 233 reprfi φ m b b 1 N 1 N repr T m Fin
235 15 a1i φ m b b 1 N d 1 N repr T m 0 ..^ T Fin
236 59 3adant2 φ m b b 1 N N 0
237 236 ad2antrr φ m b b 1 N d 1 N repr T m a 0 ..^ T N 0
238 60 3adant2 φ m b b 1 N S 0
239 238 ad2antrr φ m b b 1 N d 1 N repr T m a 0 ..^ T S 0
240 61 3adant2 φ m b b 1 N Z
241 240 ad2antrr φ m b b 1 N d 1 N repr T m a 0 ..^ T Z
242 62 3adant2 φ m b b 1 N L : 0 ..^ S
243 242 ad2antrr φ m b b 1 N d 1 N repr T m a 0 ..^ T L : 0 ..^ S
244 37 3ad2ant1 φ m b b 1 N 0 ..^ T 0 ..^ S
245 244 adantr φ m b b 1 N d 1 N repr T m 0 ..^ T 0 ..^ S
246 245 sselda φ m b b 1 N d 1 N repr T m a 0 ..^ T a 0 ..^ S
247 40 a1i φ m b b 1 N d 1 N repr T m 1 N
248 231 adantr φ m b b 1 N d 1 N repr T m m
249 232 adantr φ m b b 1 N d 1 N repr T m T 0
250 simpr φ m b b 1 N d 1 N repr T m d 1 N repr T m
251 247 248 249 250 reprf φ m b b 1 N d 1 N repr T m d : 0 ..^ T 1 N
252 251 adantr φ m b b 1 N d 1 N repr T m a 0 ..^ T d : 0 ..^ T 1 N
253 simpr φ m b b 1 N d 1 N repr T m a 0 ..^ T a 0 ..^ T
254 252 253 ffvelrnd φ m b b 1 N d 1 N repr T m a 0 ..^ T d a 1 N
255 40 254 sseldi φ m b b 1 N d 1 N repr T m a 0 ..^ T d a
256 237 239 241 243 246 255 breprexplemb φ m b b 1 N d 1 N repr T m a 0 ..^ T L a d a
257 235 256 fprodcl φ m b b 1 N d 1 N repr T m a 0 ..^ T L a d a
258 234 257 fsumcl φ m b b 1 N d 1 N repr T m a 0 ..^ T L a d a
259 71 3adant2 φ m b b 1 N T 0 ..^ S
260 73 3adant2 φ m b b 1 N b
261 236 238 240 242 259 260 breprexplemb φ m b b 1 N L T b
262 231 zcnd φ m b b 1 N m
263 simp3 φ m b b 1 N b 1 N
264 119 263 sseldi φ m b b 1 N b
265 264 zcnd φ m b b 1 N b
266 262 265 subnegd φ m b b 1 N m b = m + b
267 264 znegcld φ m b b 1 N b
268 eluzle m b b m
269 230 268 syl φ m b b 1 N b m
270 znn0sub b m b m m b 0
271 270 biimpa b m b m m b 0
272 267 231 269 271 syl21anc φ m b b 1 N m b 0
273 266 272 eqeltrrd φ m b b 1 N m + b 0
274 240 273 expcld φ m b b 1 N Z m + b
275 261 274 mulcld φ m b b 1 N L T b Z m + b
276 258 275 mulcld φ m b b 1 N d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b
277 59 adantr φ b 1 N n T N + b + 1 T N + N N 0
278 ssidd φ b 1 N n T N + b + 1 T N + N 1 N 1 N
279 fzssz T N + b + 1 T N + N
280 simpr φ b 1 N n T N + b + 1 T N + N n T N + b + 1 T N + N
281 279 280 sseldi φ b 1 N n T N + b + 1 T N + N n
282 simplr φ b 1 N n T N + b + 1 T N + N b 1 N
283 119 282 sseldi φ b 1 N n T N + b + 1 T N + N b
284 281 283 zsubcld φ b 1 N n T N + b + 1 T N + N n b
285 5 ad2antrr φ b 1 N n T N + b + 1 T N + N T 0
286 27 ad2antrr φ b 1 N n T N + b + 1 T N + N T
287 277 nn0red φ b 1 N n T N + b + 1 T N + N N
288 286 287 remulcld φ b 1 N n T N + b + 1 T N + N T N
289 283 zred φ b 1 N n T N + b + 1 T N + N b
290 221 adantr φ b 1 N T N 0
291 290 75 nn0addcld φ b 1 N T N + b 0
292 186 a1i φ b 1 N 1 0
293 291 292 nn0addcld φ b 1 N T N + b + 1 0
294 fz2ssnn0 T N + b + 1 0 T N + b + 1 T N + N 0
295 293 294 syl φ b 1 N T N + b + 1 T N + N 0
296 295 sselda φ b 1 N n T N + b + 1 T N + N n 0
297 296 nn0red φ b 1 N n T N + b + 1 T N + N n
298 25 ad2antrr φ b 1 N n T N + b + 1 T N + N T
299 277 nn0zd φ b 1 N n T N + b + 1 T N + N N
300 298 299 zmulcld φ b 1 N n T N + b + 1 T N + N T N
301 300 283 zaddcld φ b 1 N n T N + b + 1 T N + N T N + b
302 elfzle1 n T N + b + 1 T N + N T N + b + 1 n
303 280 302 syl φ b 1 N n T N + b + 1 T N + N T N + b + 1 n
304 zltp1le T N + b n T N + b < n T N + b + 1 n
305 304 biimpar T N + b n T N + b + 1 n T N + b < n
306 301 281 303 305 syl21anc φ b 1 N n T N + b + 1 T N + N T N + b < n
307 ltaddsub T N b n T N + b < n T N < n b
308 307 biimpa T N b n T N + b < n T N < n b
309 288 289 297 306 308 syl31anc φ b 1 N n T N + b + 1 T N + N T N < n b
310 277 278 284 285 309 reprgt φ b 1 N n T N + b + 1 T N + N 1 N repr T n b =
311 310 sumeq1d φ b 1 N n T N + b + 1 T N + N d 1 N repr T n b a 0 ..^ T L a d a = d a 0 ..^ T L a d a
312 sum0 d a 0 ..^ T L a d a = 0
313 311 312 syl6eq φ b 1 N n T N + b + 1 T N + N d 1 N repr T n b a 0 ..^ T L a d a = 0
314 313 oveq1d φ b 1 N n T N + b + 1 T N + N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b = 0 L T b Z n - b + b
315 74 adantr φ b 1 N n T N + b + 1 T N + N L T b
316 61 adantr φ b 1 N n T N + b + 1 T N + N Z
317 281 zcnd φ b 1 N n T N + b + 1 T N + N n
318 283 zcnd φ b 1 N n T N + b + 1 T N + N b
319 317 318 npcand φ b 1 N n T N + b + 1 T N + N n - b + b = n
320 319 296 eqeltrd φ b 1 N n T N + b + 1 T N + N n - b + b 0
321 316 320 expcld φ b 1 N n T N + b + 1 T N + N Z n - b + b
322 315 321 mulcld φ b 1 N n T N + b + 1 T N + N L T b Z n - b + b
323 322 mul02d φ b 1 N n T N + b + 1 T N + N 0 L T b Z n - b + b = 0
324 314 323 eqtrd φ b 1 N n T N + b + 1 T N + N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b = 0
325 40 a1i φ b 1 N n 0 ..^ b 1 N
326 fzossfz 0 ..^ b 0 b
327 fzssz 0 b
328 326 327 sstri 0 ..^ b
329 simpr φ b 1 N n 0 ..^ b n 0 ..^ b
330 328 329 sseldi φ b 1 N n 0 ..^ b n
331 simplr φ b 1 N n 0 ..^ b b 1 N
332 119 331 sseldi φ b 1 N n 0 ..^ b b
333 330 332 zsubcld φ b 1 N n 0 ..^ b n b
334 5 ad2antrr φ b 1 N n 0 ..^ b T 0
335 333 zred φ b 1 N n 0 ..^ b n b
336 0red φ b 1 N n 0 ..^ b 0
337 27 ad2antrr φ b 1 N n 0 ..^ b T
338 elfzolt2 n 0 ..^ b n < b
339 338 adantl φ b 1 N n 0 ..^ b n < b
340 330 zred φ b 1 N n 0 ..^ b n
341 332 zred φ b 1 N n 0 ..^ b b
342 340 341 sublt0d φ b 1 N n 0 ..^ b n b < 0 n < b
343 339 342 mpbird φ b 1 N n 0 ..^ b n b < 0
344 63 ad2antrr φ b 1 N n 0 ..^ b 0 T
345 335 336 337 343 344 ltletrd φ b 1 N n 0 ..^ b n b < T
346 325 333 334 345 reprlt φ b 1 N n 0 ..^ b 1 N repr T n b =
347 346 sumeq1d φ b 1 N n 0 ..^ b d 1 N repr T n b a 0 ..^ T L a d a = d a 0 ..^ T L a d a
348 347 312 syl6eq φ b 1 N n 0 ..^ b d 1 N repr T n b a 0 ..^ T L a d a = 0
349 348 oveq1d φ b 1 N n 0 ..^ b d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b = 0 L T b Z n - b + b
350 74 adantr φ b 1 N n 0 ..^ b L T b
351 61 adantr φ b 1 N n 0 ..^ b Z
352 340 recnd φ b 1 N n 0 ..^ b n
353 341 recnd φ b 1 N n 0 ..^ b b
354 352 353 npcand φ b 1 N n 0 ..^ b n - b + b = n
355 fzo0ssnn0 0 ..^ b 0
356 355 329 sseldi φ b 1 N n 0 ..^ b n 0
357 354 356 eqeltrd φ b 1 N n 0 ..^ b n - b + b 0
358 351 357 expcld φ b 1 N n 0 ..^ b Z n - b + b
359 350 358 mulcld φ b 1 N n 0 ..^ b L T b Z n - b + b
360 359 mul02d φ b 1 N n 0 ..^ b 0 L T b Z n - b + b = 0
361 349 360 eqtrd φ b 1 N n 0 ..^ b d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b = 0
362 221 1 227 276 324 361 fsum2dsub φ m = 0 T N b = 1 N d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b = n = 0 T N + N b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b
363 nn0sscn 0
364 363 5 sseldi φ T
365 363 1 sseldi φ N
366 364 365 adddirp1d φ T + 1 N = T N + N
367 366 oveq2d φ 0 T + 1 N = 0 T N + N
368 130 363 sstri 0 T + 1 N
369 simplr φ n 0 T + 1 N b 1 N n 0 T + 1 N
370 368 369 sseldi φ n 0 T + 1 N b 1 N n
371 45 363 sstri 1 N
372 simpr φ n 0 T + 1 N b 1 N b 1 N
373 371 372 sseldi φ n 0 T + 1 N b 1 N b
374 370 373 npcand φ n 0 T + 1 N b 1 N n - b + b = n
375 374 eqcomd φ n 0 T + 1 N b 1 N n = n - b + b
376 375 oveq2d φ n 0 T + 1 N b 1 N Z n = Z n - b + b
377 376 oveq2d φ n 0 T + 1 N b 1 N L T b Z n = L T b Z n - b + b
378 377 oveq2d φ n 0 T + 1 N b 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n = d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b
379 378 sumeq2dv φ n 0 T + 1 N b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n = b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b
380 367 379 sumeq12dv φ n = 0 T + 1 N b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n = n = 0 T N + N b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n - b + b
381 362 380 eqtr4d φ m = 0 T N b = 1 N d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b = n = 0 T + 1 N b = 1 N d 1 N repr T n b a 0 ..^ T L a d a L T b Z n
382 107 adantlr φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a
383 110 adantlr φ m 0 T N b 1 N d 1 N repr T m Z m
384 77 adantlr φ m 0 T N b 1 N L T b Z b
385 384 adantr φ m 0 T N b 1 N d 1 N repr T m L T b Z b
386 382 383 385 mulassd φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b = a 0 ..^ T L a d a Z m L T b Z b
387 74 ad4ant13 φ m 0 T N b 1 N d 1 N repr T m L T b
388 76 ad4ant13 φ m 0 T N b 1 N d 1 N repr T m Z b
389 383 387 388 mulassd φ m 0 T N b 1 N d 1 N repr T m Z m L T b Z b = Z m L T b Z b
390 387 383 388 mulassd φ m 0 T N b 1 N d 1 N repr T m L T b Z m Z b = L T b Z m Z b
391 383 387 mulcomd φ m 0 T N b 1 N d 1 N repr T m Z m L T b = L T b Z m
392 391 oveq1d φ m 0 T N b 1 N d 1 N repr T m Z m L T b Z b = L T b Z m Z b
393 108 adantlr φ m 0 T N b 1 N d 1 N repr T m Z
394 75 ad4ant13 φ m 0 T N b 1 N d 1 N repr T m b 0
395 109 adantlr φ m 0 T N b 1 N d 1 N repr T m m 0
396 393 394 395 expaddd φ m 0 T N b 1 N d 1 N repr T m Z m + b = Z m Z b
397 396 oveq2d φ m 0 T N b 1 N d 1 N repr T m L T b Z m + b = L T b Z m Z b
398 390 392 397 3eqtr4d φ m 0 T N b 1 N d 1 N repr T m Z m L T b Z b = L T b Z m + b
399 389 398 eqtr3d φ m 0 T N b 1 N d 1 N repr T m Z m L T b Z b = L T b Z m + b
400 399 oveq2d φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b = a 0 ..^ T L a d a L T b Z m + b
401 386 400 eqtrd φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b = a 0 ..^ T L a d a L T b Z m + b
402 401 sumeq2dv φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b = d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b
403 89 adantr φ m 0 T N b 1 N 1 N repr T m Fin
404 111 adantlr φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a Z m
405 403 384 404 fsummulc1 φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b = d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b
406 74 adantlr φ m 0 T N b 1 N L T b
407 61 adantlr φ m 0 T N b 1 N Z
408 85 adantr φ m 0 T N b 1 N m 0
409 75 adantlr φ m 0 T N b 1 N b 0
410 408 409 nn0addcld φ m 0 T N b 1 N m + b 0
411 407 410 expcld φ m 0 T N b 1 N Z m + b
412 406 411 mulcld φ m 0 T N b 1 N L T b Z m + b
413 403 412 382 fsummulc1 φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b = d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b
414 402 405 413 3eqtr4rd φ m 0 T N b 1 N d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b = d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b
415 414 sumeq2dv φ m 0 T N b = 1 N d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b = b = 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b
416 415 sumeq2dv φ m = 0 T N b = 1 N d 1 N repr T m a 0 ..^ T L a d a L T b Z m + b = m = 0 T N b = 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b
417 220 381 416 3eqtr2rd φ m = 0 T N b = 1 N d 1 N repr T m a 0 ..^ T L a d a Z m L T b Z b = m = 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m
418 80 113 417 3eqtr2d φ a 0 ..^ T b = 1 N L a b Z b b = 1 N L T b Z b = m = 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m
419 12 79 418 3eqtrd φ a 0 ..^ T + 1 b = 1 N L a b Z b = m = 0 T + 1 N d 1 N repr T + 1 m a 0 ..^ T + 1 L a d a Z m