Metamath Proof Explorer

Theorem knoppndvlem22

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

Ref Expression
Hypotheses knoppndvlem22.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppndvlem22.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppndvlem22.w 
|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
knoppndvlem22.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppndvlem22.d 
|- ( ph -> D e. RR+ )
knoppndvlem22.e 
|- ( ph -> E e. RR+ )
knoppndvlem22.h 
|- ( ph -> H e. RR )
knoppndvlem22.n 
|- ( ph -> N e. NN )
knoppndvlem22.1 
|- ( ph -> 1 < ( N x. ( abs ` C ) ) )
Assertion knoppndvlem22 
|- ( ph -> E. a e. RR E. b e. RR ( ( a <_ H /\ H <_ b ) /\ ( ( b - a ) < D /\ a =/= b ) /\ E <_ ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem22.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem22.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem22.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppndvlem22.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
5 knoppndvlem22.d 
 |-  ( ph -> D e. RR+ )
6 knoppndvlem22.e 
 |-  ( ph -> E e. RR+ )
7 knoppndvlem22.h 
 |-  ( ph -> H e. RR )
8 knoppndvlem22.n 
 |-  ( ph -> N e. NN )
9 knoppndvlem22.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
10 4 8 9 knoppndvlem20 
 |-  ( ph -> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR+ )
11 4 8 5 6 10 9 knoppndvlem18 
 |-  ( ph -> E. j e. NN0 ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) )
12 eqid 
 |-  ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) = ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
13 4 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> C e. ( -u 1 (,) 1 ) )
14 5 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> D e. RR+ )
15 6 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> E e. RR+ )
16 7 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> H e. RR )
17 simprl 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> j e. NN0 )
18 8 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> N e. NN )
19 9 adantr 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> 1 < ( N x. ( abs ` C ) ) )
20 simprrl 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D )
21 simprrr 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
22 1 2 3 12 13 14 15 16 17 18 19 20 21 knoppndvlem21 
 |-  ( ( ph /\ ( j e. NN0 /\ ( ( ( ( 2 x. N ) ^ -u j ) / 2 ) < D /\ E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ j ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) ) ) ) -> E. a e. RR E. b e. RR ( ( a <_ H /\ H <_ b ) /\ ( ( b - a ) < D /\ a =/= b ) /\ E <_ ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) ) )
23 11 22 rexlimddv 
 |-  ( ph -> E. a e. RR E. b e. RR ( ( a <_ H /\ H <_ b ) /\ ( ( b - a ) < D /\ a =/= b ) /\ E <_ ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) ) )