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

Theorem stoweidlem34 27750
 Description: This lemma proves that for all in there is a as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem34.1
stoweidlem34.2
stoweidlem34.3
stoweidlem34.4
stoweidlem34.5
stoweidlem34.6
stoweidlem34.7
stoweidlem34.8
stoweidlem34.9
stoweidlem34.10
stoweidlem34.11
stoweidlem34.12
stoweidlem34.13
stoweidlem34.14
stoweidlem34.15
stoweidlem34.16
stoweidlem34.17
stoweidlem34.18
Assertion
Ref Expression
stoweidlem34
Distinct variable groups:   ,,,   ,   ,   ,,,   ,,,   ,   ,   ,,
Allowed substitution hints:   (,)   (,,)   (,)   (,)   (,)   ()

Proof of Theorem stoweidlem34
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem34.3 . 2
2 simpr 448 . . . . . . . 8
3 ovex 6098 . . . . . . . . 9
43rabex 4346 . . . . . . . 8
5 stoweidlem34.6 . . . . . . . . 9
65fvmpt2 5804 . . . . . . . 8
72, 4, 6sylancl 644 . . . . . . 7
8 ssrab2 3420 . . . . . . 7
97, 8syl6eqss 3390 . . . . . 6
10 elfznn 11072 . . . . . . 7
1110ssriv 3344 . . . . . 6
129, 11syl6ss 3352 . . . . 5
13 nnssre 9996 . . . . 5
1412, 13syl6ss 3352 . . . 4
15 stoweidlem34.7 . . . . . . . . . . . . . . . 16
1615adantr 452 . . . . . . . . . . . . . . 15
17 nnuz 10513 . . . . . . . . . . . . . . 15
1816, 17syl6eleq 2525 . . . . . . . . . . . . . 14
19 eluzfz2 11057 . . . . . . . . . . . . . 14
2018, 19syl 16 . . . . . . . . . . . . 13
21 stoweidlem34.11 . . . . . . . . . . . . . . . . 17
22 3re 10063 . . . . . . . . . . . . . . . . . . . . 21
23 3ne0 10077 . . . . . . . . . . . . . . . . . . . . 21
2422, 23rereccli 9771 . . . . . . . . . . . . . . . . . . . 20
2524a1i 11 . . . . . . . . . . . . . . . . . . 19
26 1re 9082 . . . . . . . . . . . . . . . . . . . 20
2726a1i 11 . . . . . . . . . . . . . . . . . . 19
2816nnred 10007 . . . . . . . . . . . . . . . . . . 19
29 1lt3 10136 . . . . . . . . . . . . . . . . . . . . 21
3022, 29pm3.2i 442 . . . . . . . . . . . . . . . . . . . 20
31 recgt1i 9899 . . . . . . . . . . . . . . . . . . . . 21
3231simprd 450 . . . . . . . . . . . . . . . . . . . 20
3330, 32mp1i 12 . . . . . . . . . . . . . . . . . . 19
3425, 27, 28, 33ltsub2dd 9631 . . . . . . . . . . . . . . . . . 18
3528, 27resubcld 9457 . . . . . . . . . . . . . . . . . . 19
3628, 25resubcld 9457 . . . . . . . . . . . . . . . . . . 19
37 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21
3837rpred 10640 . . . . . . . . . . . . . . . . . . . 20
3938adantr 452 . . . . . . . . . . . . . . . . . . 19
4037rpgt0d 10643 . . . . . . . . . . . . . . . . . . . 20
4140adantr 452 . . . . . . . . . . . . . . . . . . 19
42 ltmul1 9852 . . . . . . . . . . . . . . . . . . 19
4335, 36, 39, 41, 42syl112anc 1188 . . . . . . . . . . . . . . . . . 18
4434, 43mpbid 202 . . . . . . . . . . . . . . . . 17
4521, 44jca 519 . . . . . . . . . . . . . . . 16
46 stoweidlem34.9 . . . . . . . . . . . . . . . . . 18
4746fnvinran 27652 . . . . . . . . . . . . . . . . 17
4835, 39remulcld 9108 . . . . . . . . . . . . . . . . 17
4936, 39remulcld 9108 . . . . . . . . . . . . . . . . 17
50 lttr 9144 . . . . . . . . . . . . . . . . . 18
51 ltle 9155 . . . . . . . . . . . . . . . . . . 19
52513adant2 976 . . . . . . . . . . . . . . . . . 18
5350, 52syld 42 . . . . . . . . . . . . . . . . 17
5447, 48, 49, 53syl3anc 1184 . . . . . . . . . . . . . . . 16
5545, 54mpd 15 . . . . . . . . . . . . . . 15
56 rabid 2876 . . . . . . . . . . . . . . 15
572, 55, 56sylanbrc 646 . . . . . . . . . . . . . 14
58 nnnn0 10220 . . . . . . . . . . . . . . . . . 18
59 nn0uz 10512 . . . . . . . . . . . . . . . . . 18
6058, 59syl6eleq 2525 . . . . . . . . . . . . . . . . 17
61 eluzfz2 11057 . . . . . . . . . . . . . . . . 17
6215, 60, 613syl 19 . . . . . . . . . . . . . . . 16
63 stoweidlem34.8 . . . . . . . . . . . . . . . . 17
64 rabexg 4345 . . . . . . . . . . . . . . . . 17
6563, 64syl 16 . . . . . . . . . . . . . . . 16
66 oveq1 6080 . . . . . . . . . . . . . . . . . . . 20
6766oveq1d 6088 . . . . . . . . . . . . . . . . . . 19
6867breq2d 4216 . . . . . . . . . . . . . . . . . 18
6968rabbidv 2940 . . . . . . . . . . . . . . . . 17
70 stoweidlem34.4 . . . . . . . . . . . . . . . . 17
7169, 70fvmptg 5796 . . . . . . . . . . . . . . . 16
7262, 65, 71syl2anc 643 . . . . . . . . . . . . . . 15
7372adantr 452 . . . . . . . . . . . . . 14
7457, 73eleqtrrd 2512 . . . . . . . . . . . . 13
75 nfcv 2571 . . . . . . . . . . . . . 14
76 nfcv 2571 . . . . . . . . . . . . . 14
77 nfmpt1 4290 . . . . . . . . . . . . . . . . 17
7870, 77nfcxfr 2568 . . . . . . . . . . . . . . . 16
7978, 75nffv 5727 . . . . . . . . . . . . . . 15
8079nfcri 2565 . . . . . . . . . . . . . 14
81 fveq2 5720 . . . . . . . . . . . . . . 15
8281eleq2d 2502 . . . . . . . . . . . . . 14
8375, 76, 80, 82elrabf 3083 . . . . . . . . . . . . 13
8420, 74, 83sylanbrc 646 . . . . . . . . . . . 12
8584, 7eleqtrrd 2512 . . . . . . . . . . 11
86 ne0i 3626 . . . . . . . . . . 11
8785, 86syl 16 . . . . . . . . . 10
88 nnwo 10534 . . . . . . . . . . 11
89 nfcv 2571 . . . . . . . . . . . 12
90 nfcv 2571 . . . . . . . . . . . . . . 15
91 nfrab1 2880 . . . . . . . . . . . . . . 15
9290, 91nfmpt 4289 . . . . . . . . . . . . . 14
935, 92nfcxfr 2568 . . . . . . . . . . . . 13
94 nfcv 2571 . . . . . . . . . . . . 13
9593, 94nffv 5727 . . . . . . . . . . . 12
96 nfv 1629 . . . . . . . . . . . . 13
9795, 96nfral 2751 . . . . . . . . . . . 12
98 nfv 1629 . . . . . . . . . . . 12
99 breq1 4207 . . . . . . . . . . . . 13
10099ralbidv 2717 . . . . . . . . . . . 12
10189, 95, 97, 98, 100cbvrexf 2919 . . . . . . . . . . 11
10288, 101sylib 189 . . . . . . . . . 10
10312, 87, 102syl2anc 643 . . . . . . . . 9
104 stoweidlem34.2 . . . . . . . . . . 11
105 nfv 1629 . . . . . . . . . . 11
106104, 105nfan 1846 . . . . . . . . . 10
1077eleq2d 2502 . . . . . . . . . . . . . . . 16
108107biimpa 471 . . . . . . . . . . . . . . 15
109 rabid 2876 . . . . . . . . . . . . . . 15
110108, 109sylib 189 . . . . . . . . . . . . . 14
111110simprd 450 . . . . . . . . . . . . 13
112111adantr 452 . . . . . . . . . . . 12
113 simp3 959 . . . . . . . . . . . . . . . . . . . 20
114 simp1l 981 . . . . . . . . . . . . . . . . . . . . . . 23
115 noel 3624 . . . . . . . . . . . . . . . . . . . . . . . . . 26
116 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
117 1m1e0 10060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118116, 117syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
119118fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
12022a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
12123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
12227, 120, 121redivcld 9834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
123122renegcld 9456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
124123, 39remulcld 9108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
125 0re 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
126125a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
127 3pos 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
12822, 127recgt0ii 9908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
129 lt0neg2 9527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
13024, 129ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
131128, 130mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
132 ltmul1 9852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
133123, 126, 39, 41, 132syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
134131, 133mpbii 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
135 mul02lem2 9235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
13639, 135syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
137134, 136breqtrd 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
138 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
139124, 126, 47, 137, 138ltletrd 9222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
140124, 47ltnled 9212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
141139, 140mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
142 nan 564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
143141, 142mpbir 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
144 rabid 2876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
145143, 144sylnibr 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
14615nnnn0d 10266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
147 elnn0uz 10515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
148146, 147sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
149 eluzfz1 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151 rabexg 4345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
15263, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
154 df-neg 9286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
155153, 154syl6eqr 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
156155oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
157156breq2d 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
158157rabbidv 2940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159158, 70fvmptg 5796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160150, 152, 159syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
161145, 160neleqtrrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1621, 161alrimi 1781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
163 eq0 3634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
164 nfcv 2571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
165 nfrab1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
166164, 165nfmpt 4289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
16770, 166nfcxfr 2568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
168 nfcv 2571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
169167, 168nffv 5727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
170169nfcri 2565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
171170nfn 1811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
172 nfv 1629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
173 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
174173notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
175171, 172, 174cbval 1982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
176163, 175bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
177162, 176sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
178119, 177sylan9eqr 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
179178eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . 26
180115, 179mtbiri 295 . . . . . . . . . . . . . . . . . . . . . . . . 25
181180ex 424 . . . . . . . . . . . . . . . . . . . . . . . 24
182181con2d 109 . . . . . . . . . . . . . . . . . . . . . . 23
183114, 113, 182sylc 58 . . . . . . . . . . . . . . . . . . . . . 22
184 simplll 735 . . . . . . . . . . . . . . . . . . . . . . . . 25
185107, 109syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
186185simprbda 607 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
18715, 17syl6eleq 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
188187adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
189 elfzp12 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
190188, 189syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
191190adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
192186, 191mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26
193192orcanai 880 . . . . . . . . . . . . . . . . . . . . . . . . 25
194 fzssp1 11087 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
19515nncnd 10008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
196 ax-1cn 9040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
197196a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
198195, 197npcand 9407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
199198oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200194, 199syl5sseq 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
201200adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
202 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
203 1z 10303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
204 zaddcl 10309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
205203, 203, 204mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
206205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
20715nnzd 10366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
208207adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
209 elfzelz 11051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
210209adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
211203a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
212 fzsubel 11080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
213206, 208, 210, 211, 212syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
214202, 213mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
215 pncan 9303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216196, 196, 215mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
217216oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
218214, 217syl6eleq 2525 . . . . . . . . . . . . . . . . . . . . . . . . . 26
219201, 218sseldd 3341 . . . . . . . . . . . . . . . . . . . . . . . . 25
220184, 193, 219syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24
221220ex 424 . . . . . . . . . . . . . . . . . . . . . . 23
2222213adant3 977 . . . . . . . . . . . . . . . . . . . . . 22
223183, 222mpd 15 . . . . . . . . . . . . . . . . . . . . 21
224 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . 23
225224eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . 22
226225elrab3 3085 . . . . . . . . . . . . . . . . . . . . 21
227223, 226syl 16 . . . . . . . . . . . . . . . . . . . 20
228113, 227mpbird 224 . . . . . . . . . . . . . . . . . . 19
229 nfcv 2571 . . . . . . . . . . . . . . . . . . . 20
230 nfv 1629 . . . . . . . . . . . . . . . . . . . 20
231 nfcv 2571 . . . . . . . . . . . . . . . . . . . . . 22
23278, 231nffv 5727 . . . . . . . . . . . . . . . . . . . . 21
233232nfcri 2565 . . . . . . . . . . . . . . . . . . . 20
234 fveq2 5720 . . . . . . . . . . . . . . . . . . . . 21
235234eleq2d 2502 . . . . . . . . . . . . . . . . . . . 20
23676, 229, 230, 233, 235cbvrab 2946 . . . . . . . . . . . . . . . . . . 19
237228, 236syl6eleqr 2526 . . . . . . . . . . . . . . . . . 18
23873ad2ant1 978 . . . . . . . . . . . . . . . . . 18
239237, 238eleqtrrd 2512 . . . . . . . . . . . . . . . . 17
240 elfzelz 11051 . . . . . . . . . . . . . . . . . . . . 21
241 zre 10278 . . . . . . . . . . . . . . . . . . . . 21
242186, 240, 2413syl 19 . . . . . . . . . . . . . . . . . . . 20
2432423adant3 977 . . . . . . . . . . . . . . . . . . 19
244 peano2rem 9359 . . . . . . . . . . . . . . . . . . 19
245243, 244ex-natded5.3i 21709 . . . . . . . . . . . . . . . . . 18
246 ltm1 9842 . . . . . . . . . . . . . . . . . . . 20
247246adantr 452 . . . . . . . . . . . . . . . . . . 19
248 ltnle 9147 . . . . . . . . . . . . . . . . . . . 20
249248ancoms 440 . . . . . . . . . . . . . . . . . . 19
250247, 249mpbid 202 . . . . . . . . . . . . . . . . . 18
251245, 250syl 16 . . . . . . . . . . . . . . . . 17
252 breq2 4208 . . . . . . . . . . . . . . . . . . 19
253252notbid 286 . . . . . . . . . . . . . . . . . 18
254253rspcev 3044 . . . . . . . . . . . . . . . . 17
255239, 251, 254syl2anc 643 . . . . . . . . . . . . . . . 16
256 rexnal 2708 . . . . . . . . . . . . . . . 16
257255, 256sylib 189 . . . . . . . . . . . . . . 15
2582573expia 1155 . . . . . . . . . . . . . 14
259258con2d 109 . . . . . . . . . . . . 13
260259imp 419 . . . . . . . . . . . 12
261112, 260eldifd 3323 . . . . . . . . . . 11
262261exp31 588 . . . . . . . . . 10
263106, 262reximdai 2806 . . . . . . . . 9
264103, 263mpd 15 . . . . . . . 8
265 df-rex 2703 . . . . . . . 8
266264, 265sylib 189 . . . . . . 7
267 simprl 733 . . . . . . . . . 10
268 eldifn 3462 . . . . . . . . . . . . 13
269 simplr 732 . . . . . . . . . . . . . 14
270 simpll 731 . . . . . . . . . . . . . . . . 17
271186adantrr 698 . . . . . . . . . . . . . . . . 17
272 simprr 734 . . . . . . . . . . . . . . . . 17
273 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
274273oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . 26
275274breq2d 4216 . . . . . . . . . . . . . . . . . . . . . . . . 25
276275rabbidv 2940 . . . . . . . . . . . . . . . . . . . . . . . 24
277276cbvmptv 4292 . . . . . . . . . . . . . . . . . . . . . . 23
27870, 277eqtri 2455 . . . . . . . . . . . . . . . . . . . . . 22
279278a1i 11 . . . . . . . . . . . . . . . . . . . . 21
280 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . 25
281280oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . 24
282281breq2d 4216 . . . . . . . . . . . . . . . . . . . . . . 23
283282rabbidv 2940 . . . . . . . . . . . . . . . . . . . . . 22
284283adantl 453 . . . . . . . . . . . . . . . . . . . . 21
285 fzssp1 11087 . . . . . . . . . . . . . . . . . . . . . . . 24
286198oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . 24
287285, 286syl5sseq 3388 . . . . . . . . . . . . . . . . . . . . . . 23
288287adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
289 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24
290203a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
291207adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
292240adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25
293 fzsubel 11080 . . . . . . . . . . . . . . . . . . . . . . . . 25
294290, 291, 292, 290, 293syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24
295289, 294mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23
296117a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
297296oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . 23
298295, 297eleqtrd 2511 . . . . . . . . . . . . . . . . . . . . . 22
299288, 298sseldd 3341 . . . . . . . . . . . . . . . . . . . . 21
30063adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
301 rabexg 4345 . . . . . . . . . . . . . . . . . . . . . 22
302300, 301syl 16 . . . . . . . . . . . . . . . . . . . . 21
303279, 284, 299, 302fvmptd 5802 . . . . . . . . . . . . . . . . . . . 20
304303eleq2d 2502 . . . . . . . . . . . . . . . . . . 19
305304notbid 286 . . . . . . . . . . . . . . . . . 18
306305biimpa 471 . . . . . . . . . . . . . . . . 17
307270, 271, 272, 306syl21anc 1183 . . . . . . . . . . . . . . . 16
308 rabid 2876 . . . . . . . . . . . . . . . . 17
309242adantrr 698 . . . . . . . . . . . . . . . . . . . 20
310 recn 9072 . . . . . . . . . . . . . . . . . . . . . . 23
311196a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
31226, 22, 233pm3.2i 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25
313 redivcl 9725 . . . . . . . . . . . . . . . . . . . . . . . . 25
314 recn 9072 . . . . . . . . . . . . . . . . . . . . . . . . 25
315312, 313, 314mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24
316315a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
317310, 311, 316subsub4d 9434 . . . . . . . . . . . . . . . . . . . . . 22
318 3cn 10064 . . . . . . . . . . . . . . . . . . . . . . . . . 26
319318, 196, 318, 23divdiri 9763 . . . . . . . . . . . . . . . . . . . . . . . . 25
320 3p1e4 10096 . . . . . . . . . . . . . . . . . . . . . . . . . 26
321320oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25
322318, 23dividi 9739 . . . . . . . . . . . . . . . . . . . . . . . . . 26
323322oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25
324319, 321, 3233eqtr3i 2463 . . . . . . . . . . . . . . . . . . . . . . . 24
325324a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
326325oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22
327317, 326eqtr4d 2470 . . . . . . . . . . . . . . . . . . . . 21
328327oveq1d 6088 . . . . . . . . . . . . . . . . . . . 20
329309, 328syl 16 . . . . . . . . . . . . . . . . . . 19
330329breq2d 4216 . . . . . . . . . . . . . . . . . 18
331330anbi2d 685 . . . . . . . . . . . . . . . . 17
332308, 331syl5bb 249 . . . . . . . . . . . . . . . 16
333307, 332mtbid 292 . . . . . . . . . . . . . . 15
334 imnan 412 . . . . . . . . . . . . . . 15
335333, 334sylibr 204 . . . . . . . . . . . . . 14
336269, 335mpd 15 . . . . . . . . . . . . 13
337268, 336sylanr2 635 . . . . . . . . . . . 12
338242adantrr 698 . . . . . . . . . . . . . . 15
339 4re 10065 . . . . . . . . . . . . . . . . 17
340339a1i 11 . . . . . . . . . . . . . . . 16
34122a1i 11 . . . . . . . . . . . . . . . 16
34223a1i 11 . . . . . . . . . . . . . . . 16
343340, 341, 342redivcld 9834 . . . . . . . . . . . . . . 15
344338, 343resubcld 9457 . . . . . . . . . . . . . 14
34538ad2antrr 707 . . . . . . . . . . . . . 14
346 remulcl 9067 . . . . . . . . . . . . . . 15
347346rexrd 9126 . . . . . . . . . . . . . 14
348344, 345, 347syl2anc 643 . . . . . . . . . . . . 13
34947rexrd 9126 . . . . . . . . . . . . . 14
350349adantr 452 . . . . . . . . . . . . 13
351 xrltnle 9136 . . . . . . . . . . . . 13
352348, 350, 351syl2anc 643 . . . . . . . . . . . 12
353337, 352mpbird 224 . . . . . . . . . . 11
354 simpl 444 . . . . . . . . . . . 12
355 simprr 734 . . . . . . . . . . . . 13
356355eldifad 3324 . . . . . . . . . . . 12
357 simplll 735 . . . . . . . . . . . . . . 15
358186adantr 452 . . . . . . . . . . . . . . 15
359 simpr 448 . . . . . . . . . . . . . . 15
360 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . 22
361360oveq1d 6088 . . . . . . . . . . . . . . . . . . . . 21
362361breq2d 4216 . . . . . . . . . . . . . . . . . . . 20
363362rabbidv 2940 . . . . . . . . . . . . . . . . . . 19
364363adantl 453 . . . . . . . . . . . . . . . . . 18
365 0p1e1 10085 . . . . . . . . . . . . . . . . . . . . . 22
366365oveq1i 6083 . . . . . . . . . . . . . . . . . . . . 21
367 0z 10285 . . . . . . . . . . . . . . . . . . . . . 22
368 fzp1ss 11090 . . . . . . . . . . . . . . . . . . . . . 22
369367, 368ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21
370366, 369eqsstr3i 3371 . . . . . . . . . . . . . . . . . . . 20
371370sseli 3336 . . . . . . . . . . . . . . . . . . 19
372371adantl 453 . . . . . . . . . . . . . . . . . 18
373 rabexg 4345 . . . . . . . . . . . . . . . . . . 19
374300, 373syl 16 . . . . . . . . . . . . . . . . . 18
375279, 364, 372, 374fvmptd 5802 . . . . . . . . . . . . . . . . 17
376375eleq2d 2502 . . . . . . . . . . . . . . . 16
377376biimpa 471 . . . . . . . . . . . . . . 15
378357, 358, 359, 377syl21anc 1183 . . . . . . . . . . . . . 14
379 rabid 2876 . . . . . . . . . . . . . 14
380378, 379sylib 189 . . . . . . . . . . . . 13
381380simprd 450 . . . . . . . . . . . 12
382354, 267, 356, 381syl21anc 1183 . . . . . . . . . . 11
383353, 382jca 519 . . . . . . . . . 10
38415ad2antrr 707 . . . . . . . . . . . 12
385 simplr 732 . . . . . . . . . . . 12
386186adantrr 698 . . . . . . . . . . . 12
387 simplll 735 . . . . . . . . . . . . 13
388 nfv 1629 . . . . . . . . . . . . . . . 16
389104, 388nfan 1846 . . . . . . . . . . . . . . 15
390 nfv 1629 . . . . . . . . . . . . . . 15
391389, 390nfim 1832 . . . . . . . . . . . . . 14
392 eleq1 2495 . . . . . . . . . . . . . . . 16
393392anbi2d 685 . . . . . . . . . . . . . . 15
394 fveq2 5720 . . . . . . . . . . . . . . . 16
395394feq1d 5572 . . . . . . . . . . . . . . 15
396393, 395imbi12d 312 . . . . . . . . . . . . . 14
397 stoweidlem34.14 . . . . . . . . . . . . . 14
398391, 396, 397chvar 1968 . . . . . . . . . . . . 13
399387, 398sylancom 649 . . . . . . . . . . . 12
400 simpr 448 . . . . . . . . . . . . 13
401 simpllr 736 . . . . . . . . . . . . 13
402104, 388, 105nf3an 1849 . . . . . . . . . . . . . . 15
403 nfv 1629 . . . . . . . . . . . . . . 15
404402, 403nfim 1832 . . . . . . . . . . . . . 14
4053923anbi2d 1259 . . . . . . . . . . . . . . 15
406394fveq1d 5722 . . . . . . . . . . . . . . . 16
407406breq1d 4214 . . . . . . . . . . . . . . 15
408405, 407imbi12d 312 . . . . . . . . . . . . . 14
409 stoweidlem34.16 . . . . . . . . . . . . . 14
410404, 408, 409chvar 1968 . . . . . . . . . . . . 13
411387, 400, 401, 410syl3anc 1184 . . . . . . . . . . . 12
412 simplll 735 . . . . . . . . . . . . 13
413367a1i 11 . . . . . . . . . . . . . . . 16
414 elfzel2 11049 . . . . . . . . . . . . . . . . 17
415414adantl 453 . . . . . . . . . . . . . . . 16
416 elfzelz 11051 . . . . . . . . . . . . . . . . 17
417416adantl 453 . . . . . . . . . . . . . . . 16
418413, 415, 4173jca 1134 . . . . . . . . . . . . . . 15
419125a1i 11 . . . . . . . . . . . . . . . . 17
420 elfzel1 11050 . . . . . . . . . . . . . . . . . . 19
421420zred 10367 . . . . . . . . . . . . . . . . . 18
422421adantl 453 . . . . . . . . . . . . . . . . 17
423416zred 10367 . . . . . . . . . . . . . . . . . 18
424423adantl 453 . . . . . . . . . . . . . . . . 17
425125a1i 11 . . . . . . . . . . . . . . . . . . 19
42626a1i 11 . . . . . . . . . . . . . . . . . . 19
427 0le1 9543 . . . . . . . . . . . . . . . . . . . 20
428427a1i 11 . . . . . . . . . . . . . . . . . . 19
429 elfzle1 11052 . . . . . . . . . . . . . . . . . . . 20
430186, 429syl 16 . . . . . . . . . . . . . . . . . . 19
431425, 426, 242, 428, 430letrd 9219 . . . . . . . . . . . . . . . . . 18
432431adantr 452 . . . . . . . . . . . . . . . . 17
433 elfzle1 11052 . . . . . . . . . . . . . . . . . 18
434433adantl 453 . . . . . . . . . . . . . . . . 17
435419, 422, 424, 432, 434letrd 9219 . . . . . . . . . . . . . . . 16
436 elfzle2 11053 . . . . . . . . . . . . . . . . 17
437436adantl 453 . . . . . . . . . . . . . . . 16
438435, 437jca 519 . . . . . . . . . . . . . . 15
439 elfz2 11042 . . . . . . . . . . . . . . 15
440418, 438, 439sylanbrc 646 . . . . . . . . . . . . . 14
441440adantlrr 702 . . . . . . . . . . . . 13
442 simpll 731 . . . . . . . . . . . . . 14
443 simplrl 737 . . . . . . . . . . . . . 14
444 simplrr 738 . . . . . . . . . . . . . . 15
445444eldifad 3324 . . . . . . . . . . . . . 14
446 simpr 448 . . . . . . . . . . . . . 14
447 simpl1 960 . . . . . . . . . . . . . . . . 17
448447simprd 450 . . . . . . . . . . . . . . . 16
449447, 47syl 16 . . . . . . . . . . . . . . . . 17
450421adantl 453 . . . . . . . . . . . . . . . . . . 19
45124a1i 11 . . . . . . . . . . . . . . . . . . 19
452450, 451resubcld 9457 . . . . . . . . . . . . . . . . . 18
453 simpl1l 1008 . . . . . . . . . . . . . . . . . . 19
454453, 38syl 16 . . . . . . . . . . . . . . . . . 18
455452, 454remulcld 9108 . . . . . . . . . . . . . . . . 17
456423adantl 453 . . . . . . . . . . . . . . . . . . . 20
45724a1i 11 . . . . . . . . . . . . . . . . . . . 20
458456, 457resubcld 9457 . . . . . . . . . . . . . . . . . . 19
45938adantr 452 . . . . . . . . . . . . . . . . . . 19
460458, 459remulcld 9108 . . . . . . . . . . . . . . . . . 18
461453, 460sylancom 649 . . . . . . . . . . . . . . . . 17
462 simpl3 962 . . . . . . . . . . . . . . . . . . . 20
463 simpl2 961 . . . . . . . . . . . . . . . . . . . . . 22
464447, 463, 186syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
465453, 464, 375syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
466462, 465eleqtrd 2511 . . . . . . . . . . . . . . . . . . 19