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

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

Proof of Theorem stoweidlem55
StepHypRef Expression
1 0re 9640 . . . . 5
2 stoweidlem55.10 . . . . . 6
32stoweidlem4 37858 . . . . 5
41, 3mpan2 676 . . . 4
6 stoweidlem55.2 . . . . 5
7 nfcv 2591 . . . . . . 7
8 stoweidlem55.1 . . . . . . 7
97, 8nfdif 3553 . . . . . 6
10 nfcv 2591 . . . . . 6
119, 10nfeq 2602 . . . . 5
126, 11nfan 2010 . . . 4
13 0le0 10696 . . . . . . . 8
14 0cn 9632 . . . . . . . . 9
15 eqid 2450 . . . . . . . . . 10
1615fvmpt2 5955 . . . . . . . . 9
1714, 16mpan2 676 . . . . . . . 8
1813, 17syl5breqr 4438 . . . . . . 7
1918adantl 468 . . . . . 6
20 0le1 10134 . . . . . . . 8
2117, 20syl6eqbr 4439 . . . . . . 7
2221adantl 468 . . . . . 6
2319, 22jca 535 . . . . 5
2423ex 436 . . . 4
2512, 24ralrimi 2787 . . 3
26 stoweidlem55.13 . . . . . 6
27 stoweidlem55.12 . . . . . 6
2826, 27jca 535 . . . . 5
29 elunii 4202 . . . . . 6
30 stoweidlem55.5 . . . . . 6
3129, 30syl6eleqr 2539 . . . . 5
32 eqidd 2451 . . . . . 6
33 c0ex 9634 . . . . . 6
3432, 15, 33fvmpt 5946 . . . . 5
3528, 31, 343syl 18 . . . 4
3711rzalf 37332 . . . 4
39 nfcv 2591 . . . . . . 7
40 nfmpt1 4491 . . . . . . 7
4139, 40nfeq 2602 . . . . . 6
42 fveq1 5862 . . . . . . . 8
4342breq2d 4413 . . . . . . 7
4442breq1d 4411 . . . . . . 7
4543, 44anbi12d 716 . . . . . 6
4641, 45ralbid 2821 . . . . 5
47 fveq1 5862 . . . . . 6
4847eqeq1d 2452 . . . . 5
4942breq2d 4413 . . . . . 6
5041, 49ralbid 2821 . . . . 5
5146, 48, 503anbi123d 1338 . . . 4
5251rspcev 3149 . . 3
535, 25, 36, 38, 52syl13anc 1269 . 2
5411nfn 1982 . . . 4
556, 54nfan 2010 . . 3
56 stoweidlem55.3 . . 3
57 stoweidlem55.14 . . 3
58 stoweidlem55.15 . . 3
59 stoweidlem55.6 . . 3
60 stoweidlem55.4 . . . 4
62 stoweidlem55.7 . . . 4
64 stoweidlem55.8 . . . 4