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

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

Proof of Theorem stoweidlem60
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnre 10638 . . . . . . . . . . . . 13
21adantl 473 . . . . . . . . . . . 12
3 stoweidlem60.17 . . . . . . . . . . . . . 14
43rpred 11364 . . . . . . . . . . . . 13
54adantr 472 . . . . . . . . . . . 12
63rpne0d 11369 . . . . . . . . . . . . 13
76adantr 472 . . . . . . . . . . . 12
82, 5, 7redivcld 10457 . . . . . . . . . . 11
9 1red 9676 . . . . . . . . . . 11
108, 9readdcld 9688 . . . . . . . . . 10
1110adantr 472 . . . . . . . . 9
12 arch 10890 . . . . . . . . 9
1311, 12syl 17 . . . . . . . 8
14 stoweidlem60.2 . . . . . . . . . . . . . . 15
15 nfv 1769 . . . . . . . . . . . . . . 15
1614, 15nfan 2031 . . . . . . . . . . . . . 14
17 nfra1 2785 . . . . . . . . . . . . . 14
1816, 17nfan 2031 . . . . . . . . . . . . 13
19 nfv 1769 . . . . . . . . . . . . 13
2018, 19nfan 2031 . . . . . . . . . . . 12
21 nfv 1769 . . . . . . . . . . . 12
2220, 21nfan 2031 . . . . . . . . . . 11
23 simp-5l 786 . . . . . . . . . . . . . 14
24 stoweidlem60.3 . . . . . . . . . . . . . . . 16
25 stoweidlem60.4 . . . . . . . . . . . . . . . 16
26 stoweidlem60.5 . . . . . . . . . . . . . . . 16
27 stoweidlem60.15 . . . . . . . . . . . . . . . 16
2824, 25, 26, 27fcnre 37409 . . . . . . . . . . . . . . 15
2928fnvinran 37398 . . . . . . . . . . . . . 14
3023, 29sylancom 680 . . . . . . . . . . . . 13
31 simp-5r 787 . . . . . . . . . . . . . 14
3231nnred 10646 . . . . . . . . . . . . 13
33 simpllr 777 . . . . . . . . . . . . . . . 16
3433nnred 10646 . . . . . . . . . . . . . . 15
35 1red 9676 . . . . . . . . . . . . . . 15
3634, 35resubcld 10068 . . . . . . . . . . . . . 14
3723, 4syl 17 . . . . . . . . . . . . . 14
3836, 37remulcld 9689 . . . . . . . . . . . . 13
39 simpllr 777 . . . . . . . . . . . . . 14
4039r19.21bi 2776 . . . . . . . . . . . . 13
41 simplr 770 . . . . . . . . . . . . . 14
42 simpr 468 . . . . . . . . . . . . . . . 16
43 simpl1 1033 . . . . . . . . . . . . . . . . . 18
44 simpl2 1034 . . . . . . . . . . . . . . . . . 18
4543, 44, 8syl2anc 673 . . . . . . . . . . . . . . . . 17
46 1red 9676 . . . . . . . . . . . . . . . . 17
47 simpl3 1035 . . . . . . . . . . . . . . . . . 18
4847nnred 10646 . . . . . . . . . . . . . . . . 17
4945, 46, 48ltaddsubd 10234 . . . . . . . . . . . . . . . 16
5042, 49mpbid 215 . . . . . . . . . . . . . . 15
5113ad2ant2 1052 . . . . . . . . . . . . . . . . 17
5251adantr 472 . . . . . . . . . . . . . . . 16
5348, 46resubcld 10068 . . . . . . . . . . . . . . . 16
5443ad2ant1 1051 . . . . . . . . . . . . . . . . 17
5554adantr 472 . . . . . . . . . . . . . . . 16
563rpgt0d 11367 . . . . . . . . . . . . . . . . 17
5743, 56syl 17 . . . . . . . . . . . . . . . 16
58 ltdivmul2 10504 . . . . . . . . . . . . . . . 16
5952, 53, 55, 57, 58syl112anc 1296 . . . . . . . . . . . . . . 15
6050, 59mpbid 215 . . . . . . . . . . . . . 14
6123, 31, 33, 41, 60syl31anc 1295 . . . . . . . . . . . . 13
6230, 32, 38, 40, 61lttrd 9813 . . . . . . . . . . . 12
6362ex 441 . . . . . . . . . . 11
6422, 63ralrimi 2800 . . . . . . . . . 10
6564ex 441 . . . . . . . . 9
6665reximdva 2858 . . . . . . . 8
6713, 66mpd 15 . . . . . . 7
68 stoweidlem60.1 . . . . . . . 8
69 stoweidlem60.8 . . . . . . . 8
70 stoweidlem60.9 . . . . . . . 8
7168, 14, 24, 69, 25, 70, 26, 27rfcnnnub 37420 . . . . . . 7
7267, 71r19.29a 2918 . . . . . 6
73 df-rex 2762 . . . . . 6
7472, 73sylib 201 . . . . 5
75 simpr 468 . . . . . . . . 9
7614, 19nfan 2031 . . . . . . . . . . 11
77 stoweidlem60.6 . . . . . . . . . . 11
78 stoweidlem60.7 . . . . . . . . . . 11
79 eqid 2471 . . . . . . . . . . 11
80 eqid 2471 . . . . . . . . . . 11
8169adantr 472 . . . . . . . . . . 11
82 stoweidlem60.10 . . . . . . . . . . . 12
8382adantr 472 . . . . . . . . . . 11
84 stoweidlem60.11 . . . . . . . . . . . 12
85843adant1r 1285 . . . . . . . . . . 11
86 stoweidlem60.12 . . . . . . . . . . . 12
87863adant1r 1285 . . . . . . . . . . 11
88 stoweidlem60.13 . . . . . . . . . . . 12
8988adantlr 729 . . . . . . . . . . 11
90 stoweidlem60.14 . . . . . . . . . . . 12
9190adantlr 729 . . . . . . . . . . 11
9227adantr 472 . . . . . . . . . . 11
933adantr 472 . . . . . . . . . . 11
94 stoweidlem60.18 . . . . . . . . . . . 12
9594adantr 472 . . . . . . . . . . 11
96 simpr 468 . . . . . . . . . . 11
9768, 76, 24, 25, 26, 77, 78, 79, 80, 81, 83, 85, 87, 89, 91, 92, 93, 95, 96stoweidlem59 38032 . . . . . . . . . 10
9897adantrr 731 . . . . . . . . 9
99 19.42v 1842 . . . . . . . . 9
10075, 98, 99sylanbrc 677 . . . . . . . 8
101 3anass 1011 . . . . . . . . 9
102101exbii 1726 . . . . . . . 8
103100, 102sylibr 217 . . . . . . 7
104103ex 441 . . . . . 6
105104eximdv 1772 . . . . 5
10674, 105mpd 15 . . . 4
107 simpl 464 . . . . . . . 8
108 simpr1l 1087 . . . . . . . 8
109 simpr2 1037 . . . . . . . 8
110 nfv 1769 . . . . . . . . . 10
11114, 19, 110nf3an 2033 . . . . . . . . 9
112 simp2 1031 . . . . . . . . 9
113 simp3 1032 . . . . . . . . 9
114 simp1 1030 . . . . . . . . . 10
115114, 84syl3an1 1325 . . . . . . . . 9
116114, 86syl3an1 1325 . . . . . . . . 9
117883ad2antl1 1192 . . . . . . . . 9
11833ad2ant1 1051 . . . . . . . . . 10
119118rpred 11364 . . . . . . . . 9
12082sselda 3418 . . . . . . . . . . 11
12124, 25, 26, 120fcnre 37409 . . . . . . . . . 10
1221213ad2antl1 1192 . . . . . . . . 9
123111, 112, 113, 115, 116, 117, 119, 122stoweidlem17 37989 . . . . . . . 8
124107, 108, 109, 123syl3anc 1292 . . . . . . 7
125 nfv 1769 . . . . . . . . 9
126 nfv 1769 . . . . . . . . . 10
127 nfv 1769 . . . . . . . . . 10
128 nfra1 2785 . . . . . . . . . 10
129126, 127, 128nf3an 2033 . . . . . . . . 9
130125, 129nfan 2031 . . . . . . . 8
131 nfra1 2785 . . . . . . . . . . 11
13219, 131nfan 2031 . . . . . . . . . 10
133 nfcv 2612 . . . . . . . . . . 11
134 nfra1 2785 . . . . . . . . . . . 12
135 nfra1 2785 . . . . . . . . . . . 12
136 nfra1 2785 . . . . . . . . . . . 12
137134, 135, 136nf3an 2033 . . . . . . . . . . 11
138133, 137nfral 2789 . . . . . . . . . 10
139132, 110, 138nf3an 2033 . . . . . . . . 9
14014, 139nfan 2031 . . . . . . . 8
141 eqid 2471 . . . . . . . 8
142 uniexg 6607 . . . . . . . . . . 11
14369, 142syl 17 . . . . . . . . . 10
14425, 143syl5eqel 2553 . . . . . . . . 9
145144adantr 472 . . . . . . . 8
14628adantr 472 . . . . . . . 8
147 stoweidlem60.16 . . . . . . . . . 10
148147r19.21bi 2776 . . . . . . . . 9
149148adantlr 729 . . . . . . . 8
150 simpr1r 1088 . . . . . . . . 9
151150r19.21bi 2776 . . . . . . . 8
1523adantr 472 . . . . . . . 8
15394adantr 472 . . . . . . . 8
154 simpll 768 . . . . . . . . 9
155 simplr2 1073 . . . . . . . . 9
156 simpr 468 . . . . . . . . 9
157 simp1 1030 . . . . . . . . . 10
158 ffvelrn 6035 . . . . . . . . . . 11
1591583adant1 1048 . . . . . . . . . 10
16082sselda 3418 . . . . . . . . . . 11
16124, 25, 26, 160fcnre 37409 . . . . . . . . . 10
162157, 159, 161syl2anc 673 . . . . . . . . 9
163154, 155, 156, 162syl3anc 1292 . . . . . . . 8
164 simp1r3 1128 . . . . . . . . . 10
165 r19.26-3 2906 . . . . . . . . . . 11
166165simp1bi 1045 . . . . . . . . . 10
167 simpl 464 . . . . . . . . . . . 12
168167ralimi 2796 . . . . . . . . . . 11
169168ralimi 2796 . . . . . . . . . 10
170164, 166, 1693syl 18 . . . . . . . . 9
171 simp2 1031 . . . . . . . . 9
172 simp3 1032 . . . . . . . . 9
173 rspa 2774 . . . . . . . . . 10
174173r19.21bi 2776 . . . . . . . . 9
175170, 171, 172, 174syl21anc 1291 . . . . . . . 8
176 simpr 468 . . . . . . . . . . . 12
177176ralimi 2796 . . . . . . . . . . 11
178177ralimi 2796 . . . . . . . . . 10
179164, 166, 1783syl 18 . . . . . . . . 9
180 rspa 2774 . . . . . . . . . 10
181180r19.21bi 2776 . . . . . . . . 9
182179, 171, 172, 181syl21anc 1291 . . . . . . . 8
183 simp1r3 1128 . . . . . . . . . 10
184165simp2bi 1046 . . . . . . . . . 10
185183, 184syl 17 . . . . . . . . 9
186 simp2 1031 . . . . . . . . 9
187 simp3 1032 . . . . . . . . 9
188 rspa 2774 . . . . . . . . . 10
189188r19.21bi 2776 . . . . . . . . 9
190185, 186, 187, 189syl21anc 1291 . . . . . . . 8
191 simp1r3 1128 . . . . . . . . . 10
192165simp3bi 1047 . . . . . . . . . 10
193191, 192syl 17 . . . . . . . . 9
194 simp2 1031 . . . . . . . . 9
195 simp3 1032 . . . . . . . . 9
196 rspa 2774 . . . . . . . . . 10
197196r19.21bi 2776 . . . . . . . . 9
198193, 194, 195, 197syl21anc 1291 . . . . . . . 8
19968, 130, 140, 77, 78, 141, 108, 145, 146, 149, 151, 152, 153, 163, 175, 182, 190, 198stoweidlem34 38007 . . . . . . 7
200 nfmpt1 4485 . . . . . . . . . 10
201200nfeq2 2627 . . . . . . . . 9
202 fveq1 5878 . . . . . . . . . . . . 13
203202breq1d 4405 . . . . . . . . . . . 12
204202breq2d 4407 . . . . . . . . . . . 12
205203, 204anbi12d 725 . . . . . . . . . . 11
206205anbi2d 718 . . . . . . . . . 10
207206rexbidv 2892 . . . . . . . . 9
208201, 207ralbid 2826 . . . . . . . 8
209208rspcev 3136 . . . . . . 7
210124, 199, 209syl2anc 673 . . . . . 6
211210ex 441 . . . . 5
2122112eximdv 1774 . . . 4
213106, 212mpd 15 . . 3
214 idd 24 . . . 4
215214exlimdv 1787 . . 3