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

Theorem stoweidlem55 27782
 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 9093 . . . . 5
2 stoweidlem55.10 . . . . . 6
32stoweidlem4 27731 . . . . 5
41, 3mpan2 654 . . . 4
6 stoweidlem55.2 . . . . 5
7 nfcv 2574 . . . . . . 7
8 stoweidlem55.1 . . . . . . 7
97, 8nfdif 3470 . . . . . 6
10 nfcv 2574 . . . . . 6
119, 10nfeq 2581 . . . . 5
126, 11nfan 1847 . . . 4
13 0le0 10083 . . . . . . . 8
14 0cn 9086 . . . . . . . . 9
15 eqid 2438 . . . . . . . . . 10
1615fvmpt2 5814 . . . . . . . . 9
1714, 16mpan2 654 . . . . . . . 8
1813, 17syl5breqr 4250 . . . . . . 7
1918adantl 454 . . . . . 6
20 0le1 9553 . . . . . . . 8
2117, 20syl6eqbr 4251 . . . . . . 7
2221adantl 454 . . . . . 6
2319, 22jca 520 . . . . 5
2423ex 425 . . . 4
2512, 24ralrimi 2789 . . 3
26 stoweidlem55.13 . . . . . 6
27 stoweidlem55.12 . . . . . 6
2826, 27jca 520 . . . . 5
29 elunii 4022 . . . . . 6
30 stoweidlem55.5 . . . . . 6
3129, 30syl6eleqr 2529 . . . . 5
32 eqidd 2439 . . . . . 6
33 c0ex 9087 . . . . . 6
3432, 15, 33fvmpt 5808 . . . . 5
3528, 31, 343syl 19 . . . 4
3711rzalf 27666 . . . 4
39 nfcv 2574 . . . . . . 7
40 nfmpt1 4300 . . . . . . 7
4139, 40nfeq 2581 . . . . . 6
42 fveq1 5729 . . . . . . . 8
4342breq2d 4226 . . . . . . 7
4442breq1d 4224 . . . . . . 7
4543, 44anbi12d 693 . . . . . 6
4641, 45ralbid 2725 . . . . 5
47 fveq1 5729 . . . . . 6
4847eqeq1d 2446 . . . . 5
4942breq2d 4226 . . . . . 6
5041, 49ralbid 2725 . . . . 5
5146, 48, 503anbi123d 1255 . . . 4
5251rspcev 3054 . . 3
535, 25, 36, 38, 52syl13anc 1187 . 2
5411nfn 1812 . . . 4
556, 54nfan 1847 . . 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
66 stoweidlem55.9 . . . 4