Metamath Proof Explorer

Theorem knoppndvlem21

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

Ref Expression
Hypotheses knoppndvlem21.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppndvlem21.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppndvlem21.w 
|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
knoppndvlem21.g 
|- G = ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
knoppndvlem21.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppndvlem21.d 
|- ( ph -> D e. RR+ )
knoppndvlem21.e 
|- ( ph -> E e. RR+ )
knoppndvlem21.h 
|- ( ph -> H e. RR )
knoppndvlem21.j 
|- ( ph -> J e. NN0 )
knoppndvlem21.n 
|- ( ph -> N e. NN )
knoppndvlem21.1 
|- ( ph -> 1 < ( N x. ( abs ` C ) ) )
knoppndvlem21.2 
|- ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) < D )
knoppndvlem21.3 
|- ( ph -> E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) )
Assertion knoppndvlem21 
|- ( 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 knoppndvlem21.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem21.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem21.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppndvlem21.g 
 |-  G = ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
5 knoppndvlem21.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
6 knoppndvlem21.d 
 |-  ( ph -> D e. RR+ )
7 knoppndvlem21.e 
 |-  ( ph -> E e. RR+ )
8 knoppndvlem21.h 
 |-  ( ph -> H e. RR )
9 knoppndvlem21.j 
 |-  ( ph -> J e. NN0 )
10 knoppndvlem21.n 
 |-  ( ph -> N e. NN )
11 knoppndvlem21.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
12 knoppndvlem21.2 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) < D )
13 knoppndvlem21.3 
 |-  ( ph -> E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) )
14 eqid 
 |-  ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m )
15 eqid 
 |-  ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) )
16 14 15 9 8 10 knoppndvlem19 
 |-  ( ph -> E. m e. ZZ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) )
17 2re 
 |-  2 e. RR
18 17 a1i 
 |-  ( ph -> 2 e. RR )
19 10 nnred 
 |-  ( ph -> N e. RR )
20 18 19 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
21 2pos 
 |-  0 < 2
22 21 a1i 
 |-  ( ph -> 0 < 2 )
23 10 nngt0d 
 |-  ( ph -> 0 < N )
24 18 19 22 23 mulgt0d 
 |-  ( ph -> 0 < ( 2 x. N ) )
25 24 gt0ne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
26 9 nn0zd 
 |-  ( ph -> J e. ZZ )
27 26 znegcld 
 |-  ( ph -> -u J e. ZZ )
28 20 25 27 reexpclzd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. RR )
29 28 rehalfcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR )
30 29 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR )
31 simpr 
 |-  ( ( ph /\ m e. ZZ ) -> m e. ZZ )
32 31 zred 
 |-  ( ( ph /\ m e. ZZ ) -> m e. RR )
33 30 32 remulcld 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) e. RR )
34 33 adantrr 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) e. RR )
35 peano2re 
 |-  ( m e. RR -> ( m + 1 ) e. RR )
36 32 35 syl 
 |-  ( ( ph /\ m e. ZZ ) -> ( m + 1 ) e. RR )
37 30 36 jca 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR /\ ( m + 1 ) e. RR ) )
38 remulcl 
 |-  ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR /\ ( m + 1 ) e. RR ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) e. RR )
39 37 38 syl 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) e. RR )
40 39 adantrr 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) e. RR )
41 simprr 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) )
42 9 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> J e. NN0 )
43 10 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> N e. NN )
44 14 15 42 31 43 knoppndvlem16 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
45 12 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) < D )
46 44 45 eqbrtrd 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D )
47 20 27 24 3jca 
 |-  ( ph -> ( ( 2 x. N ) e. RR /\ -u J e. ZZ /\ 0 < ( 2 x. N ) ) )
48 expgt0 
 |-  ( ( ( 2 x. N ) e. RR /\ -u J e. ZZ /\ 0 < ( 2 x. N ) ) -> 0 < ( ( 2 x. N ) ^ -u J ) )
49 47 48 syl 
 |-  ( ph -> 0 < ( ( 2 x. N ) ^ -u J ) )
50 28 18 49 22 divgt0d 
 |-  ( ph -> 0 < ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
51 50 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> 0 < ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
52 44 eqcomd 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) = ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) )
53 51 52 breqtrd 
 |-  ( ( ph /\ m e. ZZ ) -> 0 < ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) )
54 33 39 posdifd 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) < ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) <-> 0 < ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
55 53 54 mpbird 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) < ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) )
56 33 55 ltned 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) )
57 46 56 jca 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) )
58 57 adantrr 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) ) -> ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) )
59 7 rpred 
 |-  ( ph -> E e. RR )
60 59 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> E e. RR )
61 5 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
62 61 simpld 
 |-  ( ph -> C e. RR )
63 62 recnd 
 |-  ( ph -> C e. CC )
64 63 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
65 20 64 remulcld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
66 65 9 reexpcld 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) e. RR )
67 4 a1i 
 |-  ( ph -> G = ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
68 5 10 11 knoppndvlem20 
 |-  ( ph -> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR+ )
69 68 rpred 
 |-  ( ph -> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR )
70 67 69 eqeltrd 
 |-  ( ph -> G e. RR )
71 66 70 remulcld 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) e. RR )
72 71 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) e. RR )
73 62 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> C e. RR )
74 61 simprd 
 |-  ( ph -> ( abs ` C ) < 1 )
75 74 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> ( abs ` C ) < 1 )
76 1 2 3 39 43 73 75 knoppcld 
 |-  ( ( ph /\ m e. ZZ ) -> ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) e. CC )
77 1 2 3 33 43 73 75 knoppcld 
 |-  ( ( ph /\ m e. ZZ ) -> ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) e. CC )
78 76 77 subcld 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) e. CC )
79 78 abscld 
 |-  ( ( ph /\ m e. ZZ ) -> ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) e. RR )
80 44 30 eqeltrd 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) e. RR )
81 53 gt0ne0d 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) =/= 0 )
82 79 80 81 redivcld 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) e. RR )
83 13 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> E <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) )
84 4 oveq2i 
 |-  ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) = ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
85 84 a1i 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) = ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
86 5 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> C e. ( -u 1 (,) 1 ) )
87 11 adantr 
 |-  ( ( ph /\ m e. ZZ ) -> 1 < ( N x. ( abs ` C ) ) )
88 1 2 3 14 15 86 42 31 43 87 knoppndvlem17 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
89 85 88 eqbrtrd 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. G ) <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
90 60 72 82 83 89 letrd 
 |-  ( ( ph /\ m e. ZZ ) -> E <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
91 90 adantrr 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) ) -> E <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
92 41 58 91 3jca 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) ) -> ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ E <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) )
93 34 40 92 3jca 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) e. RR /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) e. RR /\ ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ E <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) ) )
94 breq1 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( a <_ H <-> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H ) )
95 94 anbi1d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( ( a <_ H /\ H <_ b ) <-> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ b ) ) )
96 oveq2 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( b - a ) = ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) )
97 96 breq1d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( ( b - a ) < D <-> ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D ) )
98 neeq1 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( a =/= b <-> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= b ) )
99 97 98 anbi12d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( ( ( b - a ) < D /\ a =/= b ) <-> ( ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= b ) ) )
100 fveq2 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( W ` a ) = ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) )
101 100 oveq2d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( ( W ` b ) - ( W ` a ) ) = ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
102 101 fveq2d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( abs ` ( ( W ` b ) - ( W ` a ) ) ) = ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) )
103 102 96 oveq12d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) = ( ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
104 103 breq2d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( E <_ ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) <-> E <_ ( ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) )
105 95 99 104 3anbi123d 
 |-  ( a = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) -> ( ( ( a <_ H /\ H <_ b ) /\ ( ( b - a ) < D /\ a =/= b ) /\ E <_ ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) ) <-> ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ b ) /\ ( ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= b ) /\ E <_ ( ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) ) )
106 breq2 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( H <_ b <-> H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) )
107 106 anbi2d 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ b ) <-> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) )
108 oveq1 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) = ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) )
109 108 breq1d 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D <-> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D ) )
110 neeq2 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= b <-> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) )
111 109 110 anbi12d 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( ( ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= b ) <-> ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) ) )
112 fveq2 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( W ` b ) = ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) )
113 112 fvoveq1d 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) = ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) )
114 113 108 oveq12d 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) = ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) )
115 114 breq2d 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( E <_ ( ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) <-> E <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) )
116 107 111 115 3anbi123d 
 |-  ( b = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) -> ( ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ b ) /\ ( ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= b ) /\ E <_ ( ( abs ` ( ( W ` b ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( b - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) <-> ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ E <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) ) )
117 105 116 rspc2ev 
 |-  ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) e. RR /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) e. RR /\ ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ ( ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) < D /\ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) =/= ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) /\ E <_ ( ( abs ` ( ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) ) - ( W ` ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) / ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) ) ) ) ) -> 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 ) ) ) )
118 93 117 syl 
 |-  ( ( ph /\ ( m e. ZZ /\ ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. m ) <_ H /\ H <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( m + 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 ) ) ) )
119 16 118 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 ) ) ) )