Metamath Proof Explorer

Theorem knoppcnlem4

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppcnlem4.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppcnlem4.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppcnlem4.n 
|- ( ph -> N e. NN )
knoppcnlem4.1 
|- ( ph -> C e. RR )
knoppcnlem4.2 
|- ( ph -> A e. RR )
knoppcnlem4.3 
|- ( ph -> M e. NN0 )
Assertion knoppcnlem4 
|- ( ph -> ( abs ` ( ( F ` A ) ` M ) ) <_ ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` M ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem4.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem4.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem4.n 
 |-  ( ph -> N e. NN )
4 knoppcnlem4.1 
 |-  ( ph -> C e. RR )
5 knoppcnlem4.2 
 |-  ( ph -> A e. RR )
6 knoppcnlem4.3 
 |-  ( ph -> M e. NN0 )
7 2 5 6 knoppcnlem1 
 |-  ( ph -> ( ( F ` A ) ` M ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
8 7 fveq2d 
 |-  ( ph -> ( abs ` ( ( F ` A ) ` M ) ) = ( abs ` ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) )
9 4 recnd 
 |-  ( ph -> C e. CC )
10 9 6 expcld 
 |-  ( ph -> ( C ^ M ) e. CC )
11 2re 
 |-  2 e. RR
12 11 a1i 
 |-  ( ph -> 2 e. RR )
13 nnre 
 |-  ( N e. NN -> N e. RR )
14 3 13 syl 
 |-  ( ph -> N e. RR )
15 12 14 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
16 15 6 reexpcld 
 |-  ( ph -> ( ( 2 x. N ) ^ M ) e. RR )
17 16 5 remulcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ M ) x. A ) e. RR )
18 1 17 dnicld2 
 |-  ( ph -> ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) e. RR )
19 18 recnd 
 |-  ( ph -> ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) e. CC )
20 10 19 absmuld 
 |-  ( ph -> ( abs ` ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) = ( ( abs ` ( C ^ M ) ) x. ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) )
21 9 6 absexpd 
 |-  ( ph -> ( abs ` ( C ^ M ) ) = ( ( abs ` C ) ^ M ) )
22 21 oveq1d 
 |-  ( ph -> ( ( abs ` ( C ^ M ) ) x. ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) = ( ( ( abs ` C ) ^ M ) x. ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) )
23 20 22 eqtrd 
 |-  ( ph -> ( abs ` ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) = ( ( ( abs ` C ) ^ M ) x. ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) )
24 19 abscld 
 |-  ( ph -> ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) e. RR )
25 1red 
 |-  ( ph -> 1 e. RR )
26 9 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
27 26 6 reexpcld 
 |-  ( ph -> ( ( abs ` C ) ^ M ) e. RR )
28 9 absge0d 
 |-  ( ph -> 0 <_ ( abs ` C ) )
29 26 6 28 expge0d 
 |-  ( ph -> 0 <_ ( ( abs ` C ) ^ M ) )
30 1 dnival 
 |-  ( ( ( ( 2 x. N ) ^ M ) x. A ) e. RR -> ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) = ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
31 17 30 syl 
 |-  ( ph -> ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) = ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
32 31 fveq2d 
 |-  ( ph -> ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) = ( abs ` ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) )
33 halfre 
 |-  ( 1 / 2 ) e. RR
34 33 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
35 17 34 readdcld 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) e. RR )
36 reflcl 
 |-  ( ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) e. RR -> ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) e. RR )
37 35 36 syl 
 |-  ( ph -> ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) e. RR )
38 37 17 resubcld 
 |-  ( ph -> ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) e. RR )
39 38 recnd 
 |-  ( ph -> ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) e. CC )
40 absidm 
 |-  ( ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) e. CC -> ( abs ` ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) = ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
41 39 40 syl 
 |-  ( ph -> ( abs ` ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) = ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
42 32 41 eqtrd 
 |-  ( ph -> ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) = ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
43 31 18 eqeltrrd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) e. RR )
44 rddif 
 |-  ( ( ( ( 2 x. N ) ^ M ) x. A ) e. RR -> ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) <_ ( 1 / 2 ) )
45 17 44 syl 
 |-  ( ph -> ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) <_ ( 1 / 2 ) )
46 halflt1 
 |-  ( 1 / 2 ) < 1
47 1re 
 |-  1 e. RR
48 33 47 ltlei 
 |-  ( ( 1 / 2 ) < 1 -> ( 1 / 2 ) <_ 1 )
49 46 48 ax-mp 
 |-  ( 1 / 2 ) <_ 1
50 49 a1i 
 |-  ( ph -> ( 1 / 2 ) <_ 1 )
51 43 34 25 45 50 letrd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( ( ( ( 2 x. N ) ^ M ) x. A ) + ( 1 / 2 ) ) ) - ( ( ( 2 x. N ) ^ M ) x. A ) ) ) <_ 1 )
52 42 51 eqbrtrd 
 |-  ( ph -> ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) <_ 1 )
53 24 25 27 29 52 lemul2ad 
 |-  ( ph -> ( ( ( abs ` C ) ^ M ) x. ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) <_ ( ( ( abs ` C ) ^ M ) x. 1 ) )
54 ax-1rid 
 |-  ( ( ( abs ` C ) ^ M ) e. RR -> ( ( ( abs ` C ) ^ M ) x. 1 ) = ( ( abs ` C ) ^ M ) )
55 27 54 syl 
 |-  ( ph -> ( ( ( abs ` C ) ^ M ) x. 1 ) = ( ( abs ` C ) ^ M ) )
56 53 55 breqtrd 
 |-  ( ph -> ( ( ( abs ` C ) ^ M ) x. ( abs ` ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) <_ ( ( abs ` C ) ^ M ) )
57 23 56 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) <_ ( ( abs ` C ) ^ M ) )
58 eqidd 
 |-  ( ph -> ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) = ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) )
59 oveq2 
 |-  ( m = M -> ( ( abs ` C ) ^ m ) = ( ( abs ` C ) ^ M ) )
60 59 adantl 
 |-  ( ( ph /\ m = M ) -> ( ( abs ` C ) ^ m ) = ( ( abs ` C ) ^ M ) )
61 58 60 6 27 fvmptd 
 |-  ( ph -> ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` M ) = ( ( abs ` C ) ^ M ) )
62 61 eqcomd 
 |-  ( ph -> ( ( abs ` C ) ^ M ) = ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` M ) )
63 57 62 breqtrd 
 |-  ( ph -> ( abs ` ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) ) <_ ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` M ) )
64 8 63 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( F ` A ) ` M ) ) <_ ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` M ) )