Metamath Proof Explorer

Theorem dvfsumlem4

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvfsum.s 
|- S = ( T (,) +oo )
dvfsum.z 
|- Z = ( ZZ>= ` M )
dvfsum.m 
|- ( ph -> M e. ZZ )
dvfsum.d 
|- ( ph -> D e. RR )
dvfsum.md 
|- ( ph -> M <_ ( D + 1 ) )
dvfsum.t 
|- ( ph -> T e. RR )
dvfsum.a 
|- ( ( ph /\ x e. S ) -> A e. RR )
dvfsum.b1 
|- ( ( ph /\ x e. S ) -> B e. V )
dvfsum.b2 
|- ( ( ph /\ x e. Z ) -> B e. RR )
dvfsum.b3 
|- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
dvfsum.c 
|- ( x = k -> B = C )
dvfsum.u 
|- ( ph -> U e. RR* )
dvfsum.l 
|- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
dvfsumlem4.g 
|- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
dvfsumlem4.0 
|- ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ U ) ) -> 0 <_ B )
dvfsumlem4.1 
|- ( ph -> X e. S )
dvfsumlem4.2 
|- ( ph -> Y e. S )
dvfsumlem4.3 
|- ( ph -> D <_ X )
dvfsumlem4.4 
|- ( ph -> X <_ Y )
dvfsumlem4.5 
|- ( ph -> Y <_ U )
Assertion dvfsumlem4 
|- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) <_ [_ X / x ]_ B )

Proof

Step Hyp Ref Expression
1 dvfsum.s 
 |-  S = ( T (,) +oo )
2 dvfsum.z 
 |-  Z = ( ZZ>= ` M )
3 dvfsum.m 
 |-  ( ph -> M e. ZZ )
4 dvfsum.d 
 |-  ( ph -> D e. RR )
5 dvfsum.md 
 |-  ( ph -> M <_ ( D + 1 ) )
6 dvfsum.t 
 |-  ( ph -> T e. RR )
7 dvfsum.a 
 |-  ( ( ph /\ x e. S ) -> A e. RR )
8 dvfsum.b1 
 |-  ( ( ph /\ x e. S ) -> B e. V )
9 dvfsum.b2 
 |-  ( ( ph /\ x e. Z ) -> B e. RR )
10 dvfsum.b3 
 |-  ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
11 dvfsum.c 
 |-  ( x = k -> B = C )
12 dvfsum.u 
 |-  ( ph -> U e. RR* )
13 dvfsum.l 
 |-  ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
14 dvfsumlem4.g 
 |-  G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
15 dvfsumlem4.0 
 |-  ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ U ) ) -> 0 <_ B )
16 dvfsumlem4.1 
 |-  ( ph -> X e. S )
17 dvfsumlem4.2 
 |-  ( ph -> Y e. S )
18 dvfsumlem4.3 
 |-  ( ph -> D <_ X )
19 dvfsumlem4.4 
 |-  ( ph -> X <_ Y )
20 dvfsumlem4.5 
 |-  ( ph -> Y <_ U )
21 fzfid 
 |-  ( ph -> ( M ... ( |_ ` Y ) ) e. Fin )
22 9 ralrimiva 
 |-  ( ph -> A. x e. Z B e. RR )
23 elfzuz 
 |-  ( k e. ( M ... ( |_ ` Y ) ) -> k e. ( ZZ>= ` M ) )
24 23 2 eleqtrrdi 
 |-  ( k e. ( M ... ( |_ ` Y ) ) -> k e. Z )
25 11 eleq1d 
 |-  ( x = k -> ( B e. RR <-> C e. RR ) )
26 25 rspccva 
 |-  ( ( A. x e. Z B e. RR /\ k e. Z ) -> C e. RR )
27 22 24 26 syl2an 
 |-  ( ( ph /\ k e. ( M ... ( |_ ` Y ) ) ) -> C e. RR )
28 21 27 fsumrecl 
 |-  ( ph -> sum_ k e. ( M ... ( |_ ` Y ) ) C e. RR )
29 7 ralrimiva 
 |-  ( ph -> A. x e. S A e. RR )
30 nfcsb1v 
 |-  F/_ x [_ Y / x ]_ A
31 30 nfel1 
 |-  F/ x [_ Y / x ]_ A e. RR
32 csbeq1a 
 |-  ( x = Y -> A = [_ Y / x ]_ A )
33 32 eleq1d 
 |-  ( x = Y -> ( A e. RR <-> [_ Y / x ]_ A e. RR ) )
34 31 33 rspc 
 |-  ( Y e. S -> ( A. x e. S A e. RR -> [_ Y / x ]_ A e. RR ) )
35 17 29 34 sylc 
 |-  ( ph -> [_ Y / x ]_ A e. RR )
36 28 35 resubcld 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. RR )
37 nfcv 
 |-  F/_ x Y
38 nfcv 
 |-  F/_ x sum_ k e. ( M ... ( |_ ` Y ) ) C
39 nfcv 
 |-  F/_ x -
40 38 39 30 nfov 
 |-  F/_ x ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A )
41 fveq2 
 |-  ( x = Y -> ( |_ ` x ) = ( |_ ` Y ) )
42 41 oveq2d 
 |-  ( x = Y -> ( M ... ( |_ ` x ) ) = ( M ... ( |_ ` Y ) ) )
43 42 sumeq1d 
 |-  ( x = Y -> sum_ k e. ( M ... ( |_ ` x ) ) C = sum_ k e. ( M ... ( |_ ` Y ) ) C )
44 43 32 oveq12d 
 |-  ( x = Y -> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
45 37 40 44 14 fvmptf 
 |-  ( ( Y e. S /\ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. RR ) -> ( G ` Y ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
46 17 36 45 syl2anc 
 |-  ( ph -> ( G ` Y ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
47 fzfid 
 |-  ( ph -> ( M ... ( |_ ` X ) ) e. Fin )
48 elfzuz 
 |-  ( k e. ( M ... ( |_ ` X ) ) -> k e. ( ZZ>= ` M ) )
49 48 2 eleqtrrdi 
 |-  ( k e. ( M ... ( |_ ` X ) ) -> k e. Z )
50 22 49 26 syl2an 
 |-  ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. RR )
51 47 50 fsumrecl 
 |-  ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. RR )
52 nfcsb1v 
 |-  F/_ x [_ X / x ]_ A
53 52 nfel1 
 |-  F/ x [_ X / x ]_ A e. RR
54 csbeq1a 
 |-  ( x = X -> A = [_ X / x ]_ A )
55 54 eleq1d 
 |-  ( x = X -> ( A e. RR <-> [_ X / x ]_ A e. RR ) )
56 53 55 rspc 
 |-  ( X e. S -> ( A. x e. S A e. RR -> [_ X / x ]_ A e. RR ) )
57 16 29 56 sylc 
 |-  ( ph -> [_ X / x ]_ A e. RR )
58 51 57 resubcld 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. RR )
59 nfcv 
 |-  F/_ x X
60 nfcv 
 |-  F/_ x sum_ k e. ( M ... ( |_ ` X ) ) C
61 60 39 52 nfov 
 |-  F/_ x ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A )
62 fveq2 
 |-  ( x = X -> ( |_ ` x ) = ( |_ ` X ) )
63 62 oveq2d 
 |-  ( x = X -> ( M ... ( |_ ` x ) ) = ( M ... ( |_ ` X ) ) )
64 63 sumeq1d 
 |-  ( x = X -> sum_ k e. ( M ... ( |_ ` x ) ) C = sum_ k e. ( M ... ( |_ ` X ) ) C )
65 64 54 oveq12d 
 |-  ( x = X -> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
66 59 61 65 14 fvmptf 
 |-  ( ( X e. S /\ ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. RR ) -> ( G ` X ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
67 16 58 66 syl2anc 
 |-  ( ph -> ( G ` X ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
68 46 67 oveq12d 
 |-  ( ph -> ( ( G ` Y ) - ( G ` X ) ) = ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
69 68 fveq2d 
 |-  ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) = ( abs ` ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
70 ioossre 
 |-  ( T (,) +oo ) C_ RR
71 1 70 eqsstri 
 |-  S C_ RR
72 71 a1i 
 |-  ( ph -> S C_ RR )
73 72 7 8 10 dvmptrecl 
 |-  ( ( ph /\ x e. S ) -> B e. RR )
74 73 ralrimiva 
 |-  ( ph -> A. x e. S B e. RR )
75 nfv 
 |-  F/ m B e. RR
76 nfcsb1v 
 |-  F/_ x [_ m / x ]_ B
77 76 nfel1 
 |-  F/ x [_ m / x ]_ B e. RR
78 csbeq1a 
 |-  ( x = m -> B = [_ m / x ]_ B )
79 78 eleq1d 
 |-  ( x = m -> ( B e. RR <-> [_ m / x ]_ B e. RR ) )
80 75 77 79 cbvralw 
 |-  ( A. x e. S B e. RR <-> A. m e. S [_ m / x ]_ B e. RR )
81 74 80 sylib 
 |-  ( ph -> A. m e. S [_ m / x ]_ B e. RR )
82 csbeq1 
 |-  ( m = X -> [_ m / x ]_ B = [_ X / x ]_ B )
83 82 eleq1d 
 |-  ( m = X -> ( [_ m / x ]_ B e. RR <-> [_ X / x ]_ B e. RR ) )
84 83 rspcv 
 |-  ( X e. S -> ( A. m e. S [_ m / x ]_ B e. RR -> [_ X / x ]_ B e. RR ) )
85 16 81 84 sylc 
 |-  ( ph -> [_ X / x ]_ B e. RR )
86 58 85 resubcld 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - [_ X / x ]_ B ) e. RR )
87 71 16 sselid 
 |-  ( ph -> X e. RR )
88 reflcl 
 |-  ( X e. RR -> ( |_ ` X ) e. RR )
89 87 88 syl 
 |-  ( ph -> ( |_ ` X ) e. RR )
90 87 89 resubcld 
 |-  ( ph -> ( X - ( |_ ` X ) ) e. RR )
91 90 85 remulcld 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. RR )
92 91 58 readdcld 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. RR )
93 92 85 resubcld 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) e. RR )
94 fracge0 
 |-  ( X e. RR -> 0 <_ ( X - ( |_ ` X ) ) )
95 87 94 syl 
 |-  ( ph -> 0 <_ ( X - ( |_ ` X ) ) )
96 87 rexrd 
 |-  ( ph -> X e. RR* )
97 71 17 sselid 
 |-  ( ph -> Y e. RR )
98 97 rexrd 
 |-  ( ph -> Y e. RR* )
99 96 98 12 19 20 xrletrd 
 |-  ( ph -> X <_ U )
100 16 18 99 3jca 
 |-  ( ph -> ( X e. S /\ D <_ X /\ X <_ U ) )
101 simpr1 
 |-  ( ( ph /\ ( X e. S /\ D <_ X /\ X <_ U ) ) -> X e. S )
102 nfv 
 |-  F/ x ( ph /\ ( X e. S /\ D <_ X /\ X <_ U ) )
103 nfcv 
 |-  F/_ x 0
104 nfcv 
 |-  F/_ x <_
105 nfcsb1v 
 |-  F/_ x [_ X / x ]_ B
106 103 104 105 nfbr 
 |-  F/ x 0 <_ [_ X / x ]_ B
107 102 106 nfim 
 |-  F/ x ( ( ph /\ ( X e. S /\ D <_ X /\ X <_ U ) ) -> 0 <_ [_ X / x ]_ B )
108 eleq1 
 |-  ( x = X -> ( x e. S <-> X e. S ) )
109 breq2 
 |-  ( x = X -> ( D <_ x <-> D <_ X ) )
110 breq1 
 |-  ( x = X -> ( x <_ U <-> X <_ U ) )
111 108 109 110 3anbi123d 
 |-  ( x = X -> ( ( x e. S /\ D <_ x /\ x <_ U ) <-> ( X e. S /\ D <_ X /\ X <_ U ) ) )
112 111 anbi2d 
 |-  ( x = X -> ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ U ) ) <-> ( ph /\ ( X e. S /\ D <_ X /\ X <_ U ) ) ) )
113 csbeq1a 
 |-  ( x = X -> B = [_ X / x ]_ B )
114 113 breq2d 
 |-  ( x = X -> ( 0 <_ B <-> 0 <_ [_ X / x ]_ B ) )
115 112 114 imbi12d 
 |-  ( x = X -> ( ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ U ) ) -> 0 <_ B ) <-> ( ( ph /\ ( X e. S /\ D <_ X /\ X <_ U ) ) -> 0 <_ [_ X / x ]_ B ) ) )
116 107 115 15 vtoclg1f 
 |-  ( X e. S -> ( ( ph /\ ( X e. S /\ D <_ X /\ X <_ U ) ) -> 0 <_ [_ X / x ]_ B ) )
117 101 116 mpcom 
 |-  ( ( ph /\ ( X e. S /\ D <_ X /\ X <_ U ) ) -> 0 <_ [_ X / x ]_ B )
118 100 117 mpdan 
 |-  ( ph -> 0 <_ [_ X / x ]_ B )
119 90 85 95 118 mulge0d 
 |-  ( ph -> 0 <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
120 58 91 addge02d 
 |-  ( ph -> ( 0 <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <-> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
121 119 120 mpbid 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
122 58 92 85 121 lesub1dd 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - [_ X / x ]_ B ) <_ ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) )
123 reflcl 
 |-  ( Y e. RR -> ( |_ ` Y ) e. RR )
124 97 123 syl 
 |-  ( ph -> ( |_ ` Y ) e. RR )
125 97 124 resubcld 
 |-  ( ph -> ( Y - ( |_ ` Y ) ) e. RR )
126 csbeq1 
 |-  ( m = Y -> [_ m / x ]_ B = [_ Y / x ]_ B )
127 126 eleq1d 
 |-  ( m = Y -> ( [_ m / x ]_ B e. RR <-> [_ Y / x ]_ B e. RR ) )
128 127 rspcv 
 |-  ( Y e. S -> ( A. m e. S [_ m / x ]_ B e. RR -> [_ Y / x ]_ B e. RR ) )
129 17 81 128 sylc 
 |-  ( ph -> [_ Y / x ]_ B e. RR )
130 125 129 remulcld 
 |-  ( ph -> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) e. RR )
131 130 36 readdcld 
 |-  ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. RR )
132 131 129 resubcld 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - [_ Y / x ]_ B ) e. RR )
133 eqid 
 |-  ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )
134 1 2 3 4 5 6 7 8 9 10 11 12 13 133 16 17 18 19 20 dvfsumlem3 
 |-  ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` Y ) <_ ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` X ) /\ ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` X ) - [_ X / x ]_ B ) <_ ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` Y ) - [_ Y / x ]_ B ) ) )
135 134 simprd 
 |-  ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` X ) - [_ X / x ]_ B ) <_ ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` Y ) - [_ Y / x ]_ B ) )
136 nfcv 
 |-  F/_ x ( X - ( |_ ` X ) )
137 nfcv 
 |-  F/_ x x.
138 136 137 105 nfov 
 |-  F/_ x ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B )
139 nfcv 
 |-  F/_ x +
140 138 139 61 nfov 
 |-  F/_ x ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
141 id 
 |-  ( x = X -> x = X )
142 141 62 oveq12d 
 |-  ( x = X -> ( x - ( |_ ` x ) ) = ( X - ( |_ ` X ) ) )
143 142 113 oveq12d 
 |-  ( x = X -> ( ( x - ( |_ ` x ) ) x. B ) = ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
144 143 65 oveq12d 
 |-  ( x = X -> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
145 59 140 144 133 fvmptf 
 |-  ( ( X e. S /\ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. RR ) -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` X ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
146 16 92 145 syl2anc 
 |-  ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` X ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
147 146 oveq1d 
 |-  ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` X ) - [_ X / x ]_ B ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) )
148 nfcv 
 |-  F/_ x ( Y - ( |_ ` Y ) )
149 nfcsb1v 
 |-  F/_ x [_ Y / x ]_ B
150 148 137 149 nfov 
 |-  F/_ x ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B )
151 150 139 40 nfov 
 |-  F/_ x ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
152 id 
 |-  ( x = Y -> x = Y )
153 152 41 oveq12d 
 |-  ( x = Y -> ( x - ( |_ ` x ) ) = ( Y - ( |_ ` Y ) ) )
154 csbeq1a 
 |-  ( x = Y -> B = [_ Y / x ]_ B )
155 153 154 oveq12d 
 |-  ( x = Y -> ( ( x - ( |_ ` x ) ) x. B ) = ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) )
156 155 44 oveq12d 
 |-  ( x = Y -> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) = ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
157 37 151 156 133 fvmptf 
 |-  ( ( Y e. S /\ ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. RR ) -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` Y ) = ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
158 17 131 157 syl2anc 
 |-  ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` Y ) = ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
159 158 oveq1d 
 |-  ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` Y ) - [_ Y / x ]_ B ) = ( ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - [_ Y / x ]_ B ) )
160 135 147 159 3brtr3d 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) <_ ( ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - [_ Y / x ]_ B ) )
161 36 recnd 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. CC )
162 129 recnd 
 |-  ( ph -> [_ Y / x ]_ B e. CC )
163 130 recnd 
 |-  ( ph -> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) e. CC )
164 161 162 163 subsub3d 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) ) = ( ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) - [_ Y / x ]_ B ) )
165 161 163 addcomd 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) = ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
166 165 oveq1d 
 |-  ( ph -> ( ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) - [_ Y / x ]_ B ) = ( ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - [_ Y / x ]_ B ) )
167 164 166 eqtrd 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) ) = ( ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - [_ Y / x ]_ B ) )
168 1red 
 |-  ( ph -> 1 e. RR )
169 4 87 97 18 19 letrd 
 |-  ( ph -> D <_ Y )
170 17 169 20 3jca 
 |-  ( ph -> ( Y e. S /\ D <_ Y /\ Y <_ U ) )
171 simpr1 
 |-  ( ( ph /\ ( Y e. S /\ D <_ Y /\ Y <_ U ) ) -> Y e. S )
172 nfv 
 |-  F/ x ( ph /\ ( Y e. S /\ D <_ Y /\ Y <_ U ) )
173 103 104 149 nfbr 
 |-  F/ x 0 <_ [_ Y / x ]_ B
174 172 173 nfim 
 |-  F/ x ( ( ph /\ ( Y e. S /\ D <_ Y /\ Y <_ U ) ) -> 0 <_ [_ Y / x ]_ B )
175 eleq1 
 |-  ( x = Y -> ( x e. S <-> Y e. S ) )
176 breq2 
 |-  ( x = Y -> ( D <_ x <-> D <_ Y ) )
177 breq1 
 |-  ( x = Y -> ( x <_ U <-> Y <_ U ) )
178 175 176 177 3anbi123d 
 |-  ( x = Y -> ( ( x e. S /\ D <_ x /\ x <_ U ) <-> ( Y e. S /\ D <_ Y /\ Y <_ U ) ) )
179 178 anbi2d 
 |-  ( x = Y -> ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ U ) ) <-> ( ph /\ ( Y e. S /\ D <_ Y /\ Y <_ U ) ) ) )
180 154 breq2d 
 |-  ( x = Y -> ( 0 <_ B <-> 0 <_ [_ Y / x ]_ B ) )
181 179 180 imbi12d 
 |-  ( x = Y -> ( ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ U ) ) -> 0 <_ B ) <-> ( ( ph /\ ( Y e. S /\ D <_ Y /\ Y <_ U ) ) -> 0 <_ [_ Y / x ]_ B ) ) )
182 174 181 15 vtoclg1f 
 |-  ( Y e. S -> ( ( ph /\ ( Y e. S /\ D <_ Y /\ Y <_ U ) ) -> 0 <_ [_ Y / x ]_ B ) )
183 171 182 mpcom 
 |-  ( ( ph /\ ( Y e. S /\ D <_ Y /\ Y <_ U ) ) -> 0 <_ [_ Y / x ]_ B )
184 170 183 mpdan 
 |-  ( ph -> 0 <_ [_ Y / x ]_ B )
185 fracle1 
 |-  ( Y e. RR -> ( Y - ( |_ ` Y ) ) <_ 1 )
186 97 185 syl 
 |-  ( ph -> ( Y - ( |_ ` Y ) ) <_ 1 )
187 125 168 129 184 186 lemul1ad 
 |-  ( ph -> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) <_ ( 1 x. [_ Y / x ]_ B ) )
188 162 mullidd 
 |-  ( ph -> ( 1 x. [_ Y / x ]_ B ) = [_ Y / x ]_ B )
189 187 188 breqtrd 
 |-  ( ph -> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) <_ [_ Y / x ]_ B )
190 129 130 subge0d 
 |-  ( ph -> ( 0 <_ ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) <-> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) <_ [_ Y / x ]_ B ) )
191 189 190 mpbird 
 |-  ( ph -> 0 <_ ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) )
192 129 130 resubcld 
 |-  ( ph -> ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) e. RR )
193 36 192 subge02d 
 |-  ( ph -> ( 0 <_ ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) <-> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) ) <_ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
194 191 193 mpbid 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( [_ Y / x ]_ B - ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) ) ) <_ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
195 167 194 eqbrtrrd 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - [_ Y / x ]_ B ) <_ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
196 93 132 36 160 195 letrd 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) <_ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
197 86 93 36 122 196 letrd 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - [_ X / x ]_ B ) <_ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
198 85 58 readdcld 
 |-  ( ph -> ( [_ X / x ]_ B + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. RR )
199 fracge0 
 |-  ( Y e. RR -> 0 <_ ( Y - ( |_ ` Y ) ) )
200 97 199 syl 
 |-  ( ph -> 0 <_ ( Y - ( |_ ` Y ) ) )
201 125 129 200 184 mulge0d 
 |-  ( ph -> 0 <_ ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) )
202 36 130 addge02d 
 |-  ( ph -> ( 0 <_ ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) <-> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) )
203 201 202 mpbid 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
204 134 simpld 
 |-  ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` Y ) <_ ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) ) ` X ) )
205 204 158 146 3brtr3d 
 |-  ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
206 36 131 92 203 205 letrd 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
207 fracle1 
 |-  ( X e. RR -> ( X - ( |_ ` X ) ) <_ 1 )
208 87 207 syl 
 |-  ( ph -> ( X - ( |_ ` X ) ) <_ 1 )
209 90 168 85 118 208 lemul1ad 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <_ ( 1 x. [_ X / x ]_ B ) )
210 85 recnd 
 |-  ( ph -> [_ X / x ]_ B e. CC )
211 210 mullidd 
 |-  ( ph -> ( 1 x. [_ X / x ]_ B ) = [_ X / x ]_ B )
212 209 211 breqtrd 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <_ [_ X / x ]_ B )
213 91 85 58 212 leadd1dd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) <_ ( [_ X / x ]_ B + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
214 36 92 198 206 213 letrd 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( [_ X / x ]_ B + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
215 58 recnd 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. CC )
216 210 215 addcomd 
 |-  ( ph -> ( [_ X / x ]_ B + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) = ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) + [_ X / x ]_ B ) )
217 214 216 breqtrd 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) + [_ X / x ]_ B ) )
218 36 58 85 absdifled 
 |-  ( ph -> ( ( abs ` ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) <_ [_ X / x ]_ B <-> ( ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - [_ X / x ]_ B ) <_ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) /\ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) + [_ X / x ]_ B ) ) ) )
219 197 217 218 mpbir2and 
 |-  ( ph -> ( abs ` ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) <_ [_ X / x ]_ B )
220 69 219 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) <_ [_ X / x ]_ B )