Metamath Proof Explorer

Theorem stoweidlem24

Description: This lemma proves that for n sufficiently large, q_n( t ) > ( 1 - epsilon ), for all t in V : see Lemma 1 BrosowskiDeutsh p. 90, (at the bottom of page 90). Q is used to represent q_n in the paper, N to represent n in the paper, K to represent k , D to represent δ, and E to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem24.1 
|- V = { t e. T | ( P ` t ) < ( D / 2 ) }
stoweidlem24.2 
|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
stoweidlem24.3 
|- ( ph -> P : T --> RR )
stoweidlem24.4 
|- ( ph -> N e. NN0 )
stoweidlem24.5 
|- ( ph -> K e. NN0 )
stoweidlem24.6 
|- ( ph -> D e. RR+ )
stoweidlem24.8 
|- ( ph -> E e. RR+ )
stoweidlem24.9 
|- ( ph -> ( 1 - E ) < ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) )
stoweidlem24.10 
|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
Assertion stoweidlem24 
|- ( ( ph /\ t e. V ) -> ( 1 - E ) < ( Q ` t ) )

Proof

Step Hyp Ref Expression
1 stoweidlem24.1 
 |-  V = { t e. T | ( P ` t ) < ( D / 2 ) }
2 stoweidlem24.2 
 |-  Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
3 stoweidlem24.3 
 |-  ( ph -> P : T --> RR )
4 stoweidlem24.4 
 |-  ( ph -> N e. NN0 )
5 stoweidlem24.5 
 |-  ( ph -> K e. NN0 )
6 stoweidlem24.6 
 |-  ( ph -> D e. RR+ )
7 stoweidlem24.8 
 |-  ( ph -> E e. RR+ )
8 stoweidlem24.9 
 |-  ( ph -> ( 1 - E ) < ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) )
9 stoweidlem24.10 
 |-  ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
10 1red 
 |-  ( ( ph /\ t e. V ) -> 1 e. RR )
11 7 rpred 
 |-  ( ph -> E e. RR )
12 11 adantr 
 |-  ( ( ph /\ t e. V ) -> E e. RR )
13 10 12 resubcld 
 |-  ( ( ph /\ t e. V ) -> ( 1 - E ) e. RR )
14 5 nn0red 
 |-  ( ph -> K e. RR )
15 14 adantr 
 |-  ( ( ph /\ t e. V ) -> K e. RR )
16 3 adantr 
 |-  ( ( ph /\ t e. V ) -> P : T --> RR )
17 1 rabeq2i 
 |-  ( t e. V <-> ( t e. T /\ ( P ` t ) < ( D / 2 ) ) )
18 17 simplbi 
 |-  ( t e. V -> t e. T )
19 18 adantl 
 |-  ( ( ph /\ t e. V ) -> t e. T )
20 16 19 ffvelrnd 
 |-  ( ( ph /\ t e. V ) -> ( P ` t ) e. RR )
21 15 20 remulcld 
 |-  ( ( ph /\ t e. V ) -> ( K x. ( P ` t ) ) e. RR )
22 4 adantr 
 |-  ( ( ph /\ t e. V ) -> N e. NN0 )
23 21 22 reexpcld 
 |-  ( ( ph /\ t e. V ) -> ( ( K x. ( P ` t ) ) ^ N ) e. RR )
24 10 23 resubcld 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( ( K x. ( P ` t ) ) ^ N ) ) e. RR )
25 20 22 reexpcld 
 |-  ( ( ph /\ t e. V ) -> ( ( P ` t ) ^ N ) e. RR )
26 10 25 resubcld 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( ( P ` t ) ^ N ) ) e. RR )
27 5 4 jca 
 |-  ( ph -> ( K e. NN0 /\ N e. NN0 ) )
28 27 adantr 
 |-  ( ( ph /\ t e. V ) -> ( K e. NN0 /\ N e. NN0 ) )
29 nn0expcl 
 |-  ( ( K e. NN0 /\ N e. NN0 ) -> ( K ^ N ) e. NN0 )
30 28 29 syl 
 |-  ( ( ph /\ t e. V ) -> ( K ^ N ) e. NN0 )
31 26 30 reexpcld 
 |-  ( ( ph /\ t e. V ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) e. RR )
32 1red 
 |-  ( ph -> 1 e. RR )
33 6 rpred 
 |-  ( ph -> D e. RR )
34 14 33 remulcld 
 |-  ( ph -> ( K x. D ) e. RR )
35 34 rehalfcld 
 |-  ( ph -> ( ( K x. D ) / 2 ) e. RR )
36 35 4 reexpcld 
 |-  ( ph -> ( ( ( K x. D ) / 2 ) ^ N ) e. RR )
37 32 36 resubcld 
 |-  ( ph -> ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) e. RR )
38 37 adantr 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) e. RR )
39 8 adantr 
 |-  ( ( ph /\ t e. V ) -> ( 1 - E ) < ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) )
40 36 adantr 
 |-  ( ( ph /\ t e. V ) -> ( ( ( K x. D ) / 2 ) ^ N ) e. RR )
41 35 adantr 
 |-  ( ( ph /\ t e. V ) -> ( ( K x. D ) / 2 ) e. RR )
42 5 nn0ge0d 
 |-  ( ph -> 0 <_ K )
43 14 42 jca 
 |-  ( ph -> ( K e. RR /\ 0 <_ K ) )
44 43 adantr 
 |-  ( ( ph /\ t e. V ) -> ( K e. RR /\ 0 <_ K ) )
45 9 r19.21bi 
 |-  ( ( ph /\ t e. T ) -> ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
46 45 simpld 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( P ` t ) )
47 18 46 sylan2 
 |-  ( ( ph /\ t e. V ) -> 0 <_ ( P ` t ) )
48 mulge0 
 |-  ( ( ( K e. RR /\ 0 <_ K ) /\ ( ( P ` t ) e. RR /\ 0 <_ ( P ` t ) ) ) -> 0 <_ ( K x. ( P ` t ) ) )
49 44 20 47 48 syl12anc 
 |-  ( ( ph /\ t e. V ) -> 0 <_ ( K x. ( P ` t ) ) )
50 33 rehalfcld 
 |-  ( ph -> ( D / 2 ) e. RR )
51 50 adantr 
 |-  ( ( ph /\ t e. V ) -> ( D / 2 ) e. RR )
52 17 simprbi 
 |-  ( t e. V -> ( P ` t ) < ( D / 2 ) )
53 52 adantl 
 |-  ( ( ph /\ t e. V ) -> ( P ` t ) < ( D / 2 ) )
54 20 51 53 ltled 
 |-  ( ( ph /\ t e. V ) -> ( P ` t ) <_ ( D / 2 ) )
55 lemul2a 
 |-  ( ( ( ( P ` t ) e. RR /\ ( D / 2 ) e. RR /\ ( K e. RR /\ 0 <_ K ) ) /\ ( P ` t ) <_ ( D / 2 ) ) -> ( K x. ( P ` t ) ) <_ ( K x. ( D / 2 ) ) )
56 20 51 44 54 55 syl31anc 
 |-  ( ( ph /\ t e. V ) -> ( K x. ( P ` t ) ) <_ ( K x. ( D / 2 ) ) )
57 5 nn0cnd 
 |-  ( ph -> K e. CC )
58 57 adantr 
 |-  ( ( ph /\ t e. V ) -> K e. CC )
59 6 rpcnd 
 |-  ( ph -> D e. CC )
60 59 adantr 
 |-  ( ( ph /\ t e. V ) -> D e. CC )
61 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
62 61 a1i 
 |-  ( ( ph /\ t e. V ) -> ( 2 e. CC /\ 2 =/= 0 ) )
63 divass 
 |-  ( ( K e. CC /\ D e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( K x. D ) / 2 ) = ( K x. ( D / 2 ) ) )
64 58 60 62 63 syl3anc 
 |-  ( ( ph /\ t e. V ) -> ( ( K x. D ) / 2 ) = ( K x. ( D / 2 ) ) )
65 56 64 breqtrrd 
 |-  ( ( ph /\ t e. V ) -> ( K x. ( P ` t ) ) <_ ( ( K x. D ) / 2 ) )
66 leexp1a 
 |-  ( ( ( ( K x. ( P ` t ) ) e. RR /\ ( ( K x. D ) / 2 ) e. RR /\ N e. NN0 ) /\ ( 0 <_ ( K x. ( P ` t ) ) /\ ( K x. ( P ` t ) ) <_ ( ( K x. D ) / 2 ) ) ) -> ( ( K x. ( P ` t ) ) ^ N ) <_ ( ( ( K x. D ) / 2 ) ^ N ) )
67 21 41 22 49 65 66 syl32anc 
 |-  ( ( ph /\ t e. V ) -> ( ( K x. ( P ` t ) ) ^ N ) <_ ( ( ( K x. D ) / 2 ) ^ N ) )
68 23 40 10 67 lesub2dd 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) <_ ( 1 - ( ( K x. ( P ` t ) ) ^ N ) ) )
69 13 38 24 39 68 ltletrd 
 |-  ( ( ph /\ t e. V ) -> ( 1 - E ) < ( 1 - ( ( K x. ( P ` t ) ) ^ N ) ) )
70 20 recnd 
 |-  ( ( ph /\ t e. V ) -> ( P ` t ) e. CC )
71 58 70 22 mulexpd 
 |-  ( ( ph /\ t e. V ) -> ( ( K x. ( P ` t ) ) ^ N ) = ( ( K ^ N ) x. ( ( P ` t ) ^ N ) ) )
72 71 eqcomd 
 |-  ( ( ph /\ t e. V ) -> ( ( K ^ N ) x. ( ( P ` t ) ^ N ) ) = ( ( K x. ( P ` t ) ) ^ N ) )
73 72 oveq2d 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( ( K ^ N ) x. ( ( P ` t ) ^ N ) ) ) = ( 1 - ( ( K x. ( P ` t ) ) ^ N ) ) )
74 18 45 sylan2 
 |-  ( ( ph /\ t e. V ) -> ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
75 74 simprd 
 |-  ( ( ph /\ t e. V ) -> ( P ` t ) <_ 1 )
76 exple1 
 |-  ( ( ( ( P ` t ) e. RR /\ 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) /\ N e. NN0 ) -> ( ( P ` t ) ^ N ) <_ 1 )
77 20 47 75 22 76 syl31anc 
 |-  ( ( ph /\ t e. V ) -> ( ( P ` t ) ^ N ) <_ 1 )
78 stoweidlem10 
 |-  ( ( ( ( P ` t ) ^ N ) e. RR /\ ( K ^ N ) e. NN0 /\ ( ( P ` t ) ^ N ) <_ 1 ) -> ( 1 - ( ( K ^ N ) x. ( ( P ` t ) ^ N ) ) ) <_ ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
79 25 30 77 78 syl3anc 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( ( K ^ N ) x. ( ( P ` t ) ^ N ) ) ) <_ ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
80 73 79 eqbrtrrd 
 |-  ( ( ph /\ t e. V ) -> ( 1 - ( ( K x. ( P ` t ) ) ^ N ) ) <_ ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
81 13 24 31 69 80 ltletrd 
 |-  ( ( ph /\ t e. V ) -> ( 1 - E ) < ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
82 2 3 4 5 stoweidlem12 
 |-  ( ( ph /\ t e. T ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
83 18 82 sylan2 
 |-  ( ( ph /\ t e. V ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
84 81 83 breqtrrd 
 |-  ( ( ph /\ t e. V ) -> ( 1 - E ) < ( Q ` t ) )