Metamath Proof Explorer

Theorem knoppndvlem11

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 28-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem11.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppndvlem11.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppndvlem11.a 
|- ( ph -> A e. RR )
knoppndvlem11.b 
|- ( ph -> B e. RR )
knoppndvlem11.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppndvlem11.j 
|- ( ph -> J e. NN0 )
knoppndvlem11.n 
|- ( ph -> N e. NN )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem11.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem11.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem11.a 
 |-  ( ph -> A e. RR )
4 knoppndvlem11.b 
 |-  ( ph -> B e. RR )
5 knoppndvlem11.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
6 knoppndvlem11.j 
 |-  ( ph -> J e. NN0 )
7 knoppndvlem11.n 
 |-  ( ph -> N e. NN )
8 fzfid 
 |-  ( ph -> ( 0 ... ( J - 1 ) ) e. Fin )
9 7 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> N e. NN )
10 5 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
11 10 simpld 
 |-  ( ph -> C e. RR )
12 11 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> C e. RR )
13 4 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> B e. RR )
14 elfznn0 
 |-  ( i e. ( 0 ... ( J - 1 ) ) -> i e. NN0 )
15 14 adantl 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> i e. NN0 )
16 1 2 9 12 13 15 knoppcnlem3 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( F ` B ) ` i ) e. RR )
17 16 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( F ` B ) ` i ) e. CC )
18 3 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> A e. RR )
19 1 2 9 12 18 15 knoppcnlem3 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( F ` A ) ` i ) e. RR )
20 19 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( F ` A ) ` i ) e. CC )
21 8 17 20 fsumsub 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) = ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) )
22 21 eqcomd 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` B ) ` i ) - sum_ i e. ( 0 ... ( J - 1 ) ) ( ( F ` A ) ` i ) ) = sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) )
23 22 fveq2d 
 |-  ( ph -> ( abs ` ( 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 ) - ( ( F ` A ) ` i ) ) ) )
24 17 20 subcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) e. CC )
25 8 24 fsumcl 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) e. CC )
26 25 abscld 
 |-  ( ph -> ( abs ` sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) e. RR )
27 24 abscld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) e. RR )
28 8 27 fsumrecl 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) e. RR )
29 4 3 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
30 29 recnd 
 |-  ( ph -> ( B - A ) e. CC )
31 30 abscld 
 |-  ( ph -> ( abs ` ( B - A ) ) e. RR )
32 2re 
 |-  2 e. RR
33 32 a1i 
 |-  ( ph -> 2 e. RR )
34 nnre 
 |-  ( N e. NN -> N e. RR )
35 7 34 syl 
 |-  ( ph -> N e. RR )
36 33 35 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
37 11 recnd 
 |-  ( ph -> C e. CC )
38 37 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
39 36 38 remulcld 
 |-  ( ph -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
40 39 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( 2 x. N ) x. ( abs ` C ) ) e. RR )
41 40 15 reexpcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) e. RR )
42 8 41 fsumrecl 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) e. RR )
43 31 42 remulcld 
 |-  ( ph -> ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) e. RR )
44 8 24 fsumabs 
 |-  ( ph -> ( abs ` sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) <_ sum_ i e. ( 0 ... ( J - 1 ) ) ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) )
45 31 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( B - A ) ) e. RR )
46 45 41 remulcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) e. RR )
47 2 13 15 knoppcnlem1 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( F ` B ) ` i ) = ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) ) )
48 2 18 15 knoppcnlem1 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( F ` A ) ` i ) = ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) )
49 47 48 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) = ( ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) ) - ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) )
50 12 15 reexpcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( C ^ i ) e. RR )
51 50 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( C ^ i ) e. CC )
52 36 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( 2 x. N ) e. RR )
53 52 15 reexpcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( 2 x. N ) ^ i ) e. RR )
54 53 13 remulcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) ^ i ) x. B ) e. RR )
55 1 54 dnicld2 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) e. RR )
56 55 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) e. CC )
57 53 18 remulcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) ^ i ) x. A ) e. RR )
58 1 57 dnicld2 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) e. RR )
59 58 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) e. CC )
60 51 56 59 subdid 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( C ^ i ) x. ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) = ( ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) ) - ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) )
61 60 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) ) - ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) = ( ( C ^ i ) x. ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) )
62 49 61 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) = ( ( C ^ i ) x. ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) )
63 62 fveq2d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) = ( abs ` ( ( C ^ i ) x. ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) )
64 56 59 subcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) e. CC )
65 51 64 absmuld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( C ^ i ) x. ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) = ( ( abs ` ( C ^ i ) ) x. ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) )
66 37 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> C e. CC )
67 66 15 absexpd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( C ^ i ) ) = ( ( abs ` C ) ^ i ) )
68 67 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( abs ` ( C ^ i ) ) x. ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) = ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) )
69 65 68 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( C ^ i ) x. ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) = ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) )
70 63 69 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) = ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) )
71 64 abscld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) e. RR )
72 54 57 resubcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) e. RR )
73 72 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) e. CC )
74 73 abscld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) ) e. RR )
75 38 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` C ) e. RR )
76 75 15 reexpcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( abs ` C ) ^ i ) e. RR )
77 66 absge0d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> 0 <_ ( abs ` C ) )
78 75 15 77 expge0d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> 0 <_ ( ( abs ` C ) ^ i ) )
79 1 57 54 dnibnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) <_ ( abs ` ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) ) )
80 71 74 76 78 79 lemul2ad 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) <_ ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) )
81 53 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( 2 x. N ) ^ i ) e. CC )
82 13 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> B e. CC )
83 18 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> A e. CC )
84 81 82 83 subdid 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) ^ i ) x. ( B - A ) ) = ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) )
85 84 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) = ( ( ( 2 x. N ) ^ i ) x. ( B - A ) ) )
86 85 fveq2d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) ) = ( abs ` ( ( ( 2 x. N ) ^ i ) x. ( B - A ) ) ) )
87 30 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( B - A ) e. CC )
88 81 87 absmuld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( 2 x. N ) ^ i ) x. ( B - A ) ) ) = ( ( abs ` ( ( 2 x. N ) ^ i ) ) x. ( abs ` ( B - A ) ) ) )
89 52 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( 2 x. N ) e. CC )
90 89 15 absexpd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( 2 x. N ) ^ i ) ) = ( ( abs ` ( 2 x. N ) ) ^ i ) )
91 33 recnd 
 |-  ( ph -> 2 e. CC )
92 35 recnd 
 |-  ( ph -> N e. CC )
93 91 92 absmuld 
 |-  ( ph -> ( abs ` ( 2 x. N ) ) = ( ( abs ` 2 ) x. ( abs ` N ) ) )
94 0le2 
 |-  0 <_ 2
95 32 absidi 
 |-  ( 0 <_ 2 -> ( abs ` 2 ) = 2 )
96 94 95 ax-mp 
 |-  ( abs ` 2 ) = 2
97 96 a1i 
 |-  ( ph -> ( abs ` 2 ) = 2 )
98 0red 
 |-  ( ph -> 0 e. RR )
99 1red 
 |-  ( ph -> 1 e. RR )
100 0le1 
 |-  0 <_ 1
101 100 a1i 
 |-  ( ph -> 0 <_ 1 )
102 nnge1 
 |-  ( N e. NN -> 1 <_ N )
103 7 102 syl 
 |-  ( ph -> 1 <_ N )
104 98 99 35 101 103 letrd 
 |-  ( ph -> 0 <_ N )
105 35 104 absidd 
 |-  ( ph -> ( abs ` N ) = N )
106 97 105 oveq12d 
 |-  ( ph -> ( ( abs ` 2 ) x. ( abs ` N ) ) = ( 2 x. N ) )
107 93 106 eqtrd 
 |-  ( ph -> ( abs ` ( 2 x. N ) ) = ( 2 x. N ) )
108 107 oveq1d 
 |-  ( ph -> ( ( abs ` ( 2 x. N ) ) ^ i ) = ( ( 2 x. N ) ^ i ) )
109 108 adantr 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( abs ` ( 2 x. N ) ) ^ i ) = ( ( 2 x. N ) ^ i ) )
110 90 109 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( 2 x. N ) ^ i ) ) = ( ( 2 x. N ) ^ i ) )
111 110 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( abs ` ( ( 2 x. N ) ^ i ) ) x. ( abs ` ( B - A ) ) ) = ( ( ( 2 x. N ) ^ i ) x. ( abs ` ( B - A ) ) ) )
112 88 111 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( 2 x. N ) ^ i ) x. ( B - A ) ) ) = ( ( ( 2 x. N ) ^ i ) x. ( abs ` ( B - A ) ) ) )
113 86 112 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) ) = ( ( ( 2 x. N ) ^ i ) x. ( abs ` ( B - A ) ) ) )
114 113 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) = ( ( ( abs ` C ) ^ i ) x. ( ( ( 2 x. N ) ^ i ) x. ( abs ` ( B - A ) ) ) ) )
115 76 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( abs ` C ) ^ i ) e. CC )
116 45 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( B - A ) ) e. CC )
117 115 81 116 mulassd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) x. ( abs ` ( B - A ) ) ) = ( ( ( abs ` C ) ^ i ) x. ( ( ( 2 x. N ) ^ i ) x. ( abs ` ( B - A ) ) ) ) )
118 117 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( ( ( 2 x. N ) ^ i ) x. ( abs ` ( B - A ) ) ) ) = ( ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) x. ( abs ` ( B - A ) ) ) )
119 115 81 mulcld 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) e. CC )
120 119 116 mulcomd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) x. ( abs ` ( B - A ) ) ) = ( ( abs ` ( B - A ) ) x. ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) ) )
121 115 81 mulcomd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) = ( ( ( 2 x. N ) ^ i ) x. ( ( abs ` C ) ^ i ) ) )
122 75 recnd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` C ) e. CC )
123 89 122 15 mulexpd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) = ( ( ( 2 x. N ) ^ i ) x. ( ( abs ` C ) ^ i ) ) )
124 123 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) ^ i ) x. ( ( abs ` C ) ^ i ) ) = ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) )
125 121 124 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) = ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) )
126 125 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( abs ` ( B - A ) ) x. ( ( ( abs ` C ) ^ i ) x. ( ( 2 x. N ) ^ i ) ) ) = ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
127 118 120 126 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( ( ( 2 x. N ) ^ i ) x. ( abs ` ( B - A ) ) ) ) = ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
128 114 127 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( ( ( 2 x. N ) ^ i ) x. B ) - ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) = ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
129 80 128 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( abs ` C ) ^ i ) x. ( abs ` ( ( T ` ( ( ( 2 x. N ) ^ i ) x. B ) ) - ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) ) ) <_ ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
130 70 129 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) <_ ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
131 8 27 46 130 fsumle 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) <_ sum_ i e. ( 0 ... ( J - 1 ) ) ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
132 31 recnd 
 |-  ( ph -> ( abs ` ( B - A ) ) e. CC )
133 125 119 eqeltrrd 
 |-  ( ( ph /\ i e. ( 0 ... ( J - 1 ) ) ) -> ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) e. CC )
134 8 132 133 fsummulc2 
 |-  ( ph -> ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) = sum_ i e. ( 0 ... ( J - 1 ) ) ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
135 134 eqcomd 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( ( abs ` ( B - A ) ) x. ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) = ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
136 131 135 breqtrd 
 |-  ( ph -> sum_ i e. ( 0 ... ( J - 1 ) ) ( abs ` ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) <_ ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
137 26 28 43 44 136 letrd 
 |-  ( ph -> ( abs ` sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( F ` B ) ` i ) - ( ( F ` A ) ` i ) ) ) <_ ( ( abs ` ( B - A ) ) x. sum_ i e. ( 0 ... ( J - 1 ) ) ( ( ( 2 x. N ) x. ( abs ` C ) ) ^ i ) ) )
138 23 137 eqbrtrd 
 |-  ( 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 ) ) )