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

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

Proof of Theorem seqf1olem1
StepHypRef Expression
1 seqf1olem.7 . 2
2 fvex 5881 . . 3
32a1i 11 . 2
4 fvex 5881 . . . 4
5 ovex 6324 . . . 4
64, 5ifex 4010 . . 3
76a1i 11 . 2
8 iftrue 3947 . . . . . . . . 9
98fveq2d 5875 . . . . . . . 8
109eqeq2d 2471 . . . . . . 7
1110adantl 466 . . . . . 6
12 simprr 757 . . . . . . . . 9
13 elfzelz 11717 . . . . . . . . . . . . 13
1413zred 10994 . . . . . . . . . . . 12
1514ad2antlr 726 . . . . . . . . . . 11
16 simprl 756 . . . . . . . . . . 11
1715, 16gtned 9741 . . . . . . . . . 10
18 seqf1olem.5 . . . . . . . . . . . . . . . . 17
19 f1of 5821 . . . . . . . . . . . . . . . . 17
2018, 19syl 16 . . . . . . . . . . . . . . . 16
2120ad2antrr 725 . . . . . . . . . . . . . . 15
22 fzssp1 11755 . . . . . . . . . . . . . . . 16
23 simplr 755 . . . . . . . . . . . . . . . 16
2422, 23sseldi 3501 . . . . . . . . . . . . . . 15
2521, 24ffvelrnd 6032 . . . . . . . . . . . . . 14
26 seqf1o.4 . . . . . . . . . . . . . . . 16
27 elfzp1 11759 . . . . . . . . . . . . . . . 16
2826, 27syl 16 . . . . . . . . . . . . . . 15
2928ad2antrr 725 . . . . . . . . . . . . . 14
3025, 29mpbid 210 . . . . . . . . . . . . 13
3130ord 377 . . . . . . . . . . . 12
3218ad2antrr 725 . . . . . . . . . . . . . 14
33 f1ocnvfv 6184 . . . . . . . . . . . . . 14
3432, 24, 33syl2anc 661 . . . . . . . . . . . . 13
35 seqf1olem.8 . . . . . . . . . . . . . 14
3635eqeq1i 2464 . . . . . . . . . . . . 13
3734, 36syl6ibr 227 . . . . . . . . . . . 12
3831, 37syld 44 . . . . . . . . . . 11
3938necon1ad 2673 . . . . . . . . . 10
4017, 39mpd 15 . . . . . . . . 9
4112, 40eqeltrd 2545 . . . . . . . 8
4212eqcomd 2465 . . . . . . . . . . . 12
43 f1ocnvfv 6184 . . . . . . . . . . . . 13
4432, 24, 43syl2anc 661 . . . . . . . . . . . 12
4542, 44mpd 15 . . . . . . . . . . 11
4645, 16eqbrtrd 4472 . . . . . . . . . 10
47 iftrue 3947 . . . . . . . . . 10
4846, 47syl 16 . . . . . . . . 9
4948, 45eqtr2d 2499 . . . . . . . 8
5041, 49jca 532 . . . . . . 7
5150expr 615 . . . . . 6
5211, 51sylbid 215 . . . . 5
53 iffalse 3950 . . . . . . . . 9
5453fveq2d 5875 . . . . . . . 8
5554eqeq2d 2471 . . . . . . 7
5655adantl 466 . . . . . 6
57 simprr 757 . . . . . . . . 9
58 f1ocnv 5833 . . . . . . . . . . . . . . . . . . 19
5918, 58syl 16 . . . . . . . . . . . . . . . . . 18
60 f1of1 5820 . . . . . . . . . . . . . . . . . 18
6159, 60syl 16 . . . . . . . . . . . . . . . . 17
62 f1f 5786 . . . . . . . . . . . . . . . . 17
6361, 62syl 16 . . . . . . . . . . . . . . . 16
64 peano2uz 11163 . . . . . . . . . . . . . . . . . 18
6526, 64syl 16 . . . . . . . . . . . . . . . . 17
66 eluzfz2 11723 . . . . . . . . . . . . . . . . 17
6765, 66syl 16 . . . . . . . . . . . . . . . 16
6863, 67ffvelrnd 6032 . . . . . . . . . . . . . . 15
6935, 68syl5eqel 2549 . . . . . . . . . . . . . 14
70 elfzelz 11717 . . . . . . . . . . . . . 14
7169, 70syl 16 . . . . . . . . . . . . 13
7271zred 10994 . . . . . . . . . . . 12
7372ad2antrr 725 . . . . . . . . . . 11
7414ad2antlr 726 . . . . . . . . . . . 12
75 peano2re 9774 . . . . . . . . . . . . 13
7674, 75syl 16 . . . . . . . . . . . 12
77 simprl 756 . . . . . . . . . . . . 13
7873, 74lenltd 9752 . . . . . . . . . . . . 13
7977, 78mpbird 232 . . . . . . . . . . . 12
8074ltp1d 10501 . . . . . . . . . . . 12
8173, 74, 76, 79, 80lelttrd 9761 . . . . . . . . . . 11
8273, 81ltned 9742 . . . . . . . . . 10
8320ad2antrr 725 . . . . . . . . . . . . . . 15
84 fzp1elp1 11762 . . . . . . . . . . . . . . . 16
8584ad2antlr 726 . . . . . . . . . . . . . . 15
8683, 85ffvelrnd 6032 . . . . . . . . . . . . . 14
87 elfzp1 11759 . . . . . . . . . . . . . . . 16
8826, 87syl 16 . . . . . . . . . . . . . . 15
8988ad2antrr 725 . . . . . . . . . . . . . 14
9086, 89mpbid 210 . . . . . . . . . . . . 13
9190ord 377 . . . . . . . . . . . 12
9218ad2antrr 725 . . . . . . . . . . . . . 14
93 f1ocnvfv 6184 . . . . . . . . . . . . . 14
9492, 85, 93syl2anc 661 . . . . . . . . . . . . 13
9535eqeq1i 2464 . . . . . . . . . . . . 13
9694, 95syl6ibr 227 . . . . . . . . . . . 12
9791, 96syld 44 . . . . . . . . . . 11
9897necon1ad 2673 . . . . . . . . . 10
9982, 98mpd 15 . . . . . . . . 9
10057, 99eqeltrd 2545 . . . . . . . 8
10157eqcomd 2465 . . . . . . . . . . . . . 14
102 f1ocnvfv 6184 . . . . . . . . . . . . . . 15
10392, 85, 102syl2anc 661 . . . . . . . . . . . . . 14
104101, 103mpd 15 . . . . . . . . . . . . 13
105104breq1d 4462 . . . . . . . . . . . 12
106 lttr 9682 . . . . . . . . . . . . . 14
10774, 76, 73, 106syl3anc 1228 . . . . . . . . . . . . 13
10880, 107mpand 675 . . . . . . . . . . . 12
109105, 108sylbid 215 . . . . . . . . . . 11
11077, 109mtod 177 . . . . . . . . . 10
111 iffalse 3950 . . . . . . . . . 10
112110, 111syl 16 . . . . . . . . 9
113104oveq1d 6311 . . . . . . . . 9
11474recnd 9643 . . . . . . . . . 10
115 ax-1cn 9571 . . . . . . . . . 10
116 pncan 9849 . . . . . . . . . 10
117114, 115, 116sylancl 662 . . . . . . . . 9
118112, 113, 1173eqtrrd 2503 . . . . . . . 8
119100, 118jca 532 . . . . . . 7
120119expr 615 . . . . . 6
12156, 120sylbid 215 . . . . 5
12252, 121pm2.61dan 791 . . . 4
123122expimpd 603 . . 3
12447eqeq2d 2471 . . . . . . 7
125124adantl 466 . . . . . 6
126 simprr 757 . . . . . . . . . . 11
12763ad2antrr 725 . . . . . . . . . . . 12
128 simplr 755 . . . . . . . . . . . . 13
12922, 128sseldi 3501 . . . . . . . . . . . 12
130127, 129ffvelrnd 6032 . . . . . . . . . . 11
131126, 130eqeltrd 2545 . . . . . . . . . 10
132 elfzle1 11718 . . . . . . . . . 10
133131, 132syl 16 . . . . . . . . 9
134 elfzelz 11717 . . . . . . . . . . . . 13
135131, 134syl 16 . . . . . . . . . . . 12
136135zred 10994 . . . . . . . . . . 11
13772ad2antrr 725 . . . . . . . . . . 11
138 eluzelz 11119 . . . . . . . . . . . . . . 15
13926, 138syl 16 . . . . . . . . . . . . . 14
140139peano2zd 10997 . . . . . . . . . . . . 13
141140zred 10994 . . . . . . . . . . . 12
142141ad2antrr 725 . . . . . . . . . . 11
143 simprl 756 . . . . . . . . . . . 12
144126, 143eqbrtrd 4472 . . . . . . . . . . 11
145 elfzle2 11719 . . . . . . . . . . . . 13
14669, 145syl 16 . . . . . . . . . . . 12
147146ad2antrr 725 . . . . . . . . . . 11
148136, 137, 142, 144, 147ltletrd 9763 . . . . . . . . . 10
149139ad2antrr 725 . . . . . . . . . . 11
150 zleltp1 10939 . . . . . . . . . . 11
151135, 149, 150syl2anc 661 . . . . . . . . . 10
152148, 151mpbird 232 . . . . . . . . 9
153 eluzel2 11115 . . . . . . . . . . . 12
15426, 153syl 16 . . . . . . . . . . 11
155154ad2antrr 725 . . . . . . . . . 10
156 elfz 11707 . . . . . . . . . 10
157135, 155, 149, 156syl3anc 1228 . . . . . . . . 9
158133, 152, 157mpbir2and 922 . . . . . . . 8
159144, 9syl 16 . . . . . . . . 9
160126fveq2d 5875 . . . . . . . . 9
16118ad2antrr 725 . . . . . . . . . 10
162 f1ocnvfv2 6183 . . . . . . . . . 10
163161, 129, 162syl2anc 661 . . . . . . . . 9
164159, 160, 1633eqtrrd 2503 . . . . . . . 8
165158, 164jca 532 . . . . . . 7
166165expr 615 . . . . . 6
167125, 166sylbid 215 . . . . 5
168111eqeq2d 2471 . . . . . . 7
169168adantl 466 . . . . . 6
170154zred 10994 . . . . . . . . . . 11
171170ad2antrr 725 . . . . . . . . . 10
17272ad2antrr 725 . . . . . . . . . 10
173