Metamath Proof Explorer

Theorem stoweidlem25

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

Ref Expression
Hypotheses stoweidlem25.1 
|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
stoweidlem25.2 
|- ( ph -> N e. NN )
stoweidlem25.3 
|- ( ph -> K e. NN )
stoweidlem25.4 
|- ( ph -> D e. RR+ )
stoweidlem25.6 
|- ( ph -> P : T --> RR )
stoweidlem25.7 
|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
stoweidlem25.8 
|- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
stoweidlem25.9 
|- ( ph -> E e. RR+ )
stoweidlem25.11 
|- ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )
Assertion stoweidlem25 
|- ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) < E )

Proof

Step Hyp Ref Expression
1 stoweidlem25.1 
 |-  Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
2 stoweidlem25.2 
 |-  ( ph -> N e. NN )
3 stoweidlem25.3 
 |-  ( ph -> K e. NN )
4 stoweidlem25.4 
 |-  ( ph -> D e. RR+ )
5 stoweidlem25.6 
 |-  ( ph -> P : T --> RR )
6 stoweidlem25.7 
 |-  ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
7 stoweidlem25.8 
 |-  ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
8 stoweidlem25.9 
 |-  ( ph -> E e. RR+ )
9 stoweidlem25.11 
 |-  ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )
10 eldifi 
 |-  ( t e. ( T \ U ) -> t e. T )
11 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
12 3 nnnn0d 
 |-  ( ph -> K e. NN0 )
13 1 5 11 12 stoweidlem12 
 |-  ( ( ph /\ t e. T ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
14 1red 
 |-  ( ( ph /\ t e. T ) -> 1 e. RR )
15 5 ffvelcdmda 
 |-  ( ( ph /\ t e. T ) -> ( P ` t ) e. RR )
16 11 adantr 
 |-  ( ( ph /\ t e. T ) -> N e. NN0 )
17 15 16 reexpcld 
 |-  ( ( ph /\ t e. T ) -> ( ( P ` t ) ^ N ) e. RR )
18 14 17 resubcld 
 |-  ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) e. RR )
19 3 11 nnexpcld 
 |-  ( ph -> ( K ^ N ) e. NN )
20 19 nnnn0d 
 |-  ( ph -> ( K ^ N ) e. NN0 )
21 20 adantr 
 |-  ( ( ph /\ t e. T ) -> ( K ^ N ) e. NN0 )
22 18 21 reexpcld 
 |-  ( ( ph /\ t e. T ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) e. RR )
23 13 22 eqeltrd 
 |-  ( ( ph /\ t e. T ) -> ( Q ` t ) e. RR )
24 10 23 sylan2 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) e. RR )
25 3 nnred 
 |-  ( ph -> K e. RR )
26 4 rpred 
 |-  ( ph -> D e. RR )
27 25 26 remulcld 
 |-  ( ph -> ( K x. D ) e. RR )
28 27 11 reexpcld 
 |-  ( ph -> ( ( K x. D ) ^ N ) e. RR )
29 3 nncnd 
 |-  ( ph -> K e. CC )
30 3 nnne0d 
 |-  ( ph -> K =/= 0 )
31 4 rpcnne0d 
 |-  ( ph -> ( D e. CC /\ D =/= 0 ) )
32 mulne0 
 |-  ( ( ( K e. CC /\ K =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( K x. D ) =/= 0 )
33 29 30 31 32 syl21anc 
 |-  ( ph -> ( K x. D ) =/= 0 )
34 4 rpcnd 
 |-  ( ph -> D e. CC )
35 29 34 mulcld 
 |-  ( ph -> ( K x. D ) e. CC )
36 expne0 
 |-  ( ( ( K x. D ) e. CC /\ N e. NN ) -> ( ( ( K x. D ) ^ N ) =/= 0 <-> ( K x. D ) =/= 0 ) )
37 35 2 36 syl2anc 
 |-  ( ph -> ( ( ( K x. D ) ^ N ) =/= 0 <-> ( K x. D ) =/= 0 ) )
38 33 37 mpbird 
 |-  ( ph -> ( ( K x. D ) ^ N ) =/= 0 )
39 28 38 rereccld 
 |-  ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) e. RR )
40 39 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( 1 / ( ( K x. D ) ^ N ) ) e. RR )
41 8 rpred 
 |-  ( ph -> E e. RR )
42 41 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> E e. RR )
43 10 13 sylan2 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
44 2 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> N e. NN )
45 3 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> K e. NN )
46 4 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> D e. RR+ )
47 5 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> P : T --> RR )
48 10 adantl 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> t e. T )
49 47 48 ffvelcdmd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( P ` t ) e. RR )
50 0red 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> 0 e. RR )
51 26 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> D e. RR )
52 4 rpgt0d 
 |-  ( ph -> 0 < D )
53 52 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> 0 < D )
54 7 r19.21bi 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> D <_ ( P ` t ) )
55 50 51 49 53 54 ltletrd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> 0 < ( P ` t ) )
56 49 55 elrpd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( P ` t ) e. RR+ )
57 6 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
58 rsp 
 |-  ( A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) -> ( t e. T -> ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) ) )
59 57 48 58 sylc 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
60 59 simpld 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> 0 <_ ( P ` t ) )
61 59 simprd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( P ` t ) <_ 1 )
62 44 45 46 56 60 61 54 stoweidlem1 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )
63 43 62 eqbrtrd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )
64 9 adantr 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( 1 / ( ( K x. D ) ^ N ) ) < E )
65 24 40 42 63 64 lelttrd 
 |-  ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) < E )