Metamath Proof Explorer

Theorem knoppndvlem14

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 1-Jul-2021) (Revised by Asger C. Ipsen, 7-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 knoppndvlem14.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem14.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem14.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
4 knoppndvlem14.b 
 |-  B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) )
5 knoppndvlem14.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
6 knoppndvlem14.j 
 |-  ( ph -> J e. NN0 )
7 knoppndvlem14.m 
 |-  ( ph -> M e. ZZ )
8 knoppndvlem14.n 
 |-  ( ph -> N e. NN )
9 knoppndvlem14.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
10 4 a1i 
 |-  ( ph -> B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) )
11 6 nn0zd 
 |-  ( ph -> J e. ZZ )
12 7 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
13 8 11 12 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) e. RR )
14 10 13 eqeltrd 
 |-  ( ph -> B e. RR )
15 5 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
16 15 simpld 
 |-  ( ph -> C e. RR )
17 1 2 14 16 8 knoppndvlem5 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) e. RR )
18 3 a1i 
 |-  ( ph -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
19 8 11 7 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )
20 18 19 eqeltrd 
 |-  ( ph -> A e. RR )
21 1 2 20 16 8 knoppndvlem5 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) e. RR )
22 17 21 resubcld 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) e. RR )
23 22 recnd 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) e. CC )
24 23 abscld 
 |-  ( ph -> ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) e. RR )
25 14 20 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
26 25 recnd 
 |-  ( ph -> ( B - A ) e. CC )
27 26 abscld 
 |-  ( ph -> ( abs ` ( B - A ) ) e. RR )
28 fzfid 
 |-  ( ph -> ( 0 ... ( J - 1 ) ) e. Fin )
29 2re 
 |-  2 e. RR
30 29 a1i 
 |-  ( ph -> 2 e. RR )
31 nnre 
 |-  ( N e. NN -> N e. RR )
32 8 31 syl 
 |-  ( ph -> N e. RR )
33 30 32 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
34 16 recnd 
 |-  ( ph -> C e. CC )
35 34 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
36 33 35 remulcld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
37 36 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
38 elfznn0 
 |-  ( i e. ( 0 ... ( J - 1 ) ) -> i e. NN0 )
39 38 adantl 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> i e. NN0 )
40 37 39 reexpcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) e. RR )
41 28 40 fsumrecl 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) e. RR )
42 27 41 remulcld 
 |-  ( ph -> ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) e. RR )
43 35 6 reexpcld 
 |-  ( ph -> ( ( abs ` C ) ^ J ) e. RR )
44 2ne0 
 |-  2 =/= 0
45 44 a1i 
 |-  ( ph -> 2 =/= 0 )
46 43 30 45 redivcld 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / 2 ) e. RR )
47 1red 
 |-  ( ph -> 1 e. RR )
48 36 47 resubcld 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR )
49 0red 
 |-  ( ph -> 0 e. RR )
50 0lt1 
 |-  0 < 1
51 50 a1i 
 |-  ( ph -> 0 < 1 )
52 5 8 9 knoppndvlem12 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 /\ 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
53 52 simprd 
 |-  ( ph -> 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
54 49 47 48 51 53 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
55 49 54 jca 
 |-  ( ph -> ( 0 e. RR /\ 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
56 ltne 
 |-  ( ( 0 e. RR /\ 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) =/= 0 )
57 55 56 syl 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) =/= 0 )
58 47 48 57 redivcld 
 |-  ( ph -> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR )
59 46 58 remulcld 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR )
60 1 2 20 14 5 6 8 knoppndvlem11 
 |-  ( ph -> ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) <_ ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
61 10 18 oveq12d 
 |-  ( ph -> ( B - A ) = ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
62 30 recnd 
 |-  ( ph -> 2 e. CC )
63 32 recnd 
 |-  ( ph -> N e. CC )
64 nnge1 
 |-  ( N e. NN -> 1 <_ N )
65 8 64 syl 
 |-  ( ph -> 1 <_ N )
66 49 47 32 51 65 ltletrd 
 |-  ( ph -> 0 < N )
67 49 66 jca 
 |-  ( ph -> ( 0 e. RR /\ 0 < N ) )
68 ltne 
 |-  ( ( 0 e. RR /\ 0 < N ) -> N =/= 0 )
69 67 68 syl 
 |-  ( ph -> N =/= 0 )
70 62 63 45 69 mulne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
71 11 znegcld 
 |-  ( ph -> -u J e. ZZ )
72 33 70 71 reexpclzd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. RR )
73 72 30 45 redivcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR )
74 73 recnd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. CC )
75 12 zcnd 
 |-  ( ph -> ( M + 1 ) e. CC )
76 7 zcnd 
 |-  ( ph -> M e. CC )
77 74 75 76 subdid 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( M + 1 ) - M ) ) = ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
78 77 eqcomd 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( M + 1 ) - M ) ) )
79 1cnd 
 |-  ( ph -> 1 e. CC )
80 76 79 pncan2d 
 |-  ( ph -> ( ( M + 1 ) - M ) = 1 )
81 80 oveq2d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( M + 1 ) - M ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. 1 ) )
82 74 mulid1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. 1 ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
83 78 81 82 3eqtrd 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
84 61 83 eqtrd 
 |-  ( ph -> ( B - A ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
85 84 fveq2d 
 |-  ( ph -> ( abs ` ( B - A ) ) = ( abs ` ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
86 72 recnd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. CC )
87 86 62 45 absdivd 
 |-  ( ph -> ( abs ` ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( abs ` ( ( 2 x. N ) ^ -u J ) ) / ( abs ` 2 ) ) )
88 62 63 mulcld 
 |-  ( ph -> ( 2 x. N ) e. CC )
89 88 70 71 3jca 
 |-  ( ph -> ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 /\ -u J e. ZZ ) )
90 absexpz 
 |-  ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 /\ -u J e. ZZ ) -> ( abs ` ( ( 2 x. N ) ^ -u J ) ) = ( ( abs ` ( 2 x. N ) ) ^ -u J ) )
91 89 90 syl 
 |-  ( ph -> ( abs ` ( ( 2 x. N ) ^ -u J ) ) = ( ( abs ` ( 2 x. N ) ) ^ -u J ) )
92 62 63 absmuld 
 |-  ( ph -> ( abs ` ( 2 x. N ) ) = ( ( abs ` 2 ) x. ( abs ` N ) ) )
93 0le2 
 |-  0 <_ 2
94 29 93 pm3.2i 
 |-  ( 2 e. RR /\ 0 <_ 2 )
95 absid 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
96 94 95 ax-mp 
 |-  ( abs ` 2 ) = 2
97 96 a1i 
 |-  ( ph -> ( abs ` 2 ) = 2 )
98 49 32 66 ltled 
 |-  ( ph -> 0 <_ N )
99 32 98 absidd 
 |-  ( ph -> ( abs ` N ) = N )
100 97 99 oveq12d 
 |-  ( ph -> ( ( abs ` 2 ) x. ( abs ` N ) ) = ( 2 x. N ) )
101 92 100 eqtrd 
 |-  ( ph -> ( abs ` ( 2 x. N ) ) = ( 2 x. N ) )
102 101 oveq1d 
 |-  ( ph -> ( ( abs ` ( 2 x. N ) ) ^ -u J ) = ( ( 2 x. N ) ^ -u J ) )
103 91 102 eqtrd 
 |-  ( ph -> ( abs ` ( ( 2 x. N ) ^ -u J ) ) = ( ( 2 x. N ) ^ -u J ) )
104 103 97 oveq12d 
 |-  ( ph -> ( ( abs ` ( ( 2 x. N ) ^ -u J ) ) / ( abs ` 2 ) ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
105 87 104 eqtrd 
 |-  ( ph -> ( abs ` ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
106 85 105 eqtrd 
 |-  ( ph -> ( abs ` ( B - A ) ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
107 36 recnd 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. CC )
108 52 simpld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 )
109 107 108 6 geoser 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) = ( ( 1 - ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) / ( 1 - ( ( 2 x. N ) x. ( abs ` C ) ) ) ) )
110 107 6 expcld 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) e. CC )
111 108 necomd 
 |-  ( ph -> 1 =/= ( ( 2 x. N ) x. ( abs ` C ) ) )
112 79 110 79 107 111 div2subd 
 |-  ( ph -> ( ( 1 - ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) / ( 1 - ( ( 2 x. N ) x. ( abs ` C ) ) ) ) = ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
113 109 112 eqtrd 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) = ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
114 106 113 oveq12d 
 |-  ( ph -> ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
115 113 41 eqeltrrd 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR )
116 36 6 reexpcld 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) e. RR )
117 116 48 57 redivcld 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR )
118 2rp 
 |-  2 e. RR+
119 118 a1i 
 |-  ( ph -> 2 e. RR+ )
120 119 rpgt0d 
 |-  ( ph -> 0 < 2 )
121 30 32 120 66 mulgt0d 
 |-  ( ph -> 0 < ( 2 x. N ) )
122 33 71 121 3jca 
 |-  ( ph -> ( ( 2 x. N ) e. RR /\ -u J e. ZZ /\ 0 < ( 2 x. N ) ) )
123 expgt0 
 |-  ( ( ( 2 x. N ) e. RR /\ -u J e. ZZ /\ 0 < ( 2 x. N ) ) -> 0 < ( ( 2 x. N ) ^ -u J ) )
124 122 123 syl 
 |-  ( ph -> 0 < ( ( 2 x. N ) ^ -u J ) )
125 49 72 124 ltled 
 |-  ( ph -> 0 <_ ( ( 2 x. N ) ^ -u J ) )
126 72 119 125 divge0d 
 |-  ( ph -> 0 <_ ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
127 116 47 resubcld 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) e. RR )
128 48 54 elrpd 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR+ )
129 116 lem1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) <_ ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) )
130 127 116 128 129 lediv1dd 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) <_ ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
131 115 117 73 126 130 lemul2ad 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) <_ ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
132 48 recnd 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. CC )
133 110 132 57 divrecd 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) = ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
134 133 oveq2d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
135 58 recnd 
 |-  ( ph -> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. CC )
136 74 110 135 mulassd 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
137 136 eqcomd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) = ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
138 86 110 62 45 div23d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) / 2 ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) )
139 138 eqcomd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) = ( ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) / 2 ) )
140 88 70 jca 
 |-  ( ph -> ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) )
141 35 recnd 
 |-  ( ph -> ( abs ` C ) e. CC )
142 5 8 9 knoppndvlem13 
 |-  ( ph -> C =/= 0 )
143 34 142 absne0d 
 |-  ( ph -> ( abs ` C ) =/= 0 )
144 141 143 jca 
 |-  ( ph -> ( ( abs ` C ) e. CC /\ ( abs ` C ) =/= 0 ) )
145 140 144 11 3jca 
 |-  ( ph -> ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) /\ ( ( abs ` C ) e. CC /\ ( abs ` C ) =/= 0 ) /\ J e. ZZ ) )
146 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 ) ) )
147 145 146 syl 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) = ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) )
148 147 oveq2d 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) = ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) ) )
149 88 6 expcld 
 |-  ( ph -> ( ( 2 x. N ) ^ J ) e. CC )
150 43 recnd 
 |-  ( ph -> ( ( abs ` C ) ^ J ) e. CC )
151 86 149 150 mulassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) x. ( ( abs ` C ) ^ J ) ) = ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) ) )
152 151 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) ^ J ) x. ( ( abs ` C ) ^ J ) ) ) = ( ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) x. ( ( abs ` C ) ^ J ) ) )
153 140 71 11 jca32 
 |-  ( ph -> ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) /\ ( -u J e. ZZ /\ J e. ZZ ) ) )
154 expaddz 
 |-  ( ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) /\ ( -u J e. ZZ /\ J e. ZZ ) ) -> ( ( 2 x. N ) ^ ( -u J + J ) ) = ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) )
155 153 154 syl 
 |-  ( ph -> ( ( 2 x. N ) ^ ( -u J + J ) ) = ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) )
156 155 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) = ( ( 2 x. N ) ^ ( -u J + J ) ) )
157 71 zcnd 
 |-  ( ph -> -u J e. CC )
158 6 nn0cnd 
 |-  ( ph -> J e. CC )
159 157 158 addcomd 
 |-  ( ph -> ( -u J + J ) = ( J + -u J ) )
160 158 negidd 
 |-  ( ph -> ( J + -u J ) = 0 )
161 159 160 eqtrd 
 |-  ( ph -> ( -u J + J ) = 0 )
162 161 oveq2d 
 |-  ( ph -> ( ( 2 x. N ) ^ ( -u J + J ) ) = ( ( 2 x. N ) ^ 0 ) )
163 88 exp0d 
 |-  ( ph -> ( ( 2 x. N ) ^ 0 ) = 1 )
164 156 162 163 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) = 1 )
165 164 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) x. ( ( abs ` C ) ^ J ) ) = ( 1 x. ( ( abs ` C ) ^ J ) ) )
166 150 mulid2d 
 |-  ( ph -> ( 1 x. ( ( abs ` C ) ^ J ) ) = ( ( abs ` C ) ^ J ) )
167 165 166 eqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) x. ( ( 2 x. N ) ^ J ) ) x. ( ( abs ` C ) ^ J ) ) = ( ( abs ` C ) ^ J ) )
168 148 152 167 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) = ( ( abs ` C ) ^ J ) )
169 168 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) / 2 ) = ( ( ( abs ` C ) ^ J ) / 2 ) )
170 139 169 eqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) = ( ( ( abs ` C ) ^ J ) / 2 ) )
171 170 oveq1d 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) = ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
172 134 137 171 3eqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) = ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
173 131 172 breqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ J ) - 1 ) / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) <_ ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
174 114 173 eqbrtrd 
 |-  ( ph -> ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) <_ ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )
175 24 42 59 60 174 letrd 
 |-  ( ph -> ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) <_ ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) )