Proof of Theorem poimirlem6
Step | Hyp | Ref
| Expression |
1 | | poimirlem9.1 |
. . . . . . . 8
|
2 | | elrabi 3359 |
. . . . . . . . 9
..^
..^ |
3 | | poimirlem22.s |
. . . . . . . . 9
..^ |
4 | 2, 3 | eleq2s 2719 |
. . . . . . . 8
..^ |
5 | 1, 4 | syl 17 |
. . . . . . 7
..^ |
6 | | xp1st 7198 |
. . . . . . 7
..^ ..^ |
7 | 5, 6 | syl 17 |
. . . . . 6
..^ |
8 | | xp2nd 7199 |
. . . . . 6
..^ |
9 | 7, 8 | syl 17 |
. . . . 5
|
10 | | fvex 6201 |
. . . . . 6
|
11 | | f1oeq1 6127 |
. . . . . 6
|
12 | 10, 11 | elab 3350 |
. . . . 5
|
13 | 9, 12 | sylib 208 |
. . . 4
|
14 | | f1of 6137 |
. . . 4
|
15 | 13, 14 | syl 17 |
. . 3
|
16 | | poimirlem9.2 |
. . . . . . . . 9
|
17 | | elfznn 12370 |
. . . . . . . . 9
|
18 | 16, 17 | syl 17 |
. . . . . . . 8
|
19 | 18 | nnzd 11481 |
. . . . . . 7
|
20 | | peano2zm 11420 |
. . . . . . 7
|
21 | 19, 20 | syl 17 |
. . . . . 6
|
22 | | poimir.0 |
. . . . . . 7
|
23 | 22 | nnzd 11481 |
. . . . . 6
|
24 | 21 | zred 11482 |
. . . . . . 7
|
25 | 18 | nnred 11035 |
. . . . . . 7
|
26 | 22 | nnred 11035 |
. . . . . . 7
|
27 | 25 | lem1d 10957 |
. . . . . . 7
|
28 | | nnm1nn0 11334 |
. . . . . . . . . 10
|
29 | 22, 28 | syl 17 |
. . . . . . . . 9
|
30 | 29 | nn0red 11352 |
. . . . . . . 8
|
31 | | elfzle2 12345 |
. . . . . . . . 9
|
32 | 16, 31 | syl 17 |
. . . . . . . 8
|
33 | 26 | lem1d 10957 |
. . . . . . . 8
|
34 | 25, 30, 26, 32, 33 | letrd 10194 |
. . . . . . 7
|
35 | 24, 25, 26, 27, 34 | letrd 10194 |
. . . . . 6
|
36 | | eluz2 11693 |
. . . . . 6
|
37 | 21, 23, 35, 36 | syl3anbrc 1246 |
. . . . 5
|
38 | | fzss2 12381 |
. . . . 5
|
39 | 37, 38 | syl 17 |
. . . 4
|
40 | | poimirlem6.3 |
. . . 4
|
41 | 39, 40 | sseldd 3604 |
. . 3
|
42 | 15, 41 | ffvelrnd 6360 |
. 2
|
43 | | xp1st 7198 |
. . . . . . . . . . . . 13
..^ ..^ |
44 | 7, 43 | syl 17 |
. . . . . . . . . . . 12
..^ |
45 | | elmapfn 7880 |
. . . . . . . . . . . 12
..^ |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
|
47 | 46 | adantr 481 |
. . . . . . . . . 10
|
48 | | 1ex 10035 |
. . . . . . . . . . . . . . 15
|
49 | | fnconstg 6093 |
. . . . . . . . . . . . . . 15
|
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
51 | | c0ex 10034 |
. . . . . . . . . . . . . . 15
|
52 | | fnconstg 6093 |
. . . . . . . . . . . . . . 15
|
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
54 | 50, 53 | pm3.2i 471 |
. . . . . . . . . . . . 13
|
55 | | dff1o3 6143 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
57 | 13, 56 | syl 17 |
. . . . . . . . . . . . . . 15
|
58 | | imain 5974 |
. . . . . . . . . . . . . . 15
|
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
|
60 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | 40, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 61 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
|
63 | 62 | ltm1d 10956 |
. . . . . . . . . . . . . . . . 17
|
64 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . 17
|
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | imaeq2d 5466 |
. . . . . . . . . . . . . . 15
|
67 | | ima0 5481 |
. . . . . . . . . . . . . . 15
|
68 | 66, 67 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
69 | 59, 68 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
70 | | fnun 5997 |
. . . . . . . . . . . . 13
|
71 | 54, 69, 70 | sylancr 695 |
. . . . . . . . . . . 12
|
72 | 61 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | | npcan1 10455 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
75 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 61, 75 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 74, 76 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
|
78 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
79 | 61, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
80 | 79 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
81 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
83 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | 74, 84 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | | uzss 11708 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 61 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . 22
|
90 | 40, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | 62, 24, 26, 90, 35 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
|
92 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | 88, 23, 91, 92 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 87, 93 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
|
95 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . . 18
|
96 | 77, 94, 95 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
97 | 74 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
98 | 97 | uneq2d 3767 |
. . . . . . . . . . . . . . . . 17
|
99 | 96, 98 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | imaeq2d 5466 |
. . . . . . . . . . . . . . 15
|
101 | | imaundi 5545 |
. . . . . . . . . . . . . . 15
|
102 | 100, 101 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
103 | | f1ofo 6144 |
. . . . . . . . . . . . . . . 16
|
104 | 13, 103 | syl 17 |
. . . . . . . . . . . . . . 15
|
105 | | foima 6120 |
. . . . . . . . . . . . . . 15
|
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
|
107 | 102, 106 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
108 | 107 | fneq2d 5982 |
. . . . . . . . . . . 12
|
109 | 71, 108 | mpbid 222 |
. . . . . . . . . . 11
|
110 | 109 | adantr 481 |
. . . . . . . . . 10
|
111 | | ovexd 6680 |
. . . . . . . . . 10
|
112 | | inidm 3822 |
. . . . . . . . . 10
|
113 | | eqidd 2623 |
. . . . . . . . . 10
|
114 | | imaundi 5545 |
. . . . . . . . . . . . . . . . . 18
|
115 | | fzpred 12389 |
. . . . . . . . . . . . . . . . . . . 20
|
116 | 93, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
117 | 116 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . 18
|
118 | | f1ofn 6138 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 13, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | | fnsnfv 6258 |
. . . . . . . . . . . . . . . . . . . 20
|
121 | 119, 41, 120 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
122 | 121 | uneq1d 3766 |
. . . . . . . . . . . . . . . . . 18
|
123 | 114, 117,
122 | 3eqtr4a 2682 |
. . . . . . . . . . . . . . . . 17
|
124 | 123 | xpeq1d 5138 |
. . . . . . . . . . . . . . . 16
|
125 | | xpundir 5172 |
. . . . . . . . . . . . . . . 16
|
126 | 124, 125 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
127 | 126 | uneq2d 3767 |
. . . . . . . . . . . . . 14
|
128 | | un12 3771 |
. . . . . . . . . . . . . 14
|
129 | 127, 128 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
130 | 129 | fveq1d 6193 |
. . . . . . . . . . . 12
|
131 | 130 | ad2antrr 762 |
. . . . . . . . . . 11
|
132 | | fnconstg 6093 |
. . . . . . . . . . . . . . . . 17
|
133 | 51, 132 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
134 | 50, 133 | pm3.2i 471 |
. . . . . . . . . . . . . . 15
|
135 | | imain 5974 |
. . . . . . . . . . . . . . . . 17
|
136 | 57, 135 | syl 17 |
. . . . . . . . . . . . . . . 16
|
137 | 79 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
|
138 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . 21
|
139 | 62, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
140 | 62 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | 137, 62, 139, 63, 140 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . 19
|
142 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . . . 19
|
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
144 | 143 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . 17
|
145 | 144, 67 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
146 | 136, 145 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
147 | | fnun 5997 |
. . . . . . . . . . . . . . 15
|
148 | 134, 146,
147 | sylancr 695 |
. . . . . . . . . . . . . 14
|
149 | | imaundi 5545 |
. . . . . . . . . . . . . . . 16
|
150 | | imadif 5973 |
. . . . . . . . . . . . . . . . . 18
|
151 | 57, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
152 | | fzsplit 12367 |
. . . . . . . . . . . . . . . . . . . . 21
|
153 | 41, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
154 | 153 | difeq1d 3727 |
. . . . . . . . . . . . . . . . . . 19
|
155 | | difundir 3880 |
. . . . . . . . . . . . . . . . . . . 20
|
156 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
157 | 77, 85, 156 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
158 | 74 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
159 | | fzsn 12383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
160 | 88, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
161 | 158, 160 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
162 | 161 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
163 | 157, 162 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
164 | 163 | difeq1d 3727 |
. . . . . . . . . . . . . . . . . . . . . 22
|
165 | | difun2 4048 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
166 | 137, 62 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
167 | 63, 166 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
168 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
169 | 167, 168 | nsyl 135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
170 | | difsn 4328 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
172 | 165, 171 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . 22
|
173 | 164, 172 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
174 | 62, 139 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
175 | 140, 174 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
176 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
177 | 175, 176 | nsyl 135 |
. . . . . . . . . . . . . . . . . . . . . 22
|
178 | | difsn 4328 |
. . . . . . . . . . . . . . . . . . . . . 22
|
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
180 | 173, 179 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . 20
|
181 | 155, 180 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
|
182 | 154, 181 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
183 | 182 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . 17
|
184 | 121 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
185 | 106, 184 | difeq12d 3729 |
. . . . . . . . . . . . . . . . 17
|
186 | 151, 183,
185 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
|
187 | 149, 186 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
|
188 | 187 | fneq2d 5982 |
. . . . . . . . . . . . . 14
|
189 | 148, 188 | mpbid 222 |
. . . . . . . . . . . . 13
|
190 | | eldifsn 4317 |
. . . . . . . . . . . . . . 15
|
191 | 190 | biimpri 218 |
. . . . . . . . . . . . . 14
|
192 | 191 | ancoms 469 |
. . . . . . . . . . . . 13
|
193 | | disjdif 4040 |
. . . . . . . . . . . . . 14
|
194 | | fnconstg 6093 |
. . . . . . . . . . . . . . . 16
|
195 | 51, 194 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
196 | | fvun2 6270 |
. . . . . . . . . . . . . . 15
|
197 | 195, 196 | mp3an1 1411 |
. . . . . . . . . . . . . 14
|
198 | 193, 197 | mpanr1 719 |
. . . . . . . . . . . . 13
|
199 | 189, 192,
198 | syl2an 494 |
. . . . . . . . . . . 12
|
200 | 199 | anassrs 680 |
. . . . . . . . . . 11
|
201 | 131, 200 | eqtrd 2656 |
. . . . . . . . . 10
|
202 | 47, 110, 111, 111, 112, 113, 201 | ofval 6906 |
. . . . . . . . 9
|
203 | | fnconstg 6093 |
. . . . . . . . . . . . . . 15
|
204 | 48, 203 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
205 | 204, 133 | pm3.2i 471 |
. . . . . . . . . . . . 13
|
206 | | imain 5974 |
. . . . . . . . . . . . . . 15
|
207 | 57, 206 | syl 17 |
. . . . . . . . . . . . . 14
|
208 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . 17
|
209 | 140, 208 | syl 17 |
. . . . . . . . . . . . . . . 16
|
210 | 209 | imaeq2d 5466 |
. . . . . . . . . . . . . . 15
|
211 | 210, 67 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
212 | 207, 211 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
213 | | fnun 5997 |
. . . . . . . . . . . . 13
|
214 | 205, 212,
213 | sylancr 695 |
. . . . . . . . . . . 12
|
215 | 153 | imaeq2d 5466 |
. . . . . . . . . . . . . . 15
|
216 | | imaundi 5545 |
. . . . . . . . . . . . . . 15
|
217 | 215, 216 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
218 | 217, 106 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
219 | 218 | fneq2d 5982 |
. . . . . . . . . . . 12
|
220 | 214, 219 | mpbid 222 |
. . . . . . . . . . 11
|
221 | 220 | adantr 481 |
. . . . . . . . . 10
|
222 | | imaundi 5545 |
. . . . . . . . . . . . . . . . . 18
|
223 | 163 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . 18
|
224 | 121 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . 18
|
225 | 222, 223,
224 | 3eqtr4a 2682 |
. . . . . . . . . . . . . . . . 17
|
226 | 225 | xpeq1d 5138 |
. . . . . . . . . . . . . . . 16
|
227 | | xpundir 5172 |
. . . . . . . . . . . . . . . 16
|
228 | 226, 227 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
229 | 228 | uneq1d 3766 |
. . . . . . . . . . . . . 14
|
230 | | un23 3772 |
. . . . . . . . . . . . . . 15
|
231 | 230 | equncomi 3759 |
. . . . . . . . . . . . . 14
|
232 | 229, 231 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
233 | 232 | fveq1d 6193 |
. . . . . . . . . . . 12
|
234 | 233 | ad2antrr 762 |
. . . . . . . . . . 11
|
235 | | fnconstg 6093 |
. . . . . . . . . . . . . . . 16
|
236 | 48, 235 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
237 | | fvun2 6270 |
. . . . . . . . . . . . . . 15
|
238 | 236, 237 | mp3an1 1411 |
. . . . . . . . . . . . . 14
|
239 | 193, 238 | mpanr1 719 |
. . . . . . . . . . . . 13
|
240 | 189, 192,
239 | syl2an 494 |
. . . . . . . . . . . 12
|
241 | 240 | anassrs 680 |
. . . . . . . . . . 11
|
242 | 234, 241 | eqtrd 2656 |
. . . . . . . . . 10
|
243 | 47, 221, 111, 111, 112, 113, 242 | ofval 6906 |
. . . . . . . . 9
|
244 | 202, 243 | eqtr4d 2659 |
. . . . . . . 8
|
245 | 244 | an32s 846 |
. . . . . . 7
|
246 | 245 | anasss 679 |
. . . . . 6
|
247 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
248 | 247 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
|
249 | 248 | ifbid 4108 |
. . . . . . . . . . . . . . . 16
|
250 | 249 | csbeq1d 3540 |
. . . . . . . . . . . . . . 15
|
251 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
252 | 251 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
253 | 251 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
254 | 253 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . 19
|
255 | 254 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . 18
|
256 | 253 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . 19
|
257 | 256 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . 18
|
258 | 255, 257 | uneq12d 3768 |
. . . . . . . . . . . . . . . . 17
|
259 | 252, 258 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
260 | 259 | csbeq2dv 3992 |
. . . . . . . . . . . . . . 15
|
261 | 250, 260 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
262 | 261 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
|
263 | 262 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
264 | 263, 3 | elrab2 3366 |
. . . . . . . . . . 11
..^
|
265 | 264 | simprbi 480 |
. . . . . . . . . 10
|
266 | 1, 265 | syl 17 |
. . . . . . . . 9
|
267 | | breq1 4656 |
. . . . . . . . . . . . 13
|
268 | | id 22 |
. . . . . . . . . . . . 13
|
269 | 267, 268 | ifbieq1d 4109 |
. . . . . . . . . . . 12
|
270 | 25 | ltm1d 10956 |
. . . . . . . . . . . . . . 15
|
271 | 62, 24, 25, 90, 270 | lelttrd 10195 |
. . . . . . . . . . . . . 14
|
272 | 137, 62, 25, 63, 271 | lttrd 10198 |
. . . . . . . . . . . . 13
|
273 | 272 | iftrued 4094 |
. . . . . . . . . . . 12
|
274 | 269, 273 | sylan9eqr 2678 |
. . . . . . . . . . 11
|
275 | 274 | csbeq1d 3540 |
. . . . . . . . . 10
|
276 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
277 | 276 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
|
278 | 277 | xpeq1d 5138 |
. . . . . . . . . . . . . . 15
|
279 | 278 | adantl 482 |
. . . . . . . . . . . . . 14
|
280 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
281 | 280, 74 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . 17
|
282 | 281 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
283 | 282 | imaeq2d 5466 |
. . . . . . . . . . . . . . 15
|
284 | 283 | xpeq1d 5138 |
. . . . . . . . . . . . . 14
|
285 | 279, 284 | uneq12d 3768 |
. . . . . . . . . . . . 13
|
286 | 285 | oveq2d 6666 |
. . . . . . . . . . . 12
|
287 | 79, 286 | csbied 3560 |
. . . . . . . . . . 11
|
288 | 287 | adantr 481 |
. . . . . . . . . 10
|
289 | 275, 288 | eqtrd 2656 |
. . . . . . . . 9
|
290 | | 1red 10055 |
. . . . . . . . . . 11
|
291 | 62, 26, 290, 91 | lesub1dd 10643 |
. . . . . . . . . 10
|
292 | | elfz2nn0 12431 |
. . . . . . . . . 10
|
293 | 79, 29, 291, 292 | syl3anbrc 1246 |
. . . . . . . . 9
|
294 | | ovexd 6680 |
. . . . . . . . 9
|
295 | 266, 289,
293, 294 | fvmptd 6288 |
. . . . . . . 8
|
296 | 295 | fveq1d 6193 |
. . . . . . 7
|
297 | 296 | adantr 481 |
. . . . . 6
|
298 | | breq1 4656 |
. . . . . . . . . . . . 13
|
299 | | id 22 |
. . . . . . . . . . . . 13
|
300 | 298, 299 | ifbieq1d 4109 |
. . . . . . . . . . . 12
|
301 | 271 | iftrued 4094 |
. . . . . . . . . . . 12
|
302 | 300, 301 | sylan9eqr 2678 |
. . . . . . . . . . 11
|
303 | 302 | csbeq1d 3540 |
. . . . . . . . . 10
|
304 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
305 | 304 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
|
306 | 305 | xpeq1d 5138 |
. . . . . . . . . . . . . . 15
|
307 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
308 | 307 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
309 | 308 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
|
310 | 309 | xpeq1d 5138 |
. . . . . . . . . . . . . . 15
|
311 | 306, 310 | uneq12d 3768 |
. . . . . . . . . . . . . 14
|
312 | 311 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
313 | 312 | adantl 482 |
. . . . . . . . . . . 12
|
314 | 40, 313 | csbied 3560 |
. . . . . . . . . . 11
|
315 | 314 | adantr 481 |
. . . . . . . . . 10
|
316 | 303, 315 | eqtrd 2656 |
. . . . . . . . 9
|
317 | 29 | nn0zd 11480 |
. . . . . . . . . . . . 13
|
318 | 25, 26, 290, 34 | lesub1dd 10643 |
. . . . . . . . . . . . 13
|
319 | | eluz2 11693 |
. . . . . . . . . . . . 13
|
320 | 21, 317, 318, 319 | syl3anbrc 1246 |
. . . . . . . . . . . 12
|
321 | | fzss2 12381 |
. . . . . . . . . . . 12
|
322 | 320, 321 | syl 17 |
. . . . . . . . . . 11
|
323 | | 1eluzge0 11732 |
. . . . . . . . . . . 12
|
324 | | fzss1 12380 |
. . . . . . . . . . . 12
|
325 | 323, 324 | ax-mp 5 |
. . . . . . . . . . 11
|
326 | 322, 325 | syl6ss 3615 |
. . . . . . . . . 10
|
327 | 326, 40 | sseldd 3604 |
. . . . . . . . 9
|
328 | | ovexd 6680 |
. . . . . . . . 9
|
329 | 266, 316,
327, 328 | fvmptd 6288 |
. . . . . . . 8
|
330 | 329 | fveq1d 6193 |
. . . . . . 7
|
331 | 330 | adantr 481 |
. . . . . 6
|
332 | 246, 297,
331 | 3eqtr4d 2666 |
. . . . 5
|
333 | 332 | expr 643 |
. . . 4
|
334 | 333 | necon1d 2816 |
. . 3
|
335 | | elmapi 7879 |
. . . . . . . . . . 11
..^ ..^ |
336 | 44, 335 | syl 17 |
. . . . . . . . . 10
..^ |
337 | 336, 42 | ffvelrnd 6360 |
. . . . . . . . 9
..^ |
338 | | elfzonn0 12512 |
. . . . . . . . 9
..^ |
339 | 337, 338 | syl 17 |
. . . . . . . 8
|
340 | 339 | nn0red 11352 |
. . . . . . 7
|
341 | 340 | ltp1d 10954 |
. . . . . . 7
|
342 | 340, 341 | ltned 10173 |
. . . . . 6
|
343 | 295 | fveq1d 6193 |
. . . . . . 7
|
344 | | ovexd 6680 |
. . . . . . . . 9
|
345 | | eqidd 2623 |
. . . . . . . . 9
|
346 | | fzss1 12380 |
. . . . . . . . . . . . . 14
|
347 | 76, 346 | syl 17 |
. . . . . . . . . . . . 13
|
348 | | eluzfz1 12348 |
. . . . . . . . . . . . . 14
|
349 | 93, 348 | syl 17 |
. . . . . . . . . . . . 13
|
350 | | fnfvima 6496 |
. . . . . . . . . . . . 13
|
351 | 119, 347,
349, 350 | syl3anc 1326 |
. . . . . . . . . . . 12
|
352 | | fvun2 6270 |
. . . . . . . . . . . . 13
|
353 | 50, 53, 352 | mp3an12 1414 |
. . . . . . . . . . . 12
|
354 | 69, 351, 353 | syl2anc 693 |
. . . . . . . . . . 11
|
355 | 51 | fvconst2 6469 |
. . . . . . . . . . . 12
|
356 | 351, 355 | syl 17 |
. . . . . . . . . . 11
|
357 | 354, 356 | eqtrd 2656 |
. . . . . . . . . 10
|
358 | 357 | adantr 481 |
. . . . . . . . 9
|
359 | 46, 109, 344, 344, 112, 345, 358 | ofval 6906 |
. . . . . . . 8
|
360 | 42, 359 | mpdan 702 |
. . . . . . 7
|
361 | 339 | nn0cnd 11353 |
. . . . . . . 8
|
362 | 361 | addid1d 10236 |
. . . . . . 7
|
363 | 343, 360,
362 | 3eqtrd 2660 |
. . . . . 6
|
364 | 329 | fveq1d 6193 |
. . . . . . 7
|
365 | | fzss2 12381 |
. . . . . . . . . . . . . 14
|
366 | 93, 365 | syl 17 |
. . . . . . . . . . . . 13
|
367 | | elfz1end 12371 |
. . . . . . . . . . . . . 14
|
368 | 61, 367 | sylib 208 |
. . . . . . . . . . . . 13
|
369 | | fnfvima 6496 |
. . . . . . . . . . . . 13
|
370 | 119, 366,
368, 369 | syl3anc 1326 |
. . . . . . . . . . . 12
|
371 | | fvun1 6269 |
. . . . . . . . . . . . 13
|
372 | 204, 133,
371 | mp3an12 1414 |
. . . . . . . . . . . 12
|
373 | 212, 370,
372 | syl2anc 693 |
. . . . . . . . . . 11
|
374 | 48 | fvconst2 6469 |
. . . . . . . . . . . 12
|
375 | 370, 374 | syl 17 |
. . . . . . . . . . 11
|
376 | 373, 375 | eqtrd 2656 |
. . . . . . . . . 10
|
377 | 376 | adantr 481 |
. . . . . . . . 9
|
378 | 46, 220, 344, 344, 112, 345, 377 | ofval 6906 |
. . . . . . . 8
|
379 | 42, 378 | mpdan 702 |
. . . . . . 7
|
380 | 364, 379 | eqtrd 2656 |
. . . . . 6
|
381 | 342, 363,
380 | 3netr4d 2871 |
. . . . 5
|
382 | | fveq2 6191 |
. . . . . 6
|
383 | | fveq2 6191 |
. . . . . 6
|
384 | 382, 383 | neeq12d 2855 |
. . . . 5
|
385 | 381, 384 | syl5ibrcom 237 |
. . . 4
|
386 | 385 | adantr 481 |
. . 3
|
387 | 334, 386 | impbid 202 |
. 2
|
388 | 42, 387 | riota5 6637 |
1
|