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

Theorem stoweidlem44 27205
 Description: This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem44.1
stoweidlem44.2
stoweidlem44.3
stoweidlem44.4
stoweidlem44.5
stoweidlem44.6
stoweidlem44.7
stoweidlem44.8
stoweidlem44.9
stoweidlem44.10
stoweidlem44.11
stoweidlem44.12
stoweidlem44.13
stoweidlem44.14
Assertion
Ref Expression
stoweidlem44
Distinct variable groups:   ,,,,   ,,,,   ,,   ,,,,   ,,,,   ,,,   ,,,,   ,   ,,   ,,,   ,,,   ,   ,,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,,)   (,,,,,,)   (,,,,,,,)   (,,,,,)   (,)   (,,,,,,,)   (,,,,,,,)   (,)   (,,,)

Proof of Theorem stoweidlem44
StepHypRef Expression
1 stoweidlem44.2 . . . . 5
2 stoweidlem44.5 . . . . 5
3 eqid 2283 . . . . 5
4 eqidd 2284 . . . . . 6
54cbvmptv 4111 . . . . 5
6 stoweidlem44.6 . . . . 5
7 1re 8837 . . . . . . . 8
87a1i 10 . . . . . . 7
9 id 19 . . . . . . . 8
10 nnre 9753 . . . . . . . . 9
116, 10syl 15 . . . . . . . 8
129, 11syl 15 . . . . . . 7
13 nnne0 9778 . . . . . . . 8
146, 13syl 15 . . . . . . 7
158, 12, 143jca 1132 . . . . . 6
16 redivcl 9479 . . . . . 6
1715, 16syl 15 . . . . 5
18 stoweidlem44.7 . . . . . . 7
19 stoweidlem44.4 . . . . . . . . 9
20 ssrab2 3258 . . . . . . . . 9
2119, 20eqsstri 3208 . . . . . . . 8
2221a1i 10 . . . . . . 7
2318, 22jca 518 . . . . . 6
24 fss 5397 . . . . . 6
2523, 24syl 15 . . . . 5
26 stoweidlem44.11 . . . . 5
27 stoweidlem44.12 . . . . 5
28 stoweidlem44.13 . . . . . 6
2928idi 2 . . . . 5
30 stoweidlem44.3 . . . . . 6
31 stoweidlem44.9 . . . . . 6
32 eqid 2283 . . . . . 6
33 stoweidlem44.10 . . . . . . . 8
34 ssel 3174 . . . . . . . 8
3533, 34syl 15 . . . . . . 7
3635imp 418 . . . . . 6
3730, 31, 32, 36fcnre 27108 . . . . 5
381, 2, 3, 5, 6, 17, 25, 26, 27, 29, 37stoweidlem32 27193 . . . 4
391idi 2 . . . . . 6
4019, 2, 6, 18, 37stoweidlem38 27199 . . . . . . 7
4140ex 423 . . . . . 6
4239, 41ralrimi 2624 . . . . 5
4333adantr 451 . . . . . . . . 9
44 simpr 447 . . . . . . . . 9
4543, 44jca 518 . . . . . . . 8
46 ssel2 3175 . . . . . . . 8
4745, 46syl 15 . . . . . . 7
4830, 31, 32, 47fcnre 27108 . . . . . 6
49 stoweidlem44.14 . . . . . 6
5019, 2, 6, 18, 48, 49stoweidlem37 27198 . . . . 5
51 stoweidlem44.8 . . . . . . . . . . . . 13
5251adantr 451 . . . . . . . . . . . 12
53 simpr 447 . . . . . . . . . . . 12
5452, 53jca 518 . . . . . . . . . . 11
55 rsp 2603 . . . . . . . . . . . 12
5655imp 418 . . . . . . . . . . 11
5754, 56syl 15 . . . . . . . . . 10
58 df-rex 2549 . . . . . . . . . 10
5957, 58sylib 188 . . . . . . . . 9
60 stoweidlem44.1 . . . . . . . . . . 11
61 nfv 1605 . . . . . . . . . . 11
6260, 61nfan 1771 . . . . . . . . . 10
63 nfv 1605 . . . . . . . . . 10
6417adantr 451 . . . . . . . . . . . . . . 15
6564adantr 451 . . . . . . . . . . . . . 14
66 0lt1 9296 . . . . . . . . . . . . . . . . . . . 20
6766a1i 10 . . . . . . . . . . . . . . . . . . 19
688, 67jca 518 . . . . . . . . . . . . . . . . . 18
69 nngt0 9775 . . . . . . . . . . . . . . . . . . . 20
706, 69syl 15 . . . . . . . . . . . . . . . . . . 19
7111, 70jca 518 . . . . . . . . . . . . . . . . . 18
7268, 71jca 518 . . . . . . . . . . . . . . . . 17
73 divgt0 9624 . . . . . . . . . . . . . . . . 17
7472, 73syl 15 . . . . . . . . . . . . . . . 16
7574adantr 451 . . . . . . . . . . . . . . 15
7675adantr 451 . . . . . . . . . . . . . 14
7765, 76jca 518 . . . . . . . . . . . . 13
78 simpll 730 . . . . . . . . . . . . . . . 16
79 eldifi 3298 . . . . . . . . . . . . . . . . . 18
8079adantl 452 . . . . . . . . . . . . . . . . 17
8180adantr 451 . . . . . . . . . . . . . . . 16
8278, 81jca 518 . . . . . . . . . . . . . . 15
83 fzfi 11034 . . . . . . . . . . . . . . . . 17
8483a1i 10 . . . . . . . . . . . . . . . 16
85 simpll 730 . . . . . . . . . . . . . . . . . . . 20
86 simpr 447 . . . . . . . . . . . . . . . . . . . 20
8785, 86jca 518 . . . . . . . . . . . . . . . . . . 19
88 simplr 731 . . . . . . . . . . . . . . . . . . 19
8987, 88jca 518 . . . . . . . . . . . . . . . . . 18
9019, 18, 48stoweidlem15 27176 . . . . . . . . . . . . . . . . . 18
9189, 90syl 15 . . . . . . . . . . . . . . . . 17
92 simp1 955 . . . . . . . . . . . . . . . . 17
9391, 92syl 15 . . . . . . . . . . . . . . . 16
9484, 93fsumrecl 12207 . . . . . . . . . . . . . . 15
9582, 94syl 15 . . . . . . . . . . . . . 14
96 00id 8987 . . . . . . . . . . . . . . . . . 18
97 simprr 733 . . . . . . . . . . . . . . . . . . . 20
98 simprl 732 . . . . . . . . . . . . . . . . . . . . . 22
9978, 98jca 518 . . . . . . . . . . . . . . . . . . . . . . . . 25
10099, 81jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24
10119, 18, 37stoweidlem15 27176 . . . . . . . . . . . . . . . . . . . . . . . . 25
102101simp1d 967 . . . . . . . . . . . . . . . . . . . . . . . 24
103100, 102syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
104 recn 8827 . . . . . . . . . . . . . . . . . . . . . . 23
105103, 104syl 15 . . . . . . . . . . . . . . . . . . . . . 22
10698, 105jca 518 . . . . . . . . . . . . . . . . . . . . 21
107 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . 23
108107fveq1d 5527 . . . . . . . . . . . . . . . . . . . . . 22
109108sumsn 12213 . . . . . . . . . . . . . . . . . . . . 21
110106, 109syl 15 . . . . . . . . . . . . . . . . . . . 20
11197, 110breqtrrd 4049 . . . . . . . . . . . . . . . . . . 19
112 0re 8838 . . . . . . . . . . . . . . . . . . . . . 22
113112a1i 10 . . . . . . . . . . . . . . . . . . . . 21
11478, 98, 813jca 1132 . . . . . . . . . . . . . . . . . . . . . 22
115 snfi 6941 . . . . . . . . . . . . . . . . . . . . . . . 24
116115a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23
117 simpl1 958 . . . . . . . . . . . . . . . . . . . . . . . . . 26
118 simpl3 960 . . . . . . . . . . . . . . . . . . . . . . . . . 26
119117, 118jca 518 . . . . . . . . . . . . . . . . . . . . . . . . 25
120 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
121 elsni 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
122120, 121syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123 simpl2 959 . . . . . . . . . . . . . . . . . . . . . . . . . 26
124122, 123eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . . . . 25
125119, 124jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24
126125, 93syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
127116, 126fsumrecl 12207 . . . . . . . . . . . . . . . . . . . . . 22
128114, 127syl 15 . . . . . . . . . . . . . . . . . . . . 21
129113, 128, 1133jca 1132 . . . . . . . . . . . . . . . . . . . 20
130 ltadd2 8924 . . . . . . . . . . . . . . . . . . . 20
131129, 130syl 15 . . . . . . . . . . . . . . . . . . 19
132111, 131mpbid 201 . . . . . . . . . . . . . . . . . 18
13396, 132syl5eqbrr 4057 . . . . . . . . . . . . . . . . 17
134 3simpb 953 . . . . . . . . . . . . . . . . . . . 20
135 diffi 7089 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13683, 135ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . 25
137 0cn 8831 . . . . . . . . . . . . . . . . . . . . . . . . 25
138136, 137pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . 24
139 fsumconst 12252 . . . . . . . . . . . . . . . . . . . . . . . 24
140138, 139ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23
141 hashcl 11350 . . . . . . . . . . . . . . . . . . . . . . . . . 26
142136, 141ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . 25
143 nn0cn 9975 . . . . . . . . . . . . . . . . . . . . . . . . 25
144142, 143ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24
145 mul01 8991 . . . . . . . . . . . . . . . . . . . . . . . 24
146144, 145ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23
147140, 146eqtri 2303 . . . . . . . . . . . . . . . . . . . . . 22
148147a1i 10 . . . . . . . . . . . . . . . . . . . . 21
149136a1i 10 . . . . . . . . . . . . . . . . . . . . . 22
150112a1i 10 . . . . . . . . . . . . . . . . . . . . . 22
151 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . 24
152 eldifi 3298 . . . . . . . . . . . . . . . . . . . . . . . . 25
153152adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24
154151, 153jca 518 . . . . . . . . . . . . . . . . . . . . . . 23
155154, 93syl 15 . . . . . . . . . . . . . . . . . . . . . 22
156 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26
157156, 153jca 518 . . . . . . . . . . . . . . . . . . . . . . . . 25
158 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25
159157, 158jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24
160159, 90syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
161160simp2d 968 . . . . . . . . . . . . . . . . . . . . . 22
162149, 150, 155, 161fsumle 12257 . . . . . . . . . . . . . . . . . . . . 21
163148, 162eqbrtrrd 4045 . . . . . . . . . . . . . . . . . . . 20
164134, 163syl 15 . . . . . . . . . . . . . . . . . . 19
165112a1i 10 . . . . . . . . . . . . . . . . . . . . 21
166149, 155fsumrecl 12207 . . . . . . . . . . . . . . . . . . . . . 22
167134, 166syl 15 . . . . . . . . . . . . . . . . . . . . 21
168165, 167, 1273jca 1132 . . . . . . . . . . . . . . . . . . . 20
169 leadd1 9242 . . . . . . . . . . . . . . . . . . . 20
170168, 169syl 15 . . . . . . . . . . . . . . . . . . 19
171164, 170mpbid 201 . . . . . . . . . . . . . . . . . 18
172114, 171syl 15 . . . . . . . . . . . . . . . . 17
173133, 172jca 518 . . . . . . . . . . . . . . . 16
174113, 128jca 518 . . . . . . . . . . . . . . . . . . 19
175 readdcl 8820 . . . . . . . . . . . . . . . . . . 19
176174, 175syl 15 . . . . . . . . . . . . . . . . . 18
17782, 166syl 15 . . . . . . . . . . . . . . . . . . . 20
178177, 128jca 518 . . . . . . . . . . . . . . . . . . 19
179 readdcl 8820 . . . . . . . . . . . . . . . . . . 19
180178, 179syl 15 . . . . . . . . . . . . . . . . . 18
181113, 176, 1803jca 1132 . . . . . . . . . . . . . . . . 17
182 ltletr 8913 . . . . . . . . . . . . . . . . 17
183181, 182syl 15 . . . . . . . . . . . . . . . 16
184173, 183mpd 14 . . . . . . . . . . . . . . 15
185 eldifn 3299 . . . . . . . . . . . . . . . . . . . . . 22
186 imnan 411 . . . . . . . . . . . . . . . . . . . . . 22
187185, 186mpbi 199 . . . . . . . . . . . . . . . . . . . . 21
188 elin 3358 . . . . . . . . . . . . . . . . . . . . 21
189187, 188mtbir 290 . . . . . . . . . . . . . . . . . . . 20
190189ax-gen 1533 . . . . . . . . . . . . . . . . . . 19
191 eq0 3469 . . . . . . . . . . . . . . . . . . 19
192190, 191mpbir 200 . . . . . . . . . . . . . . . . . 18
193192a1i 10 . . . . . . . . . . . . . . . . 17
194 undif1 3529 . . . . . . . . . . . . . . . . . 18
195 snssi 3759 . . . . . . . . . . . . . . . . . . . 20
1961953ad2ant2 977 . . . . . . . . . . . . . . . . . . 19
197 ssequn2 3348 . . . . . . . . . . . . . . . . . . 19
198196, 197sylib 188 . . . . . . . . . . . . . . . . . 18
199194, 198syl5req 2328 . . . . . . . . . . . . . . . . 17
20083a1i 10 . . . . . . . . . . . . . . . . 17
201 simpl1 958 . . . . . . . . . . . . . . . . . . . . 21
202 simpl3 960 . . . . . . . . . . . . . . . . . . . . 21
203201, 202jca 518 . . . . . . . . . . . . . . . . . . . 20
204 simpr 447 . . . . . . . . . . . . . . . . . . . 20
205203, 204jca 518 . . . . . . . . . . . . . . . . . . 19
206205, 93syl 15 . . . . . . . . . . . . . . . . . 18
207 recn 8827 . . . . . . . . . . . . . . . . . 18
208206, 207syl 15 . . . . . . . . . . . . . . . . 17
209193, 199, 200, 208fsumsplit 12212 . . . . . . . . . . . . . . . 16
210114, 209syl 15 . . . . . . . . . . . . . . 15
211184, 210breqtrrd 4049 . . . . . . . . . . . . . 14
21295, 211jca 518 . . . . . . . . . . . . 13
21377, 212jca 518 . . . . . . . . . . . 12
214 mulgt0 8900 . . . . . . . . . . . 12
215213, 214syl 15 . . . . . . . . . . 11
216215ex 423 . . . . . . . . . 10
21762, 63, 216exlimd 1803 . . . . . . . . 9
21859, 217mpd 14 . . . . . . . 8
219 simpl 443 . . . . . . . . . 10
220219, 80jca 518 . . . . . . . . 9
22119, 2, 6, 18, 48stoweidlem30 27191 . . . . . . . . 9
222220, 221syl 15 . . . . . . . 8
223218, 222breqtrrd 4049 . . . . . . 7
224223ex 423 . . . . . 6
22539, 224ralrimi 2624 . . . . 5
22642, 50, 2253jca 1132 . . . 4
22738, 226jca 518 . . 3
228 eleq1 2343 . . . . . 6
229 nfcv 2419 . . . . . . . . 9
230 nfmpt1 4109 . . . . . . . . . 10
2312, 230nfcxfr 2416 . . . . . . . . 9
232229, 231nfeq 2426 . . . . . . . 8
233 fveq1 5524 . . . . . . . . . 10
234233breq2d 4035 . . . . . . . . 9
235233breq1d 4033 . . . . . . . . 9
236234, 235anbi12d 691 . . . . . . . 8
237232, 236ralbid 2561 . . . . . . 7
238 fveq1 5524 . . . . . . . 8
239238eqeq1d 2291 . . . . . . 7
240233breq2d 4035 . . . . . . . 8
241232, 240ralbid 2561 . . . . . . 7
242237, 239, 2413anbi123d 1252 . . . . . 6
243228, 242anbi12d 691 . . . . 5
244243spcegv 2869 . . . 4
24538, 244syl 15 . . 3
246227, 245mpd 14 . 2
247 df-rex 2549 . 2
248246, 247sylibr 203 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 934  wal 1527  wex 1528  wnf 1531   wceq 1623   wcel 1684   wne 2446  wral 2543  wrex 2544  crab 2547   cdif 3149   cun 3150   cin 3151   wss 3152  c0 3455  csn 3640  cuni 3827   class class class wbr 4023   cmpt 4077   crn 4690  wf 5251  cfv 5255  (class class class)co 5858  cfn 6863  cc 8735  cr 8736  cc0 8737  c1 8738   caddc 8740   cmul 8742   clt 8867   cle 8868   cdiv 9423  cn 9746  cn0 9965  cioo 10656  cfz 10782  chash 11337  csu 12158  ctg 13342   ccn 16954 This theorem is referenced by:  stoweidlem53  27214 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-sup 7194  df-oi 7225  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-ioo 10660  df-ico 10662  df-fz 10783  df-fzo 10871  df-seq 11047  df-exp 11105  df-hash 11338  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-clim 11962  df-sum 12159  df-topgen 13344  df-top 16636  df-bases 16638  df-topon 16639  df-cn 16957
 Copyright terms: Public domain W3C validator