Metamath Proof Explorer

Theorem stoweidlem45

Description: This lemma proves that, given an appropriate K (in another theorem we prove such a K exists), there exists a function q_n as in the proof of Lemma 1 in BrosowskiDeutsh p. 91 ( at the top of page 91): 0 <= q_n <= 1 , q_n < ε on T \ U, and q_n > 1 - ε on V . We use y to represent the final q_n in the paper (the one with n large enough), N to represent n in the paper, K to represent k , D to represent δ, E to represent ε, and P to represent p . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem45.1 
|- F/_ t P
stoweidlem45.2 
|- F/ t ph
stoweidlem45.3 
|- V = { t e. T | ( P ` t ) < ( D / 2 ) }
stoweidlem45.4 
|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
stoweidlem45.5 
|- ( ph -> N e. NN )
stoweidlem45.6 
|- ( ph -> K e. NN )
stoweidlem45.7 
|- ( ph -> D e. RR+ )
stoweidlem45.8 
|- ( ph -> D < 1 )
stoweidlem45.9 
|- ( ph -> P e. A )
stoweidlem45.10 
|- ( ph -> P : T --> RR )
stoweidlem45.11 
|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
stoweidlem45.12 
|- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
stoweidlem45.13 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem45.14 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem45.15 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem45.16 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem45.17 
|- ( ph -> E e. RR+ )
stoweidlem45.18 
|- ( ph -> ( 1 - E ) < ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) )
stoweidlem45.19 
|- ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )
Assertion stoweidlem45 
|- ( ph -> E. y e. A ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < E ) )

Proof

Step Hyp Ref Expression
1 stoweidlem45.1 
 |-  F/_ t P
2 stoweidlem45.2 
 |-  F/ t ph
3 stoweidlem45.3 
 |-  V = { t e. T | ( P ` t ) < ( D / 2 ) }
4 stoweidlem45.4 
 |-  Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
5 stoweidlem45.5 
 |-  ( ph -> N e. NN )
6 stoweidlem45.6 
 |-  ( ph -> K e. NN )
7 stoweidlem45.7 
 |-  ( ph -> D e. RR+ )
8 stoweidlem45.8 
 |-  ( ph -> D < 1 )
9 stoweidlem45.9 
 |-  ( ph -> P e. A )
10 stoweidlem45.10 
 |-  ( ph -> P : T --> RR )
11 stoweidlem45.11 
 |-  ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
12 stoweidlem45.12 
 |-  ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
13 stoweidlem45.13 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
14 stoweidlem45.14 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
15 stoweidlem45.15 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
16 stoweidlem45.16 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
17 stoweidlem45.17 
 |-  ( ph -> E e. RR+ )
18 stoweidlem45.18 
 |-  ( ph -> ( 1 - E ) < ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) )
19 stoweidlem45.19 
 |-  ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )
20 eqid 
 |-  ( t e. T |-> ( 1 - ( ( P ` t ) ^ N ) ) ) = ( t e. T |-> ( 1 - ( ( P ` t ) ^ N ) ) )
21 eqid 
 |-  ( t e. T |-> 1 ) = ( t e. T |-> 1 )
22 eqid 
 |-  ( t e. T |-> ( ( P ` t ) ^ N ) ) = ( t e. T |-> ( ( P ` t ) ^ N ) )
23 5 nnnn0d 
 |-  ( ph -> N e. NN0 )
24 6 23 nnexpcld 
 |-  ( ph -> ( K ^ N ) e. NN )
25 1 2 4 20 21 22 9 10 13 14 15 16 5 24 stoweidlem40 
 |-  ( ph -> Q e. A )
26 1red 
 |-  ( ( ph /\ t e. T ) -> 1 e. RR )
27 10 ffvelcdmda 
 |-  ( ( ph /\ t e. T ) -> ( P ` t ) e. RR )
28 23 adantr 
 |-  ( ( ph /\ t e. T ) -> N e. NN0 )
29 27 28 reexpcld 
 |-  ( ( ph /\ t e. T ) -> ( ( P ` t ) ^ N ) e. RR )
30 26 29 resubcld 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) e. RR )
31 6 nnnn0d 
 |-  ( ph -> K e. NN0 )
32 31 23 nn0expcld 
 |-  ( ph -> ( K ^ N ) e. NN0 )
33 32 adantr 
 |-  ( ( ph /\ t e. T ) -> ( K ^ N ) e. NN0 )
34 1m1e0 
 |-  ( 1 - 1 ) = 0
35 11 r19.21bi 
 |-  ( ( ph /\ t e. T ) -> ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
36 35 simpld 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( P ` t ) )
37 35 simprd 
 |-  ( ( ph /\ t e. T ) -> ( P ` t ) <_ 1 )
38 exple1 
 |-  ( ( ( ( P ` t ) e. RR /\ 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) /\ N e. NN0 ) -> ( ( P ` t ) ^ N ) <_ 1 )
39 27 36 37 28 38 syl31anc 
 |-  ( ( ph /\ t e. T ) -> ( ( P ` t ) ^ N ) <_ 1 )
40 29 26 26 39 lesub2dd 
 |-  ( ( ph /\ t e. T ) -> ( 1 - 1 ) <_ ( 1 - ( ( P ` t ) ^ N ) ) )
41 34 40 eqbrtrrid 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( 1 - ( ( P ` t ) ^ N ) ) )
42 30 33 41 expge0d 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
43 4 10 23 31 stoweidlem12 
 |-  ( ( ph /\ t e. T ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
44 42 43 breqtrrd 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( Q ` t ) )
45 0red 
 |-  ( ( ph /\ t e. T ) -> 0 e. RR )
46 27 28 36 expge0d 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( ( P ` t ) ^ N ) )
47 45 29 26 46 lesub2dd 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) <_ ( 1 - 0 ) )
48 1m0e1 
 |-  ( 1 - 0 ) = 1
49 47 48 breqtrdi 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) <_ 1 )
50 exple1 
 |-  ( ( ( ( 1 - ( ( P ` t ) ^ N ) ) e. RR /\ 0 <_ ( 1 - ( ( P ` t ) ^ N ) ) /\ ( 1 - ( ( P ` t ) ^ N ) ) <_ 1 ) /\ ( K ^ N ) e. NN0 ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) <_ 1 )
51 30 41 49 33 50 syl31anc 
 |-  ( ( ph /\ t e. T ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) <_ 1 )
52 43 51 eqbrtrd 
 |-  ( ( ph /\ t e. T ) -> ( Q ` t ) <_ 1 )
53 44 52 jca 
 |-  ( ( ph /\ t e. T ) -> ( 0 <_ ( Q ` t ) /\ ( Q ` t ) <_ 1 ) )
54 53 ex 
 |-  ( ph -> ( t e. T -> ( 0 <_ ( Q ` t ) /\ ( Q ` t ) <_ 1 ) ) )
55 2 54 ralrimi 
 |-  ( ph -> A. t e. T ( 0 <_ ( Q ` t ) /\ ( Q ` t ) <_ 1 ) )
56 3 4 10 23 31 7 17 18 11 stoweidlem24 
 |-  ( ( ph /\ t e. V ) -> ( 1 - E ) < ( Q ` t ) )
57 56 ex 
 |-  ( ph -> ( t e. V -> ( 1 - E ) < ( Q ` t ) ) )
58 2 57 ralrimi 
 |-  ( ph -> A. t e. V ( 1 - E ) < ( Q ` t ) )
59 4 5 6 7 10 11 12 17 19 stoweidlem25 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) < E )
60 59 ex 
 |-  ( ph -> ( t e. ( T \ U ) -> ( Q ` t ) < E ) )
61 2 60 ralrimi 
 |-  ( ph -> A. t e. ( T \ U ) ( Q ` t ) < E )
62 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
63 4 62 nfcxfr 
 |-  F/_ t Q
64 63 nfeq2 
 |-  F/ t y = Q
65 fveq1 
 |-  ( y = Q -> ( y ` t ) = ( Q ` t ) )
66 65 breq2d 
 |-  ( y = Q -> ( 0 <_ ( y ` t ) <-> 0 <_ ( Q ` t ) ) )
67 65 breq1d 
 |-  ( y = Q -> ( ( y ` t ) <_ 1 <-> ( Q ` t ) <_ 1 ) )
68 66 67 anbi12d 
 |-  ( y = Q -> ( ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) <-> ( 0 <_ ( Q ` t ) /\ ( Q ` t ) <_ 1 ) ) )
69 64 68 ralbid 
 |-  ( y = Q -> ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( Q ` t ) /\ ( Q ` t ) <_ 1 ) ) )
70 65 breq2d 
 |-  ( y = Q -> ( ( 1 - E ) < ( y ` t ) <-> ( 1 - E ) < ( Q ` t ) ) )
71 64 70 ralbid 
 |-  ( y = Q -> ( A. t e. V ( 1 - E ) < ( y ` t ) <-> A. t e. V ( 1 - E ) < ( Q ` t ) ) )
72 65 breq1d 
 |-  ( y = Q -> ( ( y ` t ) < E <-> ( Q ` t ) < E ) )
73 64 72 ralbid 
 |-  ( y = Q -> ( A. t e. ( T \ U ) ( y ` t ) < E <-> A. t e. ( T \ U ) ( Q ` t ) < E ) )
74 69 71 73 3anbi123d 
 |-  ( y = Q -> ( ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < E ) <-> ( A. t e. T ( 0 <_ ( Q ` t ) /\ ( Q ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( Q ` t ) /\ A. t e. ( T \ U ) ( Q ` t ) < E ) ) )
75 74 rspcev 
 |-  ( ( Q e. A /\ ( A. t e. T ( 0 <_ ( Q ` t ) /\ ( Q ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( Q ` t ) /\ A. t e. ( T \ U ) ( Q ` t ) < E ) ) -> E. y e. A ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < E ) )
76 25 55 58 61 75 syl13anc 
 |-  ( ph -> E. y e. A ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < E ) )