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

Theorem stoweidlem60 27776
 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 stoweidlem60.1 . . . . . . . 8
2 stoweidlem60.2 . . . . . . . 8
3 stoweidlem60.3 . . . . . . . 8
4 stoweidlem60.8 . . . . . . . 8
5 stoweidlem60.4 . . . . . . . 8
6 stoweidlem60.9 . . . . . . . 8
7 stoweidlem60.5 . . . . . . . 8
8 stoweidlem60.15 . . . . . . . 8
91, 2, 3, 4, 5, 6, 7, 8rfcnnnub 27674 . . . . . . 7
10 nnre 9999 . . . . . . . . . . . . . . 15
1110adantl 453 . . . . . . . . . . . . . 14
12 stoweidlem60.17 . . . . . . . . . . . . . . . 16
1312rpred 10640 . . . . . . . . . . . . . . 15
1413adantr 452 . . . . . . . . . . . . . 14
1512rpne0d 10645 . . . . . . . . . . . . . . 15
1615adantr 452 . . . . . . . . . . . . . 14
1711, 14, 16redivcld 9834 . . . . . . . . . . . . 13
18 1re 9082 . . . . . . . . . . . . . 14
1918a1i 11 . . . . . . . . . . . . 13
2017, 19readdcld 9107 . . . . . . . . . . . 12
2120adantr 452 . . . . . . . . . . 11
22 arch 10210 . . . . . . . . . . 11
2321, 22syl 16 . . . . . . . . . 10
24 nfv 1629 . . . . . . . . . . . . . . . . 17
252, 24nfan 1846 . . . . . . . . . . . . . . . 16
26 nfra1 2748 . . . . . . . . . . . . . . . 16
2725, 26nfan 1846 . . . . . . . . . . . . . . 15
28 nfv 1629 . . . . . . . . . . . . . . 15
2927, 28nfan 1846 . . . . . . . . . . . . . 14
30 nfv 1629 . . . . . . . . . . . . . 14
3129, 30nfan 1846 . . . . . . . . . . . . 13
32 simp-5l 745 . . . . . . . . . . . . . . . 16
333, 5, 7, 8fcnre 27663 . . . . . . . . . . . . . . . . 17
3433fnvinran 27652 . . . . . . . . . . . . . . . 16
3532, 34sylancom 649 . . . . . . . . . . . . . . 15
36 simp-5r 746 . . . . . . . . . . . . . . . 16
3736nnred 10007 . . . . . . . . . . . . . . 15
38 simpllr 736 . . . . . . . . . . . . . . . . . 18
3938nnred 10007 . . . . . . . . . . . . . . . . 17
4018a1i 11 . . . . . . . . . . . . . . . . 17
4139, 40resubcld 9457 . . . . . . . . . . . . . . . 16
4232, 13syl 16 . . . . . . . . . . . . . . . 16
4341, 42remulcld 9108 . . . . . . . . . . . . . . 15
44 simpllr 736 . . . . . . . . . . . . . . . 16
4544r19.21bi 2796 . . . . . . . . . . . . . . 15
46 simplr 732 . . . . . . . . . . . . . . . 16
47 simpr 448 . . . . . . . . . . . . . . . . . 18
48 simpl1 960 . . . . . . . . . . . . . . . . . . . 20
49 simpl2 961 . . . . . . . . . . . . . . . . . . . 20
5048, 49, 17syl2anc 643 . . . . . . . . . . . . . . . . . . 19
5118a1i 11 . . . . . . . . . . . . . . . . . . 19
52 simpl3 962 . . . . . . . . . . . . . . . . . . . 20
5352nnred 10007 . . . . . . . . . . . . . . . . . . 19
5450, 51, 53ltaddsubd 9618 . . . . . . . . . . . . . . . . . 18
5547, 54mpbid 202 . . . . . . . . . . . . . . . . 17
56103ad2ant2 979 . . . . . . . . . . . . . . . . . . 19
5756adantr 452 . . . . . . . . . . . . . . . . . 18
5853, 51resubcld 9457 . . . . . . . . . . . . . . . . . 18
59133ad2ant1 978 . . . . . . . . . . . . . . . . . . 19
6059adantr 452 . . . . . . . . . . . . . . . . . 18
6112rpgt0d 10643 . . . . . . . . . . . . . . . . . . 19
6248, 61syl 16 . . . . . . . . . . . . . . . . . 18
63 ltdivmul2 9877 . . . . . . . . . . . . . . . . . 18
6457, 58, 60, 62, 63syl112anc 1188 . . . . . . . . . . . . . . . . 17
6555, 64mpbid 202 . . . . . . . . . . . . . . . 16
6632, 36, 38, 46, 65syl31anc 1187 . . . . . . . . . . . . . . 15
6735, 37, 43, 45, 66lttrd 9223 . . . . . . . . . . . . . 14
6867ex 424 . . . . . . . . . . . . 13
6931, 68ralrimi 2779 . . . . . . . . . . . 12
7069ex 424 . . . . . . . . . . 11
7170reximdva 2810 . . . . . . . . . 10
7223, 71mpd 15 . . . . . . . . 9
7372ex 424 . . . . . . . 8
7473rexlimdva 2822 . . . . . . 7
759, 74mpd 15 . . . . . 6
76 df-rex 2703 . . . . . 6
7775, 76sylib 189 . . . . 5
78 simpr 448 . . . . . . . . 9
792, 28nfan 1846 . . . . . . . . . . 11
80 stoweidlem60.6 . . . . . . . . . . 11
81 stoweidlem60.7 . . . . . . . . . . 11
82 eqid 2435 . . . . . . . . . . 11
83 eqid 2435 . . . . . . . . . . 11
844adantr 452 . . . . . . . . . . 11
85 stoweidlem60.10 . . . . . . . . . . . 12
8685adantr 452 . . . . . . . . . . 11
87 stoweidlem60.11 . . . . . . . . . . . 12
88873adant1r 1177 . . . . . . . . . . 11
89 stoweidlem60.12 . . . . . . . . . . . 12
90893adant1r 1177 . . . . . . . . . . 11
91 stoweidlem60.13 . . . . . . . . . . . 12
9291adantlr 696 . . . . . . . . . . 11
93 stoweidlem60.14 . . . . . . . . . . . 12
9493adantlr 696 . . . . . . . . . . 11
958adantr 452 . . . . . . . . . . 11
9612adantr 452 . . . . . . . . . . 11
97 stoweidlem60.18 . . . . . . . . . . . 12
9897adantr 452 . . . . . . . . . . 11
99 simpr 448 . . . . . . . . . . 11
1001, 79, 3, 5, 7, 80, 81, 82, 83, 84, 86, 88, 90, 92, 94, 95, 96, 98, 99stoweidlem59 27775 . . . . . . . . . 10
101100adantrr 698 . . . . . . . . 9
102 19.42v 1928 . . . . . . . . 9
10378, 101, 102sylanbrc 646 . . . . . . . 8
104 3anass 940 . . . . . . . . 9
105104exbii 1592 . . . . . . . 8
106103, 105sylibr 204 . . . . . . 7
107106ex 424 . . . . . 6
108107eximdv 1632 . . . . 5
10977, 108mpd 15 . . . 4
110 simpl 444 . . . . . . . 8
111 simpr1l 1014 . . . . . . . 8
112 simpr2 964 . . . . . . . 8
113 nfv 1629 . . . . . . . . . 10
1142, 28, 113nf3an 1849 . . . . . . . . 9
115 simp2 958 . . . . . . . . 9
116 simp3 959 . . . . . . . . 9
117 simp1 957 . . . . . . . . . 10
118117, 87syl3an1 1217 . . . . . . . . 9
119117, 89syl3an1 1217 . . . . . . . . 9
120913ad2antl1 1119 . . . . . . . . 9
121123ad2ant1 978 . . . . . . . . . 10
122121rpred 10640 . . . . . . . . 9
12385sselda 3340 . . . . . . . . . . 11
1243, 5, 7, 123fcnre 27663 . . . . . . . . . 10
1251243ad2antl1 1119 . . . . . . . . 9
126114, 115, 116, 118, 119, 120, 122, 125stoweidlem17 27733 . . . . . . . 8
127110, 111, 112, 126syl3anc 1184 . . . . . . 7
128 nfv 1629 . . . . . . . . 9
129 nfv 1629 . . . . . . . . . 10
130 nfv 1629 . . . . . . . . . 10
131 nfra1 2748 . . . . . . . . . 10
132129, 130, 131nf3an 1849 . . . . . . . . 9
133128, 132nfan 1846 . . . . . . . 8
134 nfra1 2748 . . . . . . . . . . 11
13528, 134nfan 1846 . . . . . . . . . 10
136 nfcv 2571 . . . . . . . . . . 11
137 nfra1 2748 . . . . . . . . . . . 12
138 nfra1 2748 . . . . . . . . . . . 12
139 nfra1 2748 . . . . . . . . . . . 12
140137, 138, 139nf3an 1849 . . . . . . . . . . 11
141136, 140nfral 2751 . . . . . . . . . 10
142135, 113, 141nf3an 1849 . . . . . . . . 9
1432, 142nfan 1846 . . . . . . . 8
144 eqid 2435 . . . . . . . 8
145 uniexg 4698 . . . . . . . . . . 11
1464, 145syl 16 . . . . . . . . . 10
1475, 146syl5eqel 2519 . . . . . . . . 9
148147adantr 452 . . . . . . . 8
14933adantr 452 . . . . . . . 8
150 stoweidlem60.16 . . . . . . . . . 10
151150r19.21bi 2796 . . . . . . . . 9
152151adantlr 696 . . . . . . . 8
153 simpr1r 1015 . . . . . . . . 9
154153r19.21bi 2796 . . . . . . . 8
15512adantr 452 . . . . . . . 8
15697adantr 452 . . . . . . . 8
157 simpll 731 . . . . . . . . 9
158 simplr2 1000 . . . . . . . . 9
159 simpr 448 . . . . . . . . 9
160 simp1 957 . . . . . . . . . 10
161 ffvelrn 5860 . . . . . . . . . . 11
1621613adant1 975 . . . . . . . . . 10
16385sselda 3340 . . . . . . . . . . 11
1643, 5, 7, 163fcnre 27663 . . . . . . . . . 10
165160, 162, 164syl2anc 643 . . . . . . . . 9
166157, 158, 159, 165syl3anc 1184 . . . . . . . 8
167 simp1r3 1055 . . . . . . . . . 10
168 r19.26-3 2832 . . . . . . . . . . 11
169168simp1bi 972 . . . . . . . . . 10
170 simpl 444 . . . . . . . . . . . 12
171170ralimi 2773 . . . . . . . . . . 11
172171ralimi 2773 . . . . . . . . . 10
173167, 169, 1723syl 19 . . . . . . . . 9
174 simp2 958 . . . . . . . . 9
175 simp3 959 . . . . . . . . 9
176 rsp 2758 . . . . . . . . . . 11
177176imp 419 . . . . . . . . . 10
178177r19.21bi 2796 . . . . . . . . 9
179173, 174, 175, 178syl21anc 1183 . . . . . . . 8
180 simpr 448 . . . . . . . . . . . 12
181180ralimi 2773 . . . . . . . . . . 11
182181ralimi 2773 . . . . . . . . . 10
183167, 169, 1823syl 19 . . . . . . . . 9
184 rsp 2758 . . . . . . . . . . 11
185184imp 419 . . . . . . . . . 10
186185r19.21bi 2796 . . . . . . . . 9
187183, 174, 175, 186syl21anc 1183 . . . . . . . 8
188 simp1r3 1055 . . . . . . . . . 10
189168simp2bi 973 . . . . . . . . . 10
190188, 189syl 16 . . . . . . . . 9
191 simp2 958 . . . . . . . . 9
192 simp3 959 . . . . . . . . 9
193 rsp 2758 . . . . . . . . . . 11
194193imp 419 . . . . . . . . . 10
195194r19.21bi 2796 . . . . . . . . 9
196190, 191, 192, 195syl21anc 1183 . . . . . . . 8
197 simp1r3 1055 . . . . . . . . . 10
198168simp3bi 974 . . . . . . . . . 10
199197, 198syl 16 . . . . . . . . 9
200 simp2 958 . . . . . . . . 9
201 simp3 959 . . . . . . . . 9
202 rsp 2758 . . . . . . . . . . 11
203202imp 419 . . . . . . . . . 10
204203r19.21bi 2796 . . . . . . . . 9
205199, 200, 201, 204syl21anc 1183 . . . . . . . 8
2061, 133, 143, 80, 81, 144, 111, 148, 149, 152, 154, 155, 156, 166, 179, 187, 196, 205stoweidlem34 27750 . . . . . . 7
207 nfmpt1 4290 . . . . . . . . . 10
208207nfeq2 2582 . . . . . . . . 9
209 fveq1 5719 . . . . . . . . . . . . 13
210209breq1d 4214 . . . . . . . . . . . 12
211209breq2d 4216 . . . . . . . . . . . 12
212210, 211anbi12d 692 . . . . . . . . . . 11
213212anbi2d 685 . . . . . . . . . 10
214213rexbidv 2718 . . . . . . . . 9
215208, 214ralbid 2715 . . . . . . . 8
216215rspcev 3044 . . . . . . 7
217127, 206, 216syl2anc 643 . . . . . 6
218217ex 424 . . . . 5
2192182eximdv 1634 . . . 4