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 mulid1d
 |-  ( 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 ) ) ) )