Metamath Proof Explorer

Theorem stoweidlem5

Description: There exists a δ as in the proof of Lemma 1 in BrosowskiDeutsh p. 90: 0 < δ < 1 , p >= δ on T \ U . Here D is used to represent δ in the paper and Q to represent T \ U in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem5.1 
|- F/ t ph
stoweidlem5.2 
|- D = if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) )
stoweidlem5.3 
|- ( ph -> P : T --> RR )
stoweidlem5.4 
|- ( ph -> Q C_ T )
stoweidlem5.5 
|- ( ph -> C e. RR+ )
stoweidlem5.6 
|- ( ph -> A. t e. Q C <_ ( P ` t ) )
Assertion stoweidlem5 
|- ( ph -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. Q d <_ ( P ` t ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem5.1 
 |-  F/ t ph
2 stoweidlem5.2 
 |-  D = if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) )
3 stoweidlem5.3 
 |-  ( ph -> P : T --> RR )
4 stoweidlem5.4 
 |-  ( ph -> Q C_ T )
5 stoweidlem5.5 
 |-  ( ph -> C e. RR+ )
6 stoweidlem5.6 
 |-  ( ph -> A. t e. Q C <_ ( P ` t ) )
7 halfre 
 |-  ( 1 / 2 ) e. RR
8 halfgt0 
 |-  0 < ( 1 / 2 )
9 7 8 elrpii 
 |-  ( 1 / 2 ) e. RR+
10 ifcl 
 |-  ( ( C e. RR+ /\ ( 1 / 2 ) e. RR+ ) -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) e. RR+ )
11 5 9 10 sylancl 
 |-  ( ph -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) e. RR+ )
12 2 11 eqeltrid 
 |-  ( ph -> D e. RR+ )
13 12 rpred 
 |-  ( ph -> D e. RR )
14 7 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
15 1red 
 |-  ( ph -> 1 e. RR )
16 5 rpred 
 |-  ( ph -> C e. RR )
17 min2 
 |-  ( ( C e. RR /\ ( 1 / 2 ) e. RR ) -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) <_ ( 1 / 2 ) )
18 16 7 17 sylancl 
 |-  ( ph -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) <_ ( 1 / 2 ) )
19 2 18 eqbrtrid 
 |-  ( ph -> D <_ ( 1 / 2 ) )
20 halflt1 
 |-  ( 1 / 2 ) < 1
21 20 a1i 
 |-  ( ph -> ( 1 / 2 ) < 1 )
22 13 14 15 19 21 lelttrd 
 |-  ( ph -> D < 1 )
23 11 rpred 
 |-  ( ph -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) e. RR )
24 23 adantr 
 |-  ( ( ph /\ t e. Q ) -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) e. RR )
25 16 adantr 
 |-  ( ( ph /\ t e. Q ) -> C e. RR )
26 3 adantr 
 |-  ( ( ph /\ t e. Q ) -> P : T --> RR )
27 4 sselda 
 |-  ( ( ph /\ t e. Q ) -> t e. T )
28 26 27 ffvelrnd 
 |-  ( ( ph /\ t e. Q ) -> ( P ` t ) e. RR )
29 min1 
 |-  ( ( C e. RR /\ ( 1 / 2 ) e. RR ) -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) <_ C )
30 16 7 29 sylancl 
 |-  ( ph -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) <_ C )
31 30 adantr 
 |-  ( ( ph /\ t e. Q ) -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) <_ C )
32 6 r19.21bi 
 |-  ( ( ph /\ t e. Q ) -> C <_ ( P ` t ) )
33 24 25 28 31 32 letrd 
 |-  ( ( ph /\ t e. Q ) -> if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) ) <_ ( P ` t ) )
34 2 33 eqbrtrid 
 |-  ( ( ph /\ t e. Q ) -> D <_ ( P ` t ) )
35 34 ex 
 |-  ( ph -> ( t e. Q -> D <_ ( P ` t ) ) )
36 1 35 ralrimi 
 |-  ( ph -> A. t e. Q D <_ ( P ` t ) )
37 eleq1 
 |-  ( d = D -> ( d e. RR+ <-> D e. RR+ ) )
38 breq1 
 |-  ( d = D -> ( d < 1 <-> D < 1 ) )
39 breq1 
 |-  ( d = D -> ( d <_ ( P ` t ) <-> D <_ ( P ` t ) ) )
40 39 ralbidv 
 |-  ( d = D -> ( A. t e. Q d <_ ( P ` t ) <-> A. t e. Q D <_ ( P ` t ) ) )
41 37 38 40 3anbi123d 
 |-  ( d = D -> ( ( d e. RR+ /\ d < 1 /\ A. t e. Q d <_ ( P ` t ) ) <-> ( D e. RR+ /\ D < 1 /\ A. t e. Q D <_ ( P ` t ) ) ) )
42 41 spcegv 
 |-  ( D e. RR+ -> ( ( D e. RR+ /\ D < 1 /\ A. t e. Q D <_ ( P ` t ) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. Q d <_ ( P ` t ) ) ) )
43 12 42 syl 
 |-  ( ph -> ( ( D e. RR+ /\ D < 1 /\ A. t e. Q D <_ ( P ` t ) ) -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. Q d <_ ( P ` t ) ) ) )
44 12 22 36 43 mp3and 
 |-  ( ph -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. Q d <_ ( P ` t ) ) )