MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqf1olem2 Unicode version

Theorem seqf1olem2 12147
Description: Lemma for seqf1o 12148. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
Hypotheses
Ref Expression
seqf1o.1
seqf1o.2
seqf1o.3
seqf1o.4
seqf1o.5
seqf1olem.5
seqf1olem.6
seqf1olem.7
seqf1olem.8
seqf1olem.9
Assertion
Ref Expression
seqf1olem2
Distinct variable groups:   , , , , , ,   , , , , , ,   ,M, , , , ,   , , , , , ,   ,J, , , ,   ,N, , , , ,   , , , ,   , , , , , ,   S, , , ,   , , , , , ,

Proof of Theorem seqf1olem2
StepHypRef Expression
1 seqf1olem.6 . . . . . . . . . 10
2 ffn 5736 . . . . . . . . . 10
31, 2syl 16 . . . . . . . . 9
4 fzssp1 11755 . . . . . . . . 9
5 fnssres 5699 . . . . . . . . 9
63, 4, 5sylancl 662 . . . . . . . 8
7 fzfid 12083 . . . . . . . 8
8 fnfi 7818 . . . . . . . 8
96, 7, 8syl2anc 661 . . . . . . 7
10 elex 3118 . . . . . . 7
119, 10syl 16 . . . . . 6
12 seqf1o.1 . . . . . . . . 9
13 seqf1o.2 . . . . . . . . 9
14 seqf1o.3 . . . . . . . . 9
15 seqf1o.4 . . . . . . . . 9
16 seqf1o.5 . . . . . . . . 9
17 seqf1olem.5 . . . . . . . . 9
18 seqf1olem.7 . . . . . . . . 9
19 seqf1olem.8 . . . . . . . . 9
2012, 13, 14, 15, 16, 17, 1, 18, 19seqf1olem1 12146 . . . . . . . 8
21 f1of 5821 . . . . . . . 8
2220, 21syl 16 . . . . . . 7
23 fex2 6755 . . . . . . 7
2422, 7, 7, 23syl3anc 1228 . . . . . 6
2511, 24jca 532 . . . . 5
26 seqf1olem.9 . . . . 5
27 fssres 5756 . . . . . . 7
281, 4, 27sylancl 662 . . . . . 6
2920, 28jca 532 . . . . 5
30 f1oeq1 5812 . . . . . . . 8
31 feq1 5718 . . . . . . . 8
3230, 31bi2anan9r 874 . . . . . . 7
33 coeq1 5165 . . . . . . . . . . 11
34 coeq2 5166 . . . . . . . . . . 11
3533, 34sylan9eq 2518 . . . . . . . . . 10
3635seqeq3d 12115 . . . . . . . . 9
3736fveq1d 5873 . . . . . . . 8
38 simpl 457 . . . . . . . . . 10
3938seqeq3d 12115 . . . . . . . . 9
4039fveq1d 5873 . . . . . . . 8
4137, 40eqeq12d 2479 . . . . . . 7
4232, 41imbi12d 320 . . . . . 6
4342spc2gv 3197 . . . . 5
4425, 26, 29, 43syl3c 61 . . . 4
45 fvres 5885 . . . . . 6
4645adantl 466 . . . . 5
4715, 46seqfveq 12131 . . . 4
4844, 47eqtrd 2498 . . 3
4948oveq1d 6311 . 2
5012adantlr 714 . . . . 5
5114adantlr 714 . . . . 5
52 elfzuz3 11714 . . . . . . 7
5352adantl 466 . . . . . 6
54 eluzp1p1 11135 . . . . . 6
5553, 54syl 16 . . . . 5
56 elfzuz 11713 . . . . . 6
5756adantl 466 . . . . 5
58 f1of 5821 . . . . . . . . . 10
5917, 58syl 16 . . . . . . . . 9
60 fco 5746 . . . . . . . . 9
611, 59, 60syl2anc 661 . . . . . . . 8
6261, 16fssd 5745 . . . . . . 7
6362ffvelrnda 6031 . . . . . 6
6463adantlr 714 . . . . 5
6550, 51, 55, 57, 64seqsplit 12140 . . . 4
66 elfzp12 11786 . . . . . . 7
6766biimpa 484 . . . . . 6
6815, 67sylan 471 . . . . 5
69 seqeq1 12110 . . . . . . . . . . 11
7069eqcomd 2465 . . . . . . . . . 10
7170fveq1d 5873 . . . . . . . . 9
72 f1ocnv 5833 . . . . . . . . . . . . 13
73 f1of 5821 . . . . . . . . . . . . 13
7417, 72, 733syl 20 . . . . . . . . . . . 12
75 peano2uz 11163 . . . . . . . . . . . . 13
76 eluzfz2 11723 . . . . . . . . . . . . 13
7715, 75, 763syl 20 . . . . . . . . . . . 12
7874, 77ffvelrnd 6032 . . . . . . . . . . 11
7919, 78syl5eqel 2549 . . . . . . . . . 10
80 elfzelz 11717 . . . . . . . . . 10
81 seq1 12120 . . . . . . . . . 10
8279, 80, 813syl 20 . . . . . . . . 9
8371, 82sylan9eqr 2520 . . . . . . . 8
8483oveq1d 6311 . . . . . . 7
85 simpr 461 . . . . . . . . 9
86 eluzfz1 11722 . . . . . . . . . . 11
8715, 86syl 16 . . . . . . . . . 10
8887adantr 465 . . . . . . . . 9
8985, 88eqeltrd 2545 . . . . . . . 8
9013adantlr 714 . . . . . . . . . 10
9116adantr 465 . . . . . . . . . 10
9261adantr 465 . . . . . . . . . 10
9379adantr 465 . . . . . . . . . 10
94 peano2uz 11163 . . . . . . . . . . 11
95 fzss1 11751 . . . . . . . . . . 11
9657, 94, 953syl 20 . . . . . . . . . 10
9750, 90, 51, 55, 91, 92, 93, 96seqf1olem2a 12145 . . . . . . . . 9
98 1zzd 10920 . . . . . . . . . . 11
99 elfzuz 11713 . . . . . . . . . . . . . . . . . 18
100 fzss1 11751 . . . . . . . . . . . . . . . . . 18
10179, 99, 1003syl 20 . . . . . . . . . . . . . . . . 17
102101sselda 3503 . . . . . . . . . . . . . . . 16
10322ffvelrnda 6031 . . . . . . . . . . . . . . . 16
104102, 103syldan 470 . . . . . . . . . . . . . . 15
105 fvres 5885 . . . . . . . . . . . . . . 15
106104, 105syl 16 . . . . . . . . . . . . . 14
107 breq1 4455 . . . . . . . . . . . . . . . . . . . 20
108 id 22 . . . . . . . . . . . . . . . . . . . 20
109 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20
110107, 108, 109ifbieq12d 3968 . . . . . . . . . . . . . . . . . . 19
111110fveq2d 5875 . . . . . . . . . . . . . . . . . 18
112 fvex 5881 . . . . . . . . . . . . . . . . . 18
113111, 18, 112fvmpt 5956 . . . . . . . . . . . . . . . . 17
114102, 113syl 16 . . . . . . . . . . . . . . . 16
115 elfzle1 11718 . . . . . . . . . . . . . . . . . . 19
116115adantl 466 . . . . . . . . . . . . . . . . . 18
11779, 80syl 16 . . . . . . . . . . . . . . . . . . . . 21
118117zred 10994 . . . . . . . . . . . . . . . . . . . 20
119118adantr 465 . . . . . . . . . . . . . . . . . . 19
120 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . 21
121120adantl 466 . . . . . . . . . . . . . . . . . . . 20
122121zred 10994 . . . . . . . . . . . . . . . . . . 19
123119, 122lenltd 9752 . . . . . . . . . . . . . . . . . 18
124116, 123mpbid 210 . . . . . . . . . . . . . . . . 17
125 iffalse 3950 . . . . . . . . . . . . . . . . . 18
126125fveq2d 5875 . . . . . . . . . . . . . . . . 17
127124, 126syl 16 . . . . . . . . . . . . . . . 16
128114, 127eqtrd 2498 . . . . . . . . . . . . . . 15
129128fveq2d 5875 . . . . . . . . . . . . . 14
130106, 129eqtrd 2498 . . . . . . . . . . . . 13
131 fvco3 5950 . . . . . . . . . . . . . . 15
13222, 131sylan 471 . . . . . . . . . . . . . 14
133102, 132syldan 470 . . . . . . . . . . . . 13
134 fzp1elp1 11762 . . . . . . . . . . . . . . 15
135102, 134syl 16 . . . . . . . . . . . . . 14
136 fvco3 5950 . . . . . . . . . . . . . . 15
13759, 136sylan 471 . . . . . . . . . . . . . 14
138135, 137syldan 470 . . . . . . . . . . . . 13
139130, 133, 1383eqtr4d 2508 . . . . . . . . . . . 12
140139adantlr 714 . . . . . . . . . . 11
14153, 98, 140seqshft2 12133 . . . . . . . . . 10
142 fvco3 5950 . . . . . . . . . . . . 13
14359, 79, 142syl2anc 661 . . . . . . . . . . . 12
14419fveq2i 5874 . . . . . . . . . . . . . 14
145 f1ocnvfv2 6183 . . . . . . . . . . . . . . 15
14617, 77, 145syl2anc 661 . . . . . . . . . . . . . 14
147144, 146syl5eq 2510 . . . . . . . . . . . . 13
148147fveq2d 5875 . . . . . . . . . . . 12
149143, 148eqtr2d 2499 . . . . . . . . . . 11
150149adantr 465 . . . . . . . . . 10
151141, 150oveq12d 6314 . . . . . . . . 9
15297, 151eqtr4d 2501 . . . . . . . 8
15389, 152syldan 470 . . . . . . 7
15485seqeq1d 12113 . . . . . . . . 9
155154fveq1d 5873 . . . . . . . 8
156155oveq1d 6311 . . . . . . 7
15784, 153, 1563eqtrd 2502 . . . . . 6
158 eluzel2 11115 . . . . . . . . . . . 12
15915, 158syl 16 . . . . . . . . . . 11
160 elfzuz 11713 . . . . . . . . . . 11
161 eluzp1m1 11133 . . . . . . . . . . 11
162159, 160, 161syl2an 477 . . . . . . . . . 10
163 eluzelz 11119 . . . . . . . . . . . . . . . . . . . . 21
16415, 163syl 16 . . . . . . . . . . . . . . . . . . . 20
165164zcnd 10995 . . . . . . . . . . . . . . . . . . 19
166 ax-1cn 9571 . . . . . . . . . . . . . . . . . . 19
167 pncan 9849 . . . . . . . . . . . . . . . . . . 19
168165, 166, 167sylancl 662 . . . . . . . . . . . . . . . . . 18
169 peano2zm 10932 . . . . . . . . . . . . . . . . . . . 20
17079, 80, 1693syl 20 . . . . . . . . . . . . . . . . . . 19
171 elfzuz3 11714 . . . . . . . . . . . . . . . . . . . . 21
17279, 171syl 16 . . . . . . . . . . . . . . . . . . . 20
173117zcnd 10995 . . . . . . . . . . . . . . . . . . . . . 22
174 npcan 9852 . . . . . . . . . . . . . . . . . . . . . 22
175173, 166, 174sylancl 662 . . . . . . . . . . . . . . . . . . . . 21
176175fveq2d 5875 . . . . . . . . . . . . . . . . . . . 20
177172, 176eleqtrrd 2548 . . . . . . . . . . . . . . . . . . 19
178 eluzp1m1 11133 . . . . . . . . . . . . . . . . . . 19
179170, 177, 178syl2anc 661 . . . . . . . . . . . . . . . . . 18
180168, 179eqeltrrd 2546 . . . . . . . . . . . . . . . . 17
181 fzss2 11752 . . . . . . . . . . . . . . . . 17
182180, 181syl 16 . . . . . . . . . . . . . . . 16
183182sselda 3503 . . . . . . . . . . . . . . 15
184183, 103syldan 470 . . . . . . . . . . . . . 14
185184, 105syl 16 . . . . . . . . . . . . 13
186183, 113syl 16 . . . . . . . . . . . . . . 15
187 elfzm11 11778 . . . . . . . . . . . . . . . . . . 19
188159, 117, 187syl2anc 661 . . . . . . . . . . . . . . . . . 18
189188biimpa 484 . . . . . . . . . . . . . . . . 17
190189simp3d 1010 . . . . . . . . . . . . . . . 16
191 iftrue 3947 . . . . . . . . . . . . . . . . 17
192191fveq2d 5875 . . . . . . . . . . . . . . . 16
193190, 192syl 16 . . . . . . . . . . . . . . 15
194186, 193eqtrd 2498 . . . . . . . . . . . . . 14
195194fveq2d 5875 . . . . . . . . . . . . 13
196185, 195eqtr2d 2499 . . . . . . . . . . . 12
197 peano2uz 11163 . . . . . . . . . . . . . . 15
198 fzss2 11752 . . . . . . . . . . . . . . 15
199180, 197, 1983syl 20 . . . . . . . . . . . . . 14
200199sselda 3503 . . . . . . . . . . . . 13
201 fvco3 5950 . . . . . . . . . . . . . 14
20259, 201sylan 471 . . . . . . . . . . . . 13
203200, 202syldan 470 . . . . . . . . . . . 12
204183, 132syldan 470 . . . . . . . . . . . 12
205196, 203, 2043eqtr4d 2508 . . . . . . . . . . 11
206205adantlr 714 . . . . . . . . . 10
207162, 206seqfveq 12131 . . . . . . . . 9
208 fzp1ss 11760 . . . . . . . . . . . 12
20915, 158, 2083syl 20 . . . . . . . . . . 11
210209sselda 3503 . . . . . . . . . 10
211210, 152syldan 470 . . . . . . . . 9