Metamath Proof Explorer

Theorem stoweidlem49

Description: 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 . Here y is used to represent the final q_n in the paper (the one with n large enough), N represents n in the paper, K represents k , D represents δ, E represents ε, and P represents p . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem49.1 
|- F/_ t P
stoweidlem49.2 
|- F/ t ph
stoweidlem49.3 
|- V = { t e. T | ( P ` t ) < ( D / 2 ) }
stoweidlem49.4 
|- ( ph -> D e. RR+ )
stoweidlem49.5 
|- ( ph -> D < 1 )
stoweidlem49.6 
|- ( ph -> P e. A )
stoweidlem49.7 
|- ( ph -> P : T --> RR )
stoweidlem49.8 
|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
stoweidlem49.9 
|- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
stoweidlem49.10 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem49.11 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem49.12 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem49.13 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem49.14 
|- ( ph -> E e. RR+ )
Assertion stoweidlem49 
|- ( 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 stoweidlem49.1 
 |-  F/_ t P
2 stoweidlem49.2 
 |-  F/ t ph
3 stoweidlem49.3 
 |-  V = { t e. T | ( P ` t ) < ( D / 2 ) }
4 stoweidlem49.4 
 |-  ( ph -> D e. RR+ )
5 stoweidlem49.5 
 |-  ( ph -> D < 1 )
6 stoweidlem49.6 
 |-  ( ph -> P e. A )
7 stoweidlem49.7 
 |-  ( ph -> P : T --> RR )
8 stoweidlem49.8 
 |-  ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
9 stoweidlem49.9 
 |-  ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
10 stoweidlem49.10 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
11 stoweidlem49.11 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
12 stoweidlem49.12 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
13 stoweidlem49.13 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
14 stoweidlem49.14 
 |-  ( ph -> E e. RR+ )
15 breq2 
 |-  ( j = i -> ( ( 1 / D ) < j <-> ( 1 / D ) < i ) )
16 15 cbvrabv 
 |-  { j e. NN | ( 1 / D ) < j } = { i e. NN | ( 1 / D ) < i }
17 16 4 5 stoweidlem14 
 |-  ( ph -> E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) )
18 eqid 
 |-  ( i e. NN0 |-> ( ( 1 / ( k x. D ) ) ^ i ) ) = ( i e. NN0 |-> ( ( 1 / ( k x. D ) ) ^ i ) )
19 eqid 
 |-  ( i e. NN0 |-> ( ( ( k x. D ) / 2 ) ^ i ) ) = ( i e. NN0 |-> ( ( ( k x. D ) / 2 ) ^ i ) )
20 nnre 
 |-  ( k e. NN -> k e. RR )
21 20 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. RR )
22 4 rpred 
 |-  ( ph -> D e. RR )
23 22 adantr 
 |-  ( ( ph /\ k e. NN ) -> D e. RR )
24 21 23 remulcld 
 |-  ( ( ph /\ k e. NN ) -> ( k x. D ) e. RR )
25 24 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> ( k x. D ) e. RR )
26 simprl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> 1 < ( k x. D ) )
27 24 rehalfcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( k x. D ) / 2 ) e. RR )
28 nngt0 
 |-  ( k e. NN -> 0 < k )
29 28 adantl 
 |-  ( ( ph /\ k e. NN ) -> 0 < k )
30 4 rpgt0d 
 |-  ( ph -> 0 < D )
31 30 adantr 
 |-  ( ( ph /\ k e. NN ) -> 0 < D )
32 21 23 29 31 mulgt0d 
 |-  ( ( ph /\ k e. NN ) -> 0 < ( k x. D ) )
33 2re 
 |-  2 e. RR
34 2pos 
 |-  0 < 2
35 33 34 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
36 35 a1i 
 |-  ( ( ph /\ k e. NN ) -> ( 2 e. RR /\ 0 < 2 ) )
37 divgt0 
 |-  ( ( ( ( k x. D ) e. RR /\ 0 < ( k x. D ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( ( k x. D ) / 2 ) )
38 24 32 36 37 syl21anc 
 |-  ( ( ph /\ k e. NN ) -> 0 < ( ( k x. D ) / 2 ) )
39 27 38 elrpd 
 |-  ( ( ph /\ k e. NN ) -> ( ( k x. D ) / 2 ) e. RR+ )
40 39 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> ( ( k x. D ) / 2 ) e. RR+ )
41 simprr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> ( ( k x. D ) / 2 ) < 1 )
42 14 ad2antrr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> E e. RR+ )
43 18 19 25 26 40 41 42 stoweidlem7 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) )
44 43 ex 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) -> E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) )
45 44 reximdva 
 |-  ( ph -> ( E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) -> E. k e. NN E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) )
46 17 45 mpd 
 |-  ( ph -> E. k e. NN E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) )
47 nfv 
 |-  F/ t ( k e. NN /\ n e. NN )
48 2 47 nfan 
 |-  F/ t ( ph /\ ( k e. NN /\ n e. NN ) )
49 nfv 
 |-  F/ t ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E )
50 48 49 nfan 
 |-  F/ t ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) )
51 eqid 
 |-  ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ n ) ) ^ ( k ^ n ) ) ) = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ n ) ) ^ ( k ^ n ) ) )
52 simplrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> n e. NN )
53 simplrl 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> k e. NN )
54 4 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> D e. RR+ )
55 5 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> D < 1 )
56 6 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> P e. A )
57 7 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> P : T --> RR )
58 8 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
59 9 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> A. t e. ( T \ U ) D <_ ( P ` t ) )
60 10 ad4ant14 
 |-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A ) -> f : T --> RR )
61 simp1ll 
 |-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A /\ g e. A ) -> ph )
62 61 11 syld3an1 
 |-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
63 61 12 syld3an1 
 |-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
64 13 ad4ant14 
 |-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ x e. RR ) -> ( t e. T |-> x ) e. A )
65 14 ad2antrr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> E e. RR+ )
66 simprl 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) )
67 simprr 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> ( 1 / ( ( k x. D ) ^ n ) ) < E )
68 1 50 3 51 52 53 54 55 56 57 58 59 60 62 63 64 65 66 67 stoweidlem45 
 |-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < 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 ) )
69 68 ex 
 |-  ( ( ph /\ ( k e. NN /\ n e. NN ) ) -> ( ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < 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 ) ) )
70 69 rexlimdvva 
 |-  ( ph -> ( E. k e. NN E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < 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 ) ) )
71 46 70 mpd 
 |-  ( 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 ) )