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

Theorem stoweidlem55 27907
 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 8854 . . . . . . . 8
21a1i 10 . . . . . . 7
32ancli 534 . . . . . 6
4 stoweidlem55.10 . . . . . . 7
54stoweidlem4 27856 . . . . . 6
63, 5syl 15 . . . . 5
76adantr 451 . . . 4
8 stoweidlem55.2 . . . . . . 7
9 nfcv 2432 . . . . . . . . 9
10 stoweidlem55.1 . . . . . . . . 9
119, 10nfdif 3310 . . . . . . . 8
12 nfcv 2432 . . . . . . . 8
1311, 12nfeq 2439 . . . . . . 7
148, 13nfan 1783 . . . . . 6
15 leid 8932 . . . . . . . . . . 11
161, 15ax-mp 8 . . . . . . . . . 10
17 0cn 8847 . . . . . . . . . . . . 13
1817jctr 526 . . . . . . . . . . . 12
19 eqid 2296 . . . . . . . . . . . . 13
2019fvmpt2 5624 . . . . . . . . . . . 12
2118, 20syl 15 . . . . . . . . . . 11
2221eqcomd 2301 . . . . . . . . . 10
2316, 22syl5breq 4074 . . . . . . . . 9
2423adantl 452 . . . . . . . 8
25 0le1 9313 . . . . . . . . . 10
2622, 25syl6eqbrr 4077 . . . . . . . . 9
2726adantl 452 . . . . . . . 8
2824, 27jca 518 . . . . . . 7
2928ex 423 . . . . . 6
3014, 29ralrimi 2637 . . . . 5
31 stoweidlem55.13 . . . . . . . . 9
32 stoweidlem55.12 . . . . . . . . 9
3331, 32jca 518 . . . . . . . 8
34 elunii 3848 . . . . . . . . 9
35 stoweidlem55.5 . . . . . . . . 9
3634, 35syl6eleqr 2387 . . . . . . . 8
3733, 36syl 15 . . . . . . 7
38 eqidd 2297 . . . . . . . 8
39 elex 2809 . . . . . . . . 9
4017, 39ax-mp 8 . . . . . . . 8
4138, 19, 40fvmpt 5618 . . . . . . 7
4237, 41syl 15 . . . . . 6
4342adantr 451 . . . . 5
4413rzalf 27791 . . . . . 6
4544adantl 452 . . . . 5
4630, 43, 453jca 1132 . . . 4
477, 46jca 518 . . 3
48 nfcv 2432 . . . . . . 7
49 nfmpt1 4125 . . . . . . 7
5048, 49nfeq 2439 . . . . . 6
51 fveq1 5540 . . . . . . . 8
5251breq2d 4051 . . . . . . 7
5351breq1d 4049 . . . . . . 7
5452, 53anbi12d 691 . . . . . 6
5550, 54ralbid 2574 . . . . 5
56 fveq1 5540 . . . . . 6
5756eqeq1d 2304 . . . . 5
5851breq2d 4051 . . . . . 6
5950, 58ralbid 2574 . . . . 5
6055, 57, 593anbi123d 1252 . . . 4
6160rspcev 2897 . . 3
6247, 61syl 15 . 2
6313nfn 1777 . . . 4
648, 63nfan 1783 . . 3
65 stoweidlem55.3 . . 3
66 stoweidlem55.14 . . 3
67 stoweidlem55.15 . . 3
68 stoweidlem55.6 . . 3
69 stoweidlem55.4 . . . 4
71 stoweidlem55.7 . . . 4
73 simp1l 979 . . . . 5
74 simp2 956 . . . . 5
75 simp3 957 . . . . 5
7673, 74, 753jca 1132 . . . 4
77 stoweidlem55.8 . . . 4
7876, 77syl 15 . . 3
79 stoweidlem55.9 . . . 4
8076, 79syl 15 . . 3
81 simpll 730 . . . . 5
82 simpr 447 . . . . 5
8381, 82jca 518 . . . 4
8483, 4syl 15 . . 3
85 simpll 730 . . . . 5
86 simpr 447 . . . . 5
8785, 86jca 518 . . . 4
88 stoweidlem55.11 . . . 4
8987, 88syl 15 . . 3