Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem50 Structured version   Unicode version

Theorem fourierdlem50 31780
 Description: Continuity of and its limits with respect to the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem50.xre
fourierdlem50.p ..^
fourierdlem50.m
fourierdlem50.v
fourierdlem50.a
fourierdlem50.b
fourierdlem50.altb
fourierdlem50.ab
fourierdlem50.q
fourierdlem50.t
fourierdlem50.n
fourierdlem50.s
fourierdlem50.j ..^
fourierdlem50.u ..^
fourierdlem50.ch ..^ ..^
Assertion
Ref Expression
fourierdlem50 ..^
Distinct variable groups:   ,,   ,,   ,,,   ,   ,,   ,   ,,   ,   ,   ,,   ,   ,,   ,,   ,   ,,
Allowed substitution hints:   (,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,)   (,)   (,,,)   (,,,)   (,,)   ()   (,,,)   (,)   ()

Proof of Theorem fourierdlem50
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem50.u . . 3 ..^
2 fourierdlem50.m . . . . . . . 8
3 fourierdlem50.a . . . . . . . 8
4 fourierdlem50.b . . . . . . . 8
5 fourierdlem50.altb . . . . . . . . 9
63, 4, 5ltled 9744 . . . . . . . 8
7 fourierdlem50.p . . . . . . . . . . . . 13 ..^
8 fourierdlem50.v . . . . . . . . . . . . 13
97, 2, 8fourierdlem15 31745 . . . . . . . . . . . 12
10 pire 22718 . . . . . . . . . . . . . . . . 17
1110renegcli 9892 . . . . . . . . . . . . . . . 16
1211a1i 11 . . . . . . . . . . . . . . 15
13 fourierdlem50.xre . . . . . . . . . . . . . . 15
1412, 13jca 532 . . . . . . . . . . . . . 14
15 readdcl 9587 . . . . . . . . . . . . . 14
1614, 15syl 16 . . . . . . . . . . . . 13
1710a1i 11 . . . . . . . . . . . . . . 15
1817, 13jca 532 . . . . . . . . . . . . . 14
19 readdcl 9587 . . . . . . . . . . . . . 14
2018, 19syl 16 . . . . . . . . . . . . 13
2116, 20iccssred 31426 . . . . . . . . . . . 12
229, 21fssd 5746 . . . . . . . . . . 11
2322ffvelrnda 6032 . . . . . . . . . 10
2413adantr 465 . . . . . . . . . 10
2523, 24resubcld 9999 . . . . . . . . 9
26 fourierdlem50.q . . . . . . . . 9
2725, 26fmptd 6056 . . . . . . . 8
2826a1i 11 . . . . . . . . . . 11
29 fveq2 5872 . . . . . . . . . . . . 13
3029oveq1d 6310 . . . . . . . . . . . 12
3130adantl 466 . . . . . . . . . . 11
32 nnssnn0 10810 . . . . . . . . . . . . . . 15
3332a1i 11 . . . . . . . . . . . . . 14
34 nn0uz 11128 . . . . . . . . . . . . . 14
3533, 34syl6sseq 3555 . . . . . . . . . . . . 13
3635, 2sseldd 3510 . . . . . . . . . . . 12
37 eluzfz1 11705 . . . . . . . . . . . 12
3836, 37syl 16 . . . . . . . . . . 11
3922, 38ffvelrnd 6033 . . . . . . . . . . . 12
4039, 13resubcld 9999 . . . . . . . . . . 11
4128, 31, 38, 40fvmptd 5962 . . . . . . . . . 10
427fourierdlem2 31732 . . . . . . . . . . . . . . . 16 ..^
432, 42syl 16 . . . . . . . . . . . . . . 15 ..^
448, 43mpbid 210 . . . . . . . . . . . . . 14 ..^
4544simprd 463 . . . . . . . . . . . . 13 ..^
4645simpld 459 . . . . . . . . . . . 12
4746simpld 459 . . . . . . . . . . 11
4847oveq1d 6310 . . . . . . . . . 10
4912recnd 9634 . . . . . . . . . . 11
5013recnd 9634 . . . . . . . . . . 11
5149, 50pncand 9943 . . . . . . . . . 10
5241, 48, 513eqtrd 2512 . . . . . . . . 9
5312rexrd 9655 . . . . . . . . . 10
5417rexrd 9655 . . . . . . . . . 10
55 fourierdlem50.ab . . . . . . . . . . 11
563leidd 10131 . . . . . . . . . . . 12
573, 4, 3, 56, 6eliccd 31425 . . . . . . . . . . 11
5855, 57sseldd 3510 . . . . . . . . . 10
59 iccgelb 11593 . . . . . . . . . 10
6053, 54, 58, 59syl3anc 1228 . . . . . . . . 9
6152, 60eqbrtrd 4473 . . . . . . . 8
624leidd 10131 . . . . . . . . . . . 12
633, 4, 4, 6, 62eliccd 31425 . . . . . . . . . . 11
6455, 63sseldd 3510 . . . . . . . . . 10
65 iccleub 11592 . . . . . . . . . 10
6653, 54, 64, 65syl3anc 1228 . . . . . . . . 9
67 fveq2 5872 . . . . . . . . . . . . 13
6867oveq1d 6310 . . . . . . . . . . . 12
6968adantl 466 . . . . . . . . . . 11
70 eluzfz2 11706 . . . . . . . . . . . 12
7136, 70syl 16 . . . . . . . . . . 11
7222, 71ffvelrnd 6033 . . . . . . . . . . . 12
7372, 13resubcld 9999 . . . . . . . . . . 11
7428, 69, 71, 73fvmptd 5962 . . . . . . . . . 10
7546simprd 463 . . . . . . . . . . 11
7675oveq1d 6310 . . . . . . . . . 10
7717recnd 9634 . . . . . . . . . . 11
7877, 50pncand 9943 . . . . . . . . . 10
7974, 76, 783eqtrrd 2513 . . . . . . . . 9
8066, 79breqtrd 4477 . . . . . . . 8
81 fourierdlem50.j . . . . . . . 8 ..^
82 eqid 2467 . . . . . . . 8
83 fourierdlem50.t . . . . . . . . . . 11
84 prfi 7807 . . . . . . . . . . . . 13
8584a1i 11 . . . . . . . . . . . 12
86 fzfid 12063 . . . . . . . . . . . . . 14
8726rnmptfi 31348 . . . . . . . . . . . . . 14
8886, 87syl 16 . . . . . . . . . . . . 13
89 infi 7755 . . . . . . . . . . . . 13
9088, 89syl 16 . . . . . . . . . . . 12
91 unfi 7799 . . . . . . . . . . . 12
9285, 90, 91syl2anc 661 . . . . . . . . . . 11
9383, 92syl5eqel 2559 . . . . . . . . . 10
943, 4jca 532 . . . . . . . . . . . . 13
95 prssg 4188 . . . . . . . . . . . . . 14
963, 4, 95syl2anc 661 . . . . . . . . . . . . 13
9794, 96mpbid 210 . . . . . . . . . . . 12
98 inss2 3724 . . . . . . . . . . . . . 14
99 ioossre 11598 . . . . . . . . . . . . . 14
10098, 99sstri 3518 . . . . . . . . . . . . 13
101100a1i 11 . . . . . . . . . . . 12
10297, 101unssd 3685 . . . . . . . . . . 11
10383, 102syl5eqss 3553 . . . . . . . . . 10
104 fourierdlem50.s . . . . . . . . . 10
105 fourierdlem50.n . . . . . . . . . 10
10693, 103, 104, 105fourierdlem36 31766 . . . . . . . . 9
107 isoeq5 6218 . . . . . . . . . 10
10883, 107ax-mp 5 . . . . . . . . 9
109106, 108sylib 196 . . . . . . . 8
110 eqid 2467 . . . . . . . 8 ..^ ..^
1112, 3, 4, 6, 27, 61, 80, 81, 82, 109, 110fourierdlem20 31750 . . . . . . 7 ..^
112 fourierdlem50.ch . . . . . . . . . . . . . 14 ..^ ..^
113112biimpri 206 . . . . . . . . . . . . 13 ..^ ..^
114112biimpi 194 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
115 simp-4l 765 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
116114, 115syl 16 . . . . . . . . . . . . . . . . . 18
117 simplr 754 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^
118114, 117syl 16 . . . . . . . . . . . . . . . . . 18 ..^
119116, 118jca 532 . . . . . . . . . . . . . . . . 17 ..^
120 simp-4r 766 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^
121114, 120syl 16 . . . . . . . . . . . . . . . . 17 ..^
122 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
123122ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
124114, 123syl 16 . . . . . . . . . . . . . . . . . . . . 21
125116, 22syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
126125, 124ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22
127116, 13syl 16 . . . . . . . . . . . . . . . . . . . . . 22
128126, 127resubcld 9999 . . . . . . . . . . . . . . . . . . . . 21
129 nfv 1683 . . . . . . . . . . . . . . . . . . . . . 22
130 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . 24
131 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . 26
132131oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . 25
133132eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . 24
134130, 133anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . 23
135 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . 24
136135, 132eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . 23
137134, 136imbi12d 320 . . . . . . . . . . . . . . . . . . . . . 22
13826fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . 22
139129, 137, 138chvar 1982 . . . . . . . . . . . . . . . . . . . . 21
140124, 128, 139syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
141140, 128eqeltrd 2555 . . . . . . . . . . . . . . . . . . 19
14227adantr 465 . . . . . . . . . . . . . . . . . . . . 21 ..^
143 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . 22 ..^
144143adantl 466 . . . . . . . . . . . . . . . . . . . . 21 ..^
145142, 144ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20 ..^
146116, 121, 145syl2anc 661 . . . . . . . . . . . . . . . . . . 19
147 isof1o 6220 . . . . . . . . . . . . . . . . . . . . . . . . 25
148106, 147syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
149 f1of 5822 . . . . . . . . . . . . . . . . . . . . . . . 24
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
151 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
15281, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
153150, 152ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22
154103, 153sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21
155116, 154syl 16 . . . . . . . . . . . . . . . . . . . 20
156 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
15781, 156syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
158150, 157ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . 23
159103, 158sseldd 3510 . . . . . . . . . . . . . . . . . . . . . 22
160116, 159syl 16 . . . . . . . . . . . . . . . . . . . . 21
161114simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23
162141rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24
16327adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
164 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
165164adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
166163, 165ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
167166rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
168119, 167syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
169160rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24
170155rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24
171 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
172171zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
173172ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
17481, 173syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
175 isorel 6221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
176109, 157, 152, 175syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . 26
177174, 176mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25
178116, 177syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
179162, 168, 169, 170, 178ioossioobi 31444 . . . . . . . . . . . . . . . . . . . . . . 23
180161, 179mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22
181180simpld 459 . . . . . . . . . . . . . . . . . . . . 21
182141, 160, 155, 181, 178lelttrd 9751 . . . . . . . . . . . . . . . . . . . 20
183 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
184114, 183syl 16 . . . . . . . . . . . . . . . . . . . . . 22
185 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
186185ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
187186ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
188114, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
189116, 188, 25syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
190188, 189, 138syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25
191190, 189eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . 24
192191rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . 23
193146rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . 23
194192, 193, 169, 170, 178ioossioobi 31444 . . . . . . . . . . . . . . . . . . . . . 22
195184, 194mpbid 210 . . . . . . . . . . . . . . . . . . . . 21
196195simprd 463 . . . . . . . . . . . . . . . . . . . 20
197141, 155, 146, 182, 196ltletrd 9753 . . . . . . . . . . . . . . . . . . 19
198141, 146, 127, 197ltadd2dd 9752 . . . . . . . . . . . . . . . . . 18
199140oveq2d 6311 . . . . . . . . . . . . . . . . . . . . 21
200116, 50syl 16 . . . . . . . . . . . . . . . . . . . . . 22
201 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . . . . 23
202201, 126sseldi 3507 . . . . . . . . . . . . . . . . . . . . . 22
203200, 202pncan3d 9945 . . . . . . . . . . . . . . . . . . . . 21
204199, 203eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20
205204eqcomd 2475 . . . . . . . . . . . . . . . . . . 19
206121, 143syl 16 . . . . . . . . . . . . . . . . . . . . . 22
20722adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
208207, 144ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
209116, 121, 208syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
210209, 127resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . 23
211206, 210jca 532 . . . . . . . . . . . . . . . . . . . . . 22
212 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . 25
213 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
214213oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . 26
215214eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . . 25
216212, 215anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24
217 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25
218217, 214eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . 24
219216, 218imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . 23
220219, 139vtoclg 3176 . . . . . . . . . . . . . . . . . . . . . 22
221206, 211, 220sylc 60 . . . . . . . . . . . . . . . . . . . . 21
222221oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20
223201, 209sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21
224200, 223pncan3d 9945 . . . . . . . . . . . . . . . . . . . 20
225222, 224eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19
226205, 225breq12d 4466 . . . . . . . . . . . . . . . . . 18
227198, 226mpbird 232 . . . . . . . . . . . . . . . . 17
228 nfv 1683 . . . . . . . . . . . . . . . . . 18 ..^ ..^
229 eleq1 2539 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
230229anbi2d 703 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^ ..^
231 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22
232231fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21
233232breq2d 4465 . . . . . . . . . . . . . . . . . . . 20
234230, 233anbi12d 710 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
235 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20
236235breq2d 4465 . . . . . . . . . . . . . . . . . . 19
237234, 236imbi12d 320 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
238 nfv 1683 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
239 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
240239anbi2d 703 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
241240anbi1d 704 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^ ..^ ..^
242 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22
243242breq1d 4463 . . . . . . . . . . . . . . . . . . . . 21
244241, 243anbi12d 710 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^ ..^
245242breq1d 4463 . . . . . . . . . . . . . . . . . . . 20
246244, 245imbi12d 320 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
247 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
248247ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
249 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
250249ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
251 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
252 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^ ..^ ..^
253 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
254249zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
255 peano2re 9764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
256254, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
257256ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
258247zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
259258ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
260257, 259lenltd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
261253, 260mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
262249peano2zd 10981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
263262ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
264247ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
265 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
266263, 264, 2653jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
267 eluz2 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
268266, 267sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
269268adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
270 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
271 0z 10887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
272271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
273 elfzoel2 11808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
274273ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
275 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
276275adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
277272, 274, 2763jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
278 0re 9608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
280275zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
281280adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
282254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
283 elfzole1 11816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
284283adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
285282, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
286282ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
287 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
288287adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
289282, 285, 281, 286, 288ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
290279, 282, 281, 284, 289lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
291279, 281, 290ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
292291adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
293280adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
294273zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
295294adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
296258adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
297 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
298297adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
299 elfzolt2 11817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
300299adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
301293, 296, 295, 298, 300lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
302293, 295, 301ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
303302adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
304277, 292, 303jca32 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
305 elfz2 11691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306304, 305sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
307306adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
308270, 307, 23syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
309308adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
310 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
311271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
312 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
313312adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
314278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
315313zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
316254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
317283adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
318316, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ..^
319316ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ..^
320 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
321320adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ..^
322316, 318, 315, 319, 321ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
323314, 316, 315, 317, 322lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
324314, 315, 323ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
325311, 313, 3243jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
326 eluz2 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
327325, 326sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
328327adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
329 elfzoel2 11808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
330329ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
331312zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
332331adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
333 peano2rem 9898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
334258, 333syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
335334adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
336294adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
337 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
338337adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
339258ltm1d 10490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
340334, 258, 294, 339, 299lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
341340adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
342332, 335, 336, 338, 341lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
343342adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
344343adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
345328, 330, 3443jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
346 elfzo2 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
347345, 346sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^ ..^
348185, 23sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
34945simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
350349r19.21bi 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
351348, 208, 350ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
352310, 347, 351syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
353352adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
354269, 309, 353monoord 12117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
355252, 261, 354syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
35622adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
357 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
358357adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
359356, 358ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
360359adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
361360adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
36222adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
363 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
364363adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
365362, 364ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
366365ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
367361, 366lenltd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
368355, 367mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
369368adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
370251, 369condan 792 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
371 zleltp1 10925 . . . . . . . . . . . . . . . . . . . . . . . 24
372248, 250, 371syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
373370, 372mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
374248, 250, 3733jca 1176 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
375 eluz2 11100 . . . . . . . . . . . . . . . . . . . . 21
376374, 375sylibr 212 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
37722ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
378271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
379273ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
380 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
381380adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
382378, 379, 3813jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
383278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
384258adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
385380zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
386385adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
387 elfzole1 11816 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
388387adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
389 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
390389adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
391383, 384, 386, 388, 390letrd 9750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
392391adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
393385adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
394329zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
395394adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
396254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
397 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
398397adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
399 elfzolt2 11817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
400399adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
401393, 396, 395, 398, 400lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
402393, 395, 401ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
403402adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
404382, 392, 403jca32 535 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
405404, 305sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
406405adantlll 717 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
407377, 406ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
408407adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
409 simp-4l 765 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
410271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
411 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
412411adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
413278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
414258adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
415412zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
416387adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
417 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
418417adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
419413, 414, 415, 416, 418letrd 9750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
420410, 412, 4193jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
421420, 326sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
422421adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
423422adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
424423adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
425329ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
426411zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
427426adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
428254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
429394adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
430 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
431430adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
432411adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
433249adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
434 zltlem1 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
435432, 433, 434syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
436431, 435mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
437399adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
438427, 428, 429, 436, 437lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
439438adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
440439adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
441440adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
442424, 425, 4413jca 1176 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
443442, 346sylibr 212 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^ ..^
444409, 443, 351syl2anc 661 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
445376, 408, 444monoord 12117 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
446238, 246, 445chvar 1982 . . . . . . . . . . . . . . . . . 18 ..^ ..^
447228, 237, 446chvar 1982 . . . . . . . . . . . . . . . . 17 ..^ ..^
448119, 121, 227, 447syl21anc 1227 . . . . . . . . . . . . . . . 16
449116, 121jca 532 . . . . . . . . . . . . . . . . 17 ..^
450119, 166syl 16 . . . . . . . . . . . . . . . . . . 19
451195simpld 459 . . . . . . . . . . . . . . . . . . . . 21
452191, 160, 155, 451, 178lelttrd 9751 . . . . . . . . . . . . . . . . . . . 20
453180simprd 463 . . . . . . . . . . . . . . . . . . . 20
454191, 155, 450, 452, 453ltletrd 9753 . . . . . . . . . . . . . . . . . . 19
455191, 450, 127, 454ltadd2dd 9752 . . . . . . . . . . . . . . . . . 18
456190oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20
457201a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
458116, 188, 23syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
459457, 458sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21
460200, 459pncan3d 9945 . . . . . . . . . . . . . . . . . . . 20
461456, 460eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19
46226a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
463 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25
464463oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24
465464adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
46622adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
467466, 165ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
46813adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
469467, 468resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
470462, 465, 165, 469fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . 22 ..^
471116, 118, 470syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
472471oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20
473119, 467syl 16 . . . . . . . . . . . . . . . . . . . . . 22
474473recnd 9634 . . . . . . . . . . . . . . . . . . . . 21
475200, 474pncan3d 9945 . . . . . . . . . . . . . . . . . . . 20
476472, 475eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19
477461, 476breq12d 4466 . . . . . . . . . . . . . . . . . 18
478455, 477mpbird 232 . . . . . . . . . . . . . . . . 17
479 nfv 1683 . . . . . . . . . . . . . . . . . 18 ..^ ..^
480 eleq1 2539 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
481480anbi2d 703 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^ ..^
482 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22
483482fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21
484483breq2d 4465 . . . . . . . . . . . . . . . . . . . 20
485481, 484anbi12d 710 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
486 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20
487486breq2d 4465 . . . . . . . . . . . . . . . . . . 19
488485, 487imbi12d 320 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^