Step Hyp Ref
Expression 1 seqcoll.3 . 2
2 elfznn 11743 . . . 4
3 1 , 2 syl 16 . . 3
4 eleq1 2529 . . . . . 6
5 fveq2 5871 . . . . . . . 8
6 5 fveq2d 5875 . . . . . . 7
7 fveq2 5871 . . . . . . 7
8 6 , 7 eqeq12d 2479 . . . . . 6
9 4 , 8 imbi12d 320 . . . . 5
10 9 imbi2d 316 . . . 4
11 eleq1 2529 . . . . . 6
12 fveq2 5871 . . . . . . . 8
13 12 fveq2d 5875 . . . . . . 7
14 fveq2 5871 . . . . . . 7
15 13 , 14 eqeq12d 2479 . . . . . 6
16 11 , 15 imbi12d 320 . . . . 5
17 16 imbi2d 316 . . . 4
18 eleq1 2529 . . . . . 6
19 fveq2 5871 . . . . . . . 8
20 19 fveq2d 5875 . . . . . . 7
21 fveq2 5871 . . . . . . 7
22 20 , 21 eqeq12d 2479 . . . . . 6
23 18 , 22 imbi12d 320 . . . . 5
24 23 imbi2d 316 . . . 4
25 eleq1 2529 . . . . . 6
26 fveq2 5871 . . . . . . . 8
27 26 fveq2d 5875 . . . . . . 7
28 fveq2 5871 . . . . . . 7
29 27 , 28 eqeq12d 2479 . . . . . 6
30 25 , 29 imbi12d 320 . . . . 5
31 30 imbi2d 316 . . . 4
32 seqcoll.1 . . . . . . . . 9
33 seqcoll.a . . . . . . . . 9
34 seqcoll.4 . . . . . . . . . 10
35 seqcoll.2 . . . . . . . . . . . . 13
36 isof1o 6221 . . . . . . . . . . . . 13
37 35 , 36 syl 16 . . . . . . . . . . . 12
38 f1of 5821 . . . . . . . . . . . 12
39 37 , 38 syl 16 . . . . . . . . . . 11
40 elfzuz2 11720 . . . . . . . . . . . . 13
41 1 , 40 syl 16 . . . . . . . . . . . 12
42 eluzfz1 11722 . . . . . . . . . . . 12
43 41 , 42 syl 16 . . . . . . . . . . 11
44 39 , 43 ffvelrnd 6032 . . . . . . . . . 10
45 34 , 44 sseldd 3504 . . . . . . . . 9
46 eluzle 11122 . . . . . . . . . . . . 13
47 41 , 46 syl 16 . . . . . . . . . . . 12
48 elfzelz 11717 . . . . . . . . . . . . . . . . 17
49 48 ssriv 3507 . . . . . . . . . . . . . . . 16
50 zssre 10896 . . . . . . . . . . . . . . . 16
51 49 , 50 sstri 3512 . . . . . . . . . . . . . . 15
52 51 a1i 11 . . . . . . . . . . . . . 14
53 ressxr 9658 . . . . . . . . . . . . . 14
54 52 , 53 syl6ss 3515 . . . . . . . . . . . . 13
55 eluzelre 11120 . . . . . . . . . . . . . . . 16
56 55 ssriv 3507 . . . . . . . . . . . . . . 15
57 34 , 56 syl6ss 3515 . . . . . . . . . . . . . 14
58 57 , 53 syl6ss 3515 . . . . . . . . . . . . 13
59 eluzfz2 11723 . . . . . . . . . . . . . 14
60 41 , 59 syl 16 . . . . . . . . . . . . 13
61 leisorel 12509 . . . . . . . . . . . . 13
62 35 , 54 , 58 , 43 , 60 , 61 syl122anc 1237 . . . . . . . . . . . 12
63 47 , 62 mpbid 210 . . . . . . . . . . 11
64 39 , 60 ffvelrnd 6032 . . . . . . . . . . . . . 14
65 34 , 64 sseldd 3504 . . . . . . . . . . . . 13
66 eluzelz 11119 . . . . . . . . . . . . 13
67 65 , 66 syl 16 . . . . . . . . . . . 12
68 elfz5 11709 . . . . . . . . . . . 12
69 45 , 67 , 68 syl2anc 661 . . . . . . . . . . 11
70 63 , 69 mpbird 232 . . . . . . . . . 10
71 fveq2 5871 . . . . . . . . . . . . 13
72 71 eleq1d 2526 . . . . . . . . . . . 12
73 72 imbi2d 316 . . . . . . . . . . 11
74 seqcoll.5 . . . . . . . . . . . 12
75 74 expcom 435 . . . . . . . . . . 11
76 73 , 75 vtoclga 3173 . . . . . . . . . 10
77 70 , 76 mpcom 36 . . . . . . . . 9
78 eluzelz 11119 . . . . . . . . . . . . . . . . . 18
79 45 , 78 syl 16 . . . . . . . . . . . . . . . . 17
80 peano2zm 10932 . . . . . . . . . . . . . . . . 17
81 79 , 80 syl 16 . . . . . . . . . . . . . . . 16
82 81 zred 10994 . . . . . . . . . . . . . . 15
83 79 zred 10994 . . . . . . . . . . . . . . 15
84 67 zred 10994 . . . . . . . . . . . . . . 15
85 83 lem1d 10504 . . . . . . . . . . . . . . 15
86 82 , 83 , 84 , 85 , 63 letrd 9760 . . . . . . . . . . . . . 14
87 eluz 11123 . . . . . . . . . . . . . . 15
88 81 , 67 , 87 syl2anc 661 . . . . . . . . . . . . . 14
89 86 , 88 mpbird 232 . . . . . . . . . . . . 13
90 fzss2 11752 . . . . . . . . . . . . 13
91 89 , 90 syl 16 . . . . . . . . . . . 12
92 91 sselda 3503 . . . . . . . . . . 11
93 eluzel2 11115 . . . . . . . . . . . . . . 15
94 45 , 93 syl 16 . . . . . . . . . . . . . 14
95 elfzm11 11778 . . . . . . . . . . . . . 14
96 94 , 79 , 95 syl2anc 661 . . . . . . . . . . . . 13
97 simp3 998 . . . . . . . . . . . . . 14
98 f1ocnv 5833 . . . . . . . . . . . . . . . . . . . . . . . 24
99 37 , 98 syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
100 f1of 5821 . . . . . . . . . . . . . . . . . . . . . . 23
101 99 , 100 syl 16 . . . . . . . . . . . . . . . . . . . . . 22
102 101 ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . . 21
103 elfznn 11743 . . . . . . . . . . . . . . . . . . . . 21
104 102 , 103 syl 16 . . . . . . . . . . . . . . . . . . . 20
105 104 nnge1d 10603 . . . . . . . . . . . . . . . . . . 19
106 35 adantr 465 . . . . . . . . . . . . . . . . . . . 20
107 54 adantr 465 . . . . . . . . . . . . . . . . . . . 20
108 58 adantr 465 . . . . . . . . . . . . . . . . . . . 20
109 43 adantr 465 . . . . . . . . . . . . . . . . . . . 20
110 leisorel 12509 . . . . . . . . . . . . . . . . . . . 20
111 106 , 107 ,
108 , 109 , 102 , 110 syl122anc 1237 . . . . . . . . . . . . . . . . . . 19
112 105 , 111 mpbid 210 . . . . . . . . . . . . . . . . . 18
113 f1ocnvfv2 6183 . . . . . . . . . . . . . . . . . . 19
114 37 , 113 sylan 471 . . . . . . . . . . . . . . . . . 18
115 112 , 114 breqtrd 4476 . . . . . . . . . . . . . . . . 17
116 83 adantr 465 . . . . . . . . . . . . . . . . . 18
117 57 sselda 3503 . . . . . . . . . . . . . . . . . 18
118 116 , 117 lenltd 9752 . . . . . . . . . . . . . . . . 17
119 115 , 118 mpbid 210 . . . . . . . . . . . . . . . 16
120 119 ex 434 . . . . . . . . . . . . . . 15
121 120 con2d 115 . . . . . . . . . . . . . 14
122 97 , 121 syl5 32 . . . . . . . . . . . . 13
123 96 , 122 sylbid 215 . . . . . . . . . . . 12
124 123 imp 429 . . . . . . . . . . 11
125 92 , 124 eldifd 3486 . . . . . . . . . 10
126 seqcoll.6 . . . . . . . . . 10
127 125 , 126 syldan 470 . . . . . . . . 9
128 32 , 33 , 45 , 77 , 127 seqid 12152 . . . . . . . 8
129 128 fveq1d 5873 . . . . . . 7
130 uzid 11124 . . . . . . . . 9
131 79 , 130 syl 16 . . . . . . . 8
132 fvres 5885 . . . . . . . 8
133 131 , 132 syl 16 . . . . . . 7
134 seq1 12120 . . . . . . . . 9
135 79 , 134 syl 16 . . . . . . . 8
136 fveq2 5871 . . . . . . . . . . . 12
137 fveq2 5871 . . . . . . . . . . . . 13
138 137 fveq2d 5875 . . . . . . . . . . . 12
139 136 , 138 eqeq12d 2479 . . . . . . . . . . 11
140 139 imbi2d 316 . . . . . . . . . 10
141 seqcoll.7 . . . . . . . . . . 11
142 141 expcom 435 . . . . . . . . . 10
143 140 , 142 vtoclga 3173 . . . . . . . . 9
144 43 , 143 mpcom 36 . . . . . . . 8
145 135 , 144 eqtr4d 2501 . . . . . . 7
146 129 , 133 ,
145 3eqtr3d 2506 . . . . . 6
147 1z 10919 . . . . . . 7
148 seq1 12120 . . . . . . 7
149 147 , 148 ax-mp 5 . . . . . 6
150 146 , 149 syl6eqr 2516 . . . . 5
151 150 a1d 25 . . . 4
152 simplr 755 . . . . . . . . . . 11
153 nnuz 11145 . . . . . . . . . . 11
154 152 , 153 syl6eleq 2555 . . . . . . . . . 10
155 nnz 10911 . . . . . . . . . . . 12
156 155 ad2antlr 726 . . . . . . . . . . 11
157 elfzuz3 11714 . . . . . . . . . . . 12
158 157 adantl 466 . . . . . . . . . . 11
159 peano2uzr 11165 . . . . . . . . . . 11
160 156 , 158 ,
159 syl2anc 661 . . . . . . . . . 10
161 elfzuzb 11711 . . . . . . . . . 10
162 154 , 160 ,
161 sylanbrc 664 . . . . . . . . 9
163 162 ex 434 . . . . . . . 8
164 163 imim1d 75 . . . . . . 7
165 oveq1 6303 . . . . . . . . . 10
166 simpll 753 . . . . . . . . . . . . . . 15
167 seqcoll.1b . . . . . . . . . . . . . . 15
168 166 , 167 sylan 471 . . . . . . . . . . . . . 14
169 34 ad2antrr 725 . . . . . . . . . . . . . . 15
170 39 ad2antrr 725 . . . . . . . . . . . . . . . 16
171 170 , 162 ffvelrnd 6032 . . . . . . . . . . . . . . 15
172 169 , 171 sseldd 3504 . . . . . . . . . . . . . 14
173 nnre 10568 . . . . . . . . . . . . . . . . . . 19
174 173 ad2antlr 726 . . . . . . . . . . . . . . . . . 18
175 174 ltp1d 10501 . . . . . . . . . . . . . . . . 17
176 35 ad2antrr 725 . . . . . . . . . . . . . . . . . 18
177 simpr 461 . . . . . . . . . . . . . . . . . 18
178 isorel 6222 . . . . . . . . . . . . . . . . . 18
179 176 , 162 ,
177 , 178 syl12anc 1226 . . . . . . . . . . . . . . . . 17
180 175 , 179 mpbid 210 . . . . . . . . . . . . . . . 16
181 eluzelz 11119 . . . . . . . . . . . . . . . . . 18
182 172 , 181 syl 16 . . . . . . . . . . . . . . . . 17
183 170 , 177 ffvelrnd 6032 . . . . . . . . . . . . . . . . . . 19
184 169 , 183 sseldd 3504 . . . . . . . . . . . . . . . . . 18
185 eluzelz 11119 . . . . . . . . . . . . . . . . . 18
186 184 , 185 syl 16 . . . . . . . . . . . . . . . . 17
187 zltlem1 10941 . . . . . . . . . . . . . . . . 17
188 182 , 186 ,
187 syl2anc 661 . . . . . . . . . . . . . . . 16
189 180 , 188 mpbid 210 . . . . . . . . . . . . . . 15
190 peano2zm 10932 . . . . . . . . . . . . . . . . 17
191 186 , 190 syl 16 . . . . . . . . . . . . . . . 16
192 eluz 11123 . . . . . . . . . . . . . . . 16
193 182 , 191 ,
192 syl2anc 661 . . . . . . . . . . . . . . 15
194 189 , 193 mpbird 232 . . . . . . . . . . . . . 14
195 191 zred 10994 . . . . . . . . . . . . . . . . . . . . 21
196 186 zred 10994 . . . . . . . . . . . . . . . . . . . . 21
197 84 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
198 196 lem1d 10504 . . . . . . . . . . . . . . . . . . . . 21
199 elfzle2 11719 . . . . . . . . . . . . . . . . . . . . . . 23
200 199 adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
201 54 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
202 58 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
203 60 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
204 leisorel 12509 . . . . . . . . . . . . . . . . . . . . . . 23
205 176 , 201 ,
202 , 177 , 203 , 204 syl122anc 1237 . . . . . . . . . . . . . . . . . . . . . 22
206 200 , 205 mpbid 210 . . . . . . . . . . . . . . . . . . . . 21
207 195 , 196 ,
197 , 198 , 206 letrd 9760 . . . . . . . . . . . . . . . . . . . 20
208 67 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
209 eluz 11123 . . . . . . . . . . . . . . . . . . . . 21
210 191 , 208 ,
209 syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
211 207 , 210 mpbird 232 . . . . . . . . . . . . . . . . . . 19
212 uztrn 11126 . . . . . . . . . . . . . . . . . . 19
213 211 , 194 ,
212 syl2anc 661 . . . . . . . . . . . . . . . . . 18
214 fzss2 11752 . . . . . . . . . . . . . . . . . 18
215 213 , 214 syl 16 . . . . . . . . . . . . . . . . 17
216 215 sselda 3503 . . . . . . . . . . . . . . . 16
217 166 , 74 sylan 471 . . . . . . . . . . . . . . . 16
218 216 , 217 syldan 470 . . . . . . . . . . . . . . 15
219 seqcoll.c . . . . . . . . . . . . . . . 16
220 166 , 219 sylan 471 . . . . . . . . . . . . . . 15
221 172 , 218 ,
220 seqcl 12127 . . . . . . . . . . . . . 14
222 simplll 759 . . . . . . . . . . . . . . 15
223 elfzuz 11713 . . . . . . . . . . . . . . . . . 18
224 peano2uz 11163 . . . . . . . . . . . . . . . . . . 19
225 172 , 224 syl 16 . . . . . . . . . . . . . . . . . 18
226 uztrn 11126 . . . . . . . . . . . . . . . . . 18
