Metamath Proof Explorer

Theorem knoppndvlem15

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem15.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem15.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem15.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppndvlem15.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
5 knoppndvlem15.b 
 |-  B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) )
6 knoppndvlem15.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
7 knoppndvlem15.j 
 |-  ( ph -> J e. NN0 )
8 knoppndvlem15.m 
 |-  ( ph -> M e. ZZ )
9 knoppndvlem15.n 
 |-  ( ph -> N e. NN )
10 knoppndvlem15.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 1red 
 |-  ( ph -> 1 e. RR )
22 9 nnred 
 |-  ( ph -> N e. RR )
23 17 22 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
24 23 14 remulcld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
25 24 21 resubcld 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR )
26 0red 
 |-  ( ph -> 0 e. RR )
27 0lt1 
 |-  0 < 1
28 27 a1i 
 |-  ( ph -> 0 < 1 )
29 6 9 10 knoppndvlem12 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) =/= 1 /\ 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
30 29 simprd 
 |-  ( ph -> 1 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
31 26 21 25 28 30 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) )
32 25 31 jca 
 |-  ( ph -> ( ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) e. RR /\ 0 < ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) )
33 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 )
34 32 33 syl 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) =/= 0 )
35 21 25 34 redivcld 
 |-  ( ph -> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR )
36 21 35 resubcld 
 |-  ( ph -> ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR )
37 20 36 remulcld 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) e. RR )
38 4 a1i 
 |-  ( ph -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
39 7 nn0zd 
 |-  ( ph -> J e. ZZ )
40 9 39 8 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )
41 38 40 eqeltrd 
 |-  ( ph -> A e. RR )
42 1 2 9 12 41 7 knoppcnlem3 
 |-  ( ph -> ( ( F ` A ) ` J ) e. RR )
43 42 recnd 
 |-  ( ph -> ( ( F ` A ) ` J ) e. CC )
44 5 a1i 
 |-  ( ph -> B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) )
45 8 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
46 9 39 45 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) e. RR )
47 44 46 eqeltrd 
 |-  ( ph -> B e. RR )
48 1 2 9 12 47 7 knoppcnlem3 
 |-  ( ph -> ( ( F ` B ) ` J ) e. RR )
49 48 recnd 
 |-  ( ph -> ( ( F ` B ) ` J ) e. CC )
50 43 49 subcld 
 |-  ( ph -> ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) e. CC )
51 50 abscld 
 |-  ( ph -> ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) e. RR )
52 1 2 47 12 9 knoppndvlem5 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) e. RR )
53 52 recnd 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) e. CC )
54 1 2 41 12 9 knoppndvlem5 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) e. RR )
55 54 recnd 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) e. CC )
56 53 55 subcld 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) e. CC )
57 56 abscld 
 |-  ( ph -> ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) e. RR )
58 51 57 resubcld 
 |-  ( ph -> ( ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) - ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) e. RR )
59 50 56 subcld 
 |-  ( ph -> ( ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) e. CC )
60 59 abscld 
 |-  ( ph -> ( abs ` ( ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) e. RR )
61 20 35 jca 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) e. RR /\ ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR ) )
62 remulcl 
 |-  ( ( ( ( ( abs ` C ) ^ J ) / 2 ) e. RR /\ ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. RR ) -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR )
63 61 62 syl 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR )
64 20 63 jca 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) e. RR /\ ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR ) )
65 resubcl 
 |-  ( ( ( ( ( abs ` C ) ^ J ) / 2 ) e. RR /\ ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR ) -> ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) e. RR )
66 64 65 syl 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) e. RR )
67 20 recnd 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / 2 ) e. CC )
68 1cnd 
 |-  ( ph -> 1 e. CC )
69 35 recnd 
 |-  ( ph -> ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) e. CC )
70 67 68 69 subdid 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) = ( ( ( ( ( abs ` C ) ^ J ) / 2 ) x. 1 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
71 67 mulridd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. 1 ) = ( ( ( abs ` C ) ^ J ) / 2 ) )
72 71 oveq1d 
 |-  ( ph -> ( ( ( ( ( abs ` C ) ^ J ) / 2 ) x. 1 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) = ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
73 66 leidd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
74 72 73 eqbrtrd 
 |-  ( ph -> ( ( ( ( ( abs ` C ) ^ J ) / 2 ) x. 1 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
75 70 74 eqbrtrd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) )
76 20 35 remulcld 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) e. RR )
77 20 leidd 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / 2 ) <_ ( ( ( abs ` C ) ^ J ) / 2 ) )
78 43 49 abssubd 
 |-  ( ph -> ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) = ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) )
79 1 2 4 5 6 7 8 9 knoppndvlem10 
 |-  ( ph -> ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) = ( ( ( abs ` C ) ^ J ) / 2 ) )
80 78 79 eqtrd 
 |-  ( ph -> ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) = ( ( ( abs ` C ) ^ J ) / 2 ) )
81 80 eqcomd 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / 2 ) = ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) )
82 77 81 breqtrd 
 |-  ( ph -> ( ( ( abs ` C ) ^ J ) / 2 ) <_ ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) )
83 1 2 4 5 6 7 8 9 10 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 ) ) ) )
84 20 57 51 76 82 83 le2subd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) - ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) - ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) )
85 37 66 58 75 84 letrd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) - ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) )
86 50 56 abs2difd 
 |-  ( ph -> ( ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) - ( abs ` ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) <_ ( abs ` ( ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) )
87 37 58 60 85 86 letrd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( abs ` ( ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) )
88 50 56 abssubd 
 |-  ( ph -> ( abs ` ( ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) ) ) = ( abs ` ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) - ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) ) )
89 87 88 breqtrd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( abs ` ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) - ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) ) )
90 1 2 3 5 6 7 45 9 knoppndvlem6 
 |-  ( ph -> ( W ` B ) = sum_ i e. ( 0 ... J ) ( ( F ` B ) ` i ) )
91 elnn0uz 
 |-  ( J e. NN0 <-> J e. ( ZZ>= ` 0 ) )
92 7 91 sylib 
 |-  ( ph -> J e. ( ZZ>= ` 0 ) )
93 9 adantr 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> N e. NN )
94 12 adantr 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> C e. RR )
95 47 adantr 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> B e. RR )
96 elfznn0 
 |-  ( i e. ( 0 ... J ) -> i e. NN0 )
97 96 adantl 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> i e. NN0 )
98 1 2 93 94 95 97 knoppcnlem3 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> ( ( F ` B ) ` i ) e. RR )
99 98 recnd 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> ( ( F ` B ) ` i ) e. CC )
100 fveq2 
 |-  ( i = J -> ( ( F ` B ) ` i ) = ( ( F ` B ) ` J ) )
101 92 99 100 fsumm1 
 |-  ( ph -> sum_ i e. ( 0 ... J ) ( ( F ` B ) ` i ) = ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) + ( ( F ` B ) ` J ) ) )
102 90 101 eqtrd 
 |-  ( ph -> ( W ` B ) = ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) + ( ( F ` B ) ` J ) ) )
103 1 2 3 4 6 7 8 9 knoppndvlem6 
 |-  ( ph -> ( W ` A ) = sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) )
104 41 adantr 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> A e. RR )
105 1 2 93 94 104 97 knoppcnlem3 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> ( ( F ` A ) ` i ) e. RR )
106 105 recnd 
 |-  ( ( ph /\ i e. ( 0 ... J ) ) -> ( ( F ` A ) ` i ) e. CC )
107 fveq2 
 |-  ( i = J -> ( ( F ` A ) ` i ) = ( ( F ` A ) ` J ) )
108 92 106 107 fsumm1 
 |-  ( ph -> sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) = ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) + ( ( F ` A ) ` J ) ) )
109 103 108 eqtrd 
 |-  ( ph -> ( W ` A ) = ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) + ( ( F ` A ) ` J ) ) )
110 102 109 oveq12d 
 |-  ( ph -> ( ( W ` B ) - ( W ` A ) ) = ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) + ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) + ( ( F ` A ) ` J ) ) ) )
111 53 55 43 49 subadd4d 
 |-  ( ph -> ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) - ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) = ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) + ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) + ( ( F ` A ) ` J ) ) ) )
112 111 eqcomd 
 |-  ( ph -> ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) + ( ( F ` B ) ` J ) ) - ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) + ( ( F ` A ) ` J ) ) ) = ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) - ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) )
113 110 112 eqtrd 
 |-  ( ph -> ( ( W ` B ) - ( W ` A ) ) = ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) - ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) )
114 113 fveq2d 
 |-  ( ph -> ( abs ` ( ( W ` B ) - ( W ` A ) ) ) = ( abs ` ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) - ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) ) )
115 114 eqcomd 
 |-  ( ph -> ( abs ` ( ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) - ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) ) = ( abs ` ( ( W ` B ) - ( W ` A ) ) ) )
116 89 115 breqtrd 
 |-  ( ph -> ( ( ( ( abs ` C ) ^ J ) / 2 ) x. ( 1 - ( 1 / ( ( ( 2 x. N ) x. ( abs ` C ) ) - 1 ) ) ) ) <_ ( abs ` ( ( W ` B ) - ( W ` A ) ) ) )