Metamath Proof Explorer

Theorem knoppndvlem17

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 12-Aug-2021)

Ref Expression
Hypotheses knoppndvlem17.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppndvlem17.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppndvlem17.w 
|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
knoppndvlem17.a 
|- A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
knoppndvlem17.b 
|- B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) )
knoppndvlem17.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppndvlem17.j 
|- ( ph -> J e. NN0 )
knoppndvlem17.m 
|- ( ph -> M e. ZZ )
knoppndvlem17.n 
|- ( ph -> N e. NN )
knoppndvlem17.1 
|- ( ph -> 1 < ( N x. ( abs ` C ) ) )
Assertion knoppndvlem17 
|- ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( abs ` ( ( W ` B ) - ( W ` A ) ) ) / ( B - A ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem17.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem17.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem17.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppndvlem17.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
5 knoppndvlem17.b 
 |-  B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) )
6 knoppndvlem17.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
7 knoppndvlem17.j 
 |-  ( ph -> J e. NN0 )
8 knoppndvlem17.m 
 |-  ( ph -> M e. ZZ )
9 knoppndvlem17.n 
 |-  ( ph -> N e. NN )
10 knoppndvlem17.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
11 6 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
12 11 simpld 
 |-  ( ph -> C e. RR )
13 12 recnd 
 |-  ( ph -> C e. CC )
14 13 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
15 14 7 reexpcld 
 |-  ( ph -> ( ( abs ` C ) ^ J ) e. RR )
16 2re 
 |-  2 e. RR
17 16 a1i 
 |-  ( ph -> 2 e. RR )
18 2ne0 
 |-  2 =/= 0
19 18 a1i 
 |-  ( ph -> 2 =/= 0 )
20 15 17 19 redivcld 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / 2 ) e. RR )
21 20 recnd 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / 2 ) e. CC )
22 1red 
 |-  ( ph -> 1 e. RR )
23 9 nnred 
 |-  ( ph -> N e. RR )
24 17 23 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
25 24 14 remulcld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
26 25 22 resubcld 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR )
27 0red 
 |-  ( ph -> 0 e. RR )
28 0lt1 
 |-  0 < 1
29 28 a1i 
 |-  ( ph -> 0 < 1 )
30 6 9 10 knoppndvlem12 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 /\ 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
31 30 simprd 
 |-  ( ph -> 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
32 27 22 26 29 31 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
33 26 32 jca 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR /\ 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
34 gt0ne0 
 |-  ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR /\ 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) =/= 0 )
35 33 34 syl 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) =/= 0 )
36 22 26 35 redivcld 
 |-  ( ph -> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR )
37 22 36 resubcld 
 |-  ( ph -> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR )
38 37 recnd 
 |-  ( ph -> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. CC )
39 21 38 mulcomd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) = ( ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) x. ( ( ( abs ` C ) ^ J ) / 2 ) ) )
40 39 oveq1d 
 |-  ( ph -> ( ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) x. ( ( ( abs ` C ) ^ J ) / 2 ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
41 2rp 
 |-  2 e. RR+
42 41 a1i 
 |-  ( ph -> 2 e. RR+ )
43 9 nnrpd 
 |-  ( ph -> N e. RR+ )
44 42 43 rpmulcld 
 |-  ( ph -> ( 2 x. N ) e. RR+ )
45 7 nn0zd 
 |-  ( ph -> J e. ZZ )
46 45 znegcld 
 |-  ( ph -> -u J e. ZZ )
47 44 46 rpexpcld 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. RR+ )
48 47 rphalfcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR+ )
49 48 rpcnd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. CC )
50 48 rpne0d 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) =/= 0 )
51 38 21 49 50 divassd 
 |-  ( ph -> ( ( ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) x. ( ( ( abs ` C ) ^ J ) / 2 ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) x. ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) )
52 21 49 50 divcld 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) e. CC )
53 38 52 mulcomd 
 |-  ( ph -> ( ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) x. ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) = ( ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
54 15 recnd 
 |-  ( ph -> ( ( abs ` C ) ^ J ) e. CC )
55 47 rpcnd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. CC )
56 17 recnd 
 |-  ( ph -> 2 e. CC )
57 47 rpne0d 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) =/= 0 )
58 54 55 56 57 19 divcan7d 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( abs ` C ) ^ J ) / ( ( 2 x. N ) ^ -u J ) ) )
59 24 recnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
60 44 rpne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
61 59 60 45 expnegd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) = ( 1 / ( ( 2 x. N ) ^ J ) ) )
62 61 oveq2d 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / ( ( 2 x. N ) ^ -u J ) ) = ( ( ( abs ` C ) ^ J ) / ( 1 / ( ( 2 x. N ) ^ J ) ) ) )
63 1cnd 
 |-  ( ph -> 1 e. CC )
64 59 7 expcld 
 |-  ( ph -> ( ( 2 x. N ) ^ J ) e. CC )
65 27 29 gtned 
 |-  ( ph -> 1 =/= 0 )
66 59 60 45 expne0d 
 |-  ( ph -> ( ( 2 x. N ) ^ J ) =/= 0 )
67 54 63 64 65 66 divdiv2d 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / ( 1 / ( ( 2 x. N ) ^ J ) ) ) = ( ( ( ( abs ` C ) ^ J ) x. ( ( 2 x. N ) ^ J ) ) / 1 ) )
68 54 64 mulcld 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) x. ( ( 2 x. N ) ^ J ) ) e. CC )
69 68 div1d 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) x. ( ( 2 x. N ) ^ J ) ) / 1 ) = ( ( ( abs ` C ) ^ J ) x. ( ( 2 x. N ) ^ J ) ) )
70 54 64 mulcomd 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) x. ( ( 2 x. N ) ^ J ) ) = ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) )
71 59 60 jca 
 |-  ( ph -> ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) )
72 14 recnd 
 |-  ( ph -> ( abs ` C ) e. CC )
73 6 9 10 knoppndvlem13 
 |-  ( ph -> C =/= 0 )
74 13 73 absne0d 
 |-  ( ph -> ( abs ` C ) =/= 0 )
75 72 74 jca 
 |-  ( ph -> ( ( abs ` C ) e. CC /\ ( abs ` C ) =/= 0 ) )
76 71 75 45 3jca 
 |-  ( ph -> ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) /\ ( ( abs ` C ) e. CC /\ ( abs ` C ) =/= 0 ) /\ J e. ZZ ) )
77 mulexpz 
 |-  ( ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) /\ ( ( abs ` C ) e. CC /\ ( abs ` C ) =/= 0 ) /\ J e. ZZ ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) = ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) )
78 76 77 syl 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) = ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) )
79 78 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) = ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) )
80 69 70 79 3eqtrd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) x. ( ( 2 x. N ) ^ J ) ) / 1 ) = ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) )
81 62 67 80 3eqtrd 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / ( ( 2 x. N ) ^ -u J ) ) = ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) )
82 58 81 eqtrd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) )
83 82 oveq1d 
 |-  ( ph -> ( ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) = ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
84 53 83 eqtrd 
 |-  ( ph -> ( ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) x. ( ( ( ( abs ` C ) ^ J ) / 2 ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) ) = ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
85 40 51 84 3eqtrd 
 |-  ( ph -> ( ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
86 85 eqcomd 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) = ( ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
87 20 37 remulcld 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) e. RR )
88 5 a1i 
 |-  ( ph -> B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) )
89 8 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
90 9 45 89 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) e. RR )
91 88 90 eqeltrd 
 |-  ( ph -> B e. RR )
92 11 simprd 
 |-  ( ph -> ( abs ` C ) < 1 )
93 1 2 3 91 9 12 92 knoppcld 
 |-  ( ph -> ( W ` B ) e. CC )
94 4 a1i 
 |-  ( ph -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
95 9 45 8 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )
96 94 95 eqeltrd 
 |-  ( ph -> A e. RR )
97 1 2 3 96 9 12 92 knoppcld 
 |-  ( ph -> ( W ` A ) e. CC )
98 93 97 subcld 
 |-  ( ph -> ( ( W ` B ) - ( W ` A ) ) e. CC )
99 98 abscld 
 |-  ( ph -> ( abs ` ( ( W ` B ) - ( W ` A ) ) ) e. RR )
100 1 2 3 4 5 6 7 8 9 10 knoppndvlem15 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( abs ` ( ( W ` B ) - ( W ` A ) ) ) )
101 87 99 48 100 lediv1dd 
 |-  ( ph -> ( ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) <_ ( ( abs ` ( ( W ` B ) - ( W ` A ) ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
102 86 101 eqbrtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( abs ` ( ( W ` B ) - ( W ` A ) ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
103 4 5 7 8 9 knoppndvlem16 
 |-  ( ph -> ( B - A ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
104 103 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) = ( B - A ) )
105 104 oveq2d 
 |-  ( ph -> ( ( abs ` ( ( W ` B ) - ( W ` A ) ) ) / ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( abs ` ( ( W ` B ) - ( W ` A ) ) ) / ( B - A ) ) )
106 102 105 breqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( abs ` ( ( W ` B ) - ( W ` A ) ) ) / ( B - A ) ) )