Metamath Proof Explorer

Theorem dvfsumlem1

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-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 )
dvfsum.h 
|- H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )
dvfsumlem1.1 
|- ( ph -> X e. S )
dvfsumlem1.2 
|- ( ph -> Y e. S )
dvfsumlem1.3 
|- ( ph -> D <_ X )
dvfsumlem1.4 
|- ( ph -> X <_ Y )
dvfsumlem1.5 
|- ( ph -> Y <_ U )
dvfsumlem1.6 
|- ( ph -> Y <_ ( ( |_ ` X ) + 1 ) )
Assertion dvfsumlem1 
|- ( ph -> ( H ` Y ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )

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 dvfsum.h 
 |-  H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )
15 dvfsumlem1.1 
 |-  ( ph -> X e. S )
16 dvfsumlem1.2 
 |-  ( ph -> Y e. S )
17 dvfsumlem1.3 
 |-  ( ph -> D <_ X )
18 dvfsumlem1.4 
 |-  ( ph -> X <_ Y )
19 dvfsumlem1.5 
 |-  ( ph -> Y <_ U )
20 dvfsumlem1.6 
 |-  ( ph -> Y <_ ( ( |_ ` X ) + 1 ) )
21 ioossre 
 |-  ( T (,) +oo ) C_ RR
22 1 21 eqsstri 
 |-  S C_ RR
23 22 16 sselid 
 |-  ( ph -> Y e. RR )
24 22 15 sselid 
 |-  ( ph -> X e. RR )
25 24 flcld 
 |-  ( ph -> ( |_ ` X ) e. ZZ )
26 reflcl 
 |-  ( X e. RR -> ( |_ ` X ) e. RR )
27 24 26 syl 
 |-  ( ph -> ( |_ ` X ) e. RR )
28 flle 
 |-  ( X e. RR -> ( |_ ` X ) <_ X )
29 24 28 syl 
 |-  ( ph -> ( |_ ` X ) <_ X )
30 27 24 23 29 18 letrd 
 |-  ( ph -> ( |_ ` X ) <_ Y )
31 flbi 
 |-  ( ( Y e. RR /\ ( |_ ` X ) e. ZZ ) -> ( ( |_ ` Y ) = ( |_ ` X ) <-> ( ( |_ ` X ) <_ Y /\ Y < ( ( |_ ` X ) + 1 ) ) ) )
32 31 baibd 
 |-  ( ( ( Y e. RR /\ ( |_ ` X ) e. ZZ ) /\ ( |_ ` X ) <_ Y ) -> ( ( |_ ` Y ) = ( |_ ` X ) <-> Y < ( ( |_ ` X ) + 1 ) ) )
33 23 25 30 32 syl21anc 
 |-  ( ph -> ( ( |_ ` Y ) = ( |_ ` X ) <-> Y < ( ( |_ ` X ) + 1 ) ) )
34 33 biimpar 
 |-  ( ( ph /\ Y < ( ( |_ ` X ) + 1 ) ) -> ( |_ ` Y ) = ( |_ ` X ) )
35 34 oveq2d 
 |-  ( ( ph /\ Y < ( ( |_ ` X ) + 1 ) ) -> ( Y - ( |_ ` Y ) ) = ( Y - ( |_ ` X ) ) )
36 35 oveq1d 
 |-  ( ( ph /\ Y < ( ( |_ ` X ) + 1 ) ) -> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) = ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) )
37 34 oveq2d 
 |-  ( ( ph /\ Y < ( ( |_ ` X ) + 1 ) ) -> ( M ... ( |_ ` Y ) ) = ( M ... ( |_ ` X ) ) )
38 37 sumeq1d 
 |-  ( ( ph /\ Y < ( ( |_ ` X ) + 1 ) ) -> sum_ k e. ( M ... ( |_ ` Y ) ) C = sum_ k e. ( M ... ( |_ ` X ) ) C )
39 38 oveq1d 
 |-  ( ( ph /\ Y < ( ( |_ ` X ) + 1 ) ) -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) )
40 36 39 oveq12d 
 |-  ( ( ph /\ Y < ( ( |_ ` X ) + 1 ) ) -> ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) ) )
41 simpr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> Y = ( ( |_ ` X ) + 1 ) )
42 24 adantr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> X e. RR )
43 42 flcld 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( |_ ` X ) e. ZZ )
44 43 peano2zd 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( |_ ` X ) + 1 ) e. ZZ )
45 41 44 eqeltrd 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> Y e. ZZ )
46 flid 
 |-  ( Y e. ZZ -> ( |_ ` Y ) = Y )
47 45 46 syl 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( |_ ` Y ) = Y )
48 47 41 eqtrd 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( |_ ` Y ) = ( ( |_ ` X ) + 1 ) )
49 48 oveq2d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( Y - ( |_ ` Y ) ) = ( Y - ( ( |_ ` X ) + 1 ) ) )
50 49 oveq1d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) = ( ( Y - ( ( |_ ` X ) + 1 ) ) x. [_ Y / x ]_ B ) )
51 23 recnd 
 |-  ( ph -> Y e. CC )
52 27 recnd 
 |-  ( ph -> ( |_ ` X ) e. CC )
53 51 52 subcld 
 |-  ( ph -> ( Y - ( |_ ` X ) ) e. CC )
54 1cnd 
 |-  ( ph -> 1 e. CC )
55 22 a1i 
 |-  ( ph -> S C_ RR )
56 55 7 8 10 dvmptrecl 
 |-  ( ( ph /\ x e. S ) -> B e. RR )
57 56 recnd 
 |-  ( ( ph /\ x e. S ) -> B e. CC )
58 57 ralrimiva 
 |-  ( ph -> A. x e. S B e. CC )
59 nfcsb1v 
 |-  F/_ x [_ Y / x ]_ B
60 59 nfel1 
 |-  F/ x [_ Y / x ]_ B e. CC
61 csbeq1a 
 |-  ( x = Y -> B = [_ Y / x ]_ B )
62 61 eleq1d 
 |-  ( x = Y -> ( B e. CC <-> [_ Y / x ]_ B e. CC ) )
63 60 62 rspc 
 |-  ( Y e. S -> ( A. x e. S B e. CC -> [_ Y / x ]_ B e. CC ) )
64 16 58 63 sylc 
 |-  ( ph -> [_ Y / x ]_ B e. CC )
65 53 54 64 subdird 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) )
66 51 52 54 subsub4d 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) = ( Y - ( ( |_ ` X ) + 1 ) ) )
67 66 oveq1d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( Y - ( ( |_ ` X ) + 1 ) ) x. [_ Y / x ]_ B ) )
68 64 mulid2d 
 |-  ( ph -> ( 1 x. [_ Y / x ]_ B ) = [_ Y / x ]_ B )
69 68 oveq2d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
70 65 67 69 3eqtr3d 
 |-  ( ph -> ( ( Y - ( ( |_ ` X ) + 1 ) ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
71 70 adantr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( Y - ( ( |_ ` X ) + 1 ) ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
72 50 71 eqtrd 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
73 25 peano2zd 
 |-  ( ph -> ( ( |_ ` X ) + 1 ) e. ZZ )
74 3 zred 
 |-  ( ph -> M e. RR )
75 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
76 74 75 syl 
 |-  ( ph -> ( M - 1 ) e. RR )
77 1red 
 |-  ( ph -> 1 e. RR )
78 74 77 4 lesubaddd 
 |-  ( ph -> ( ( M - 1 ) <_ D <-> M <_ ( D + 1 ) ) )
79 5 78 mpbird 
 |-  ( ph -> ( M - 1 ) <_ D )
80 76 4 24 79 17 letrd 
 |-  ( ph -> ( M - 1 ) <_ X )
81 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
82 3 81 syl 
 |-  ( ph -> ( M - 1 ) e. ZZ )
83 flge 
 |-  ( ( X e. RR /\ ( M - 1 ) e. ZZ ) -> ( ( M - 1 ) <_ X <-> ( M - 1 ) <_ ( |_ ` X ) ) )
84 24 82 83 syl2anc 
 |-  ( ph -> ( ( M - 1 ) <_ X <-> ( M - 1 ) <_ ( |_ ` X ) ) )
85 80 84 mpbid 
 |-  ( ph -> ( M - 1 ) <_ ( |_ ` X ) )
86 74 77 27 lesubaddd 
 |-  ( ph -> ( ( M - 1 ) <_ ( |_ ` X ) <-> M <_ ( ( |_ ` X ) + 1 ) ) )
87 85 86 mpbid 
 |-  ( ph -> M <_ ( ( |_ ` X ) + 1 ) )
88 eluz2 
 |-  ( ( ( |_ ` X ) + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( ( |_ ` X ) + 1 ) e. ZZ /\ M <_ ( ( |_ ` X ) + 1 ) ) )
89 3 73 87 88 syl3anbrc 
 |-  ( ph -> ( ( |_ ` X ) + 1 ) e. ( ZZ>= ` M ) )
90 9 recnd 
 |-  ( ( ph /\ x e. Z ) -> B e. CC )
91 90 ralrimiva 
 |-  ( ph -> A. x e. Z B e. CC )
92 elfzuz 
 |-  ( k e. ( M ... ( ( |_ ` X ) + 1 ) ) -> k e. ( ZZ>= ` M ) )
93 92 2 eleqtrrdi 
 |-  ( k e. ( M ... ( ( |_ ` X ) + 1 ) ) -> k e. Z )
94 11 eleq1d 
 |-  ( x = k -> ( B e. CC <-> C e. CC ) )
95 94 rspccva 
 |-  ( ( A. x e. Z B e. CC /\ k e. Z ) -> C e. CC )
96 91 93 95 syl2an 
 |-  ( ( ph /\ k e. ( M ... ( ( |_ ` X ) + 1 ) ) ) -> C e. CC )
97 eqvisset 
 |-  ( k = ( ( |_ ` X ) + 1 ) -> ( ( |_ ` X ) + 1 ) e. _V )
98 eqeq2 
 |-  ( k = ( ( |_ ` X ) + 1 ) -> ( x = k <-> x = ( ( |_ ` X ) + 1 ) ) )
99 98 biimpar 
 |-  ( ( k = ( ( |_ ` X ) + 1 ) /\ x = ( ( |_ ` X ) + 1 ) ) -> x = k )
100 99 11 syl 
 |-  ( ( k = ( ( |_ ` X ) + 1 ) /\ x = ( ( |_ ` X ) + 1 ) ) -> B = C )
101 97 100 csbied 
 |-  ( k = ( ( |_ ` X ) + 1 ) -> [_ ( ( |_ ` X ) + 1 ) / x ]_ B = C )
102 101 eqcomd 
 |-  ( k = ( ( |_ ` X ) + 1 ) -> C = [_ ( ( |_ ` X ) + 1 ) / x ]_ B )
103 89 96 102 fsumm1 
 |-  ( ph -> sum_ k e. ( M ... ( ( |_ ` X ) + 1 ) ) C = ( sum_ k e. ( M ... ( ( ( |_ ` X ) + 1 ) - 1 ) ) C + [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
104 ax-1cn 
 |-  1 e. CC
105 pncan 
 |-  ( ( ( |_ ` X ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` X ) + 1 ) - 1 ) = ( |_ ` X ) )
106 52 104 105 sylancl 
 |-  ( ph -> ( ( ( |_ ` X ) + 1 ) - 1 ) = ( |_ ` X ) )
107 106 oveq2d 
 |-  ( ph -> ( M ... ( ( ( |_ ` X ) + 1 ) - 1 ) ) = ( M ... ( |_ ` X ) ) )
108 107 sumeq1d 
 |-  ( ph -> sum_ k e. ( M ... ( ( ( |_ ` X ) + 1 ) - 1 ) ) C = sum_ k e. ( M ... ( |_ ` X ) ) C )
109 108 oveq1d 
 |-  ( ph -> ( sum_ k e. ( M ... ( ( ( |_ ` X ) + 1 ) - 1 ) ) C + [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
110 103 109 eqtrd 
 |-  ( ph -> sum_ k e. ( M ... ( ( |_ ` X ) + 1 ) ) C = ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
111 110 adantr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> sum_ k e. ( M ... ( ( |_ ` X ) + 1 ) ) C = ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
112 48 oveq2d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( M ... ( |_ ` Y ) ) = ( M ... ( ( |_ ` X ) + 1 ) ) )
113 112 sumeq1d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> sum_ k e. ( M ... ( |_ ` Y ) ) C = sum_ k e. ( M ... ( ( |_ ` X ) + 1 ) ) C )
114 41 csbeq1d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> [_ Y / x ]_ B = [_ ( ( |_ ` X ) + 1 ) / x ]_ B )
115 114 oveq2d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ Y / x ]_ B ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
116 111 113 115 3eqtr4d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> sum_ k e. ( M ... ( |_ ` Y ) ) C = ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ Y / x ]_ B ) )
117 116 oveq1d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) = ( ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
118 fzfid 
 |-  ( ph -> ( M ... ( |_ ` X ) ) e. Fin )
119 elfzuz 
 |-  ( k e. ( M ... ( |_ ` X ) ) -> k e. ( ZZ>= ` M ) )
120 119 2 eleqtrrdi 
 |-  ( k e. ( M ... ( |_ ` X ) ) -> k e. Z )
121 91 120 95 syl2an 
 |-  ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. CC )
122 118 121 fsumcl 
 |-  ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. CC )
123 7 recnd 
 |-  ( ( ph /\ x e. S ) -> A e. CC )
124 123 ralrimiva 
 |-  ( ph -> A. x e. S A e. CC )
125 nfcsb1v 
 |-  F/_ x [_ Y / x ]_ A
126 125 nfel1 
 |-  F/ x [_ Y / x ]_ A e. CC
127 csbeq1a 
 |-  ( x = Y -> A = [_ Y / x ]_ A )
128 127 eleq1d 
 |-  ( x = Y -> ( A e. CC <-> [_ Y / x ]_ A e. CC ) )
129 126 128 rspc 
 |-  ( Y e. S -> ( A. x e. S A e. CC -> [_ Y / x ]_ A e. CC ) )
130 16 124 129 sylc 
 |-  ( ph -> [_ Y / x ]_ A e. CC )
131 122 64 130 addsubd 
 |-  ( ph -> ( ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ Y / x ]_ B ) - [_ Y / x ]_ A ) = ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) + [_ Y / x ]_ B ) )
132 131 adantr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( sum_ k e. ( M ... ( |_ ` X ) ) C + [_ Y / x ]_ B ) - [_ Y / x ]_ A ) = ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) + [_ Y / x ]_ B ) )
133 117 132 eqtrd 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) = ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) + [_ Y / x ]_ B ) )
134 72 133 oveq12d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) + ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) + [_ Y / x ]_ B ) ) )
135 53 64 mulcld 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
136 135 adantr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
137 64 adantr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> [_ Y / x ]_ B e. CC )
138 122 130 subcld 
 |-  ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) e. CC )
139 138 adantr 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) e. CC )
140 136 137 139 nppcan3d 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) + ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) + [_ Y / x ]_ B ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) ) )
141 134 140 eqtrd 
 |-  ( ( ph /\ Y = ( ( |_ ` X ) + 1 ) ) -> ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) ) )
142 peano2re 
 |-  ( ( |_ ` X ) e. RR -> ( ( |_ ` X ) + 1 ) e. RR )
143 27 142 syl 
 |-  ( ph -> ( ( |_ ` X ) + 1 ) e. RR )
144 23 143 leloed 
 |-  ( ph -> ( Y <_ ( ( |_ ` X ) + 1 ) <-> ( Y < ( ( |_ ` X ) + 1 ) \/ Y = ( ( |_ ` X ) + 1 ) ) ) )
145 20 144 mpbid 
 |-  ( ph -> ( Y < ( ( |_ ` X ) + 1 ) \/ Y = ( ( |_ ` X ) + 1 ) ) )
146 40 141 145 mpjaodan 
 |-  ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) ) )
147 ovex 
 |-  ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. _V
148 nfcv 
 |-  F/_ x Y
149 nfcv 
 |-  F/_ x ( Y - ( |_ ` Y ) )
150 nfcv 
 |-  F/_ x x.
151 149 150 59 nfov 
 |-  F/_ x ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B )
152 nfcv 
 |-  F/_ x +
153 nfcv 
 |-  F/_ x sum_ k e. ( M ... ( |_ ` Y ) ) C
154 nfcv 
 |-  F/_ x -
155 153 154 125 nfov 
 |-  F/_ x ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A )
156 151 152 155 nfov 
 |-  F/_ x ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
157 id 
 |-  ( x = Y -> x = Y )
158 fveq2 
 |-  ( x = Y -> ( |_ ` x ) = ( |_ ` Y ) )
159 157 158 oveq12d 
 |-  ( x = Y -> ( x - ( |_ ` x ) ) = ( Y - ( |_ ` Y ) ) )
160 159 61 oveq12d 
 |-  ( x = Y -> ( ( x - ( |_ ` x ) ) x. B ) = ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) )
161 158 oveq2d 
 |-  ( x = Y -> ( M ... ( |_ ` x ) ) = ( M ... ( |_ ` Y ) ) )
162 161 sumeq1d 
 |-  ( x = Y -> sum_ k e. ( M ... ( |_ ` x ) ) C = sum_ k e. ( M ... ( |_ ` Y ) ) C )
163 162 127 oveq12d 
 |-  ( x = Y -> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
164 160 163 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 ) ) )
165 148 156 164 14 fvmptf 
 |-  ( ( Y e. S /\ ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. _V ) -> ( H ` Y ) = ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
166 16 147 165 sylancl 
 |-  ( ph -> ( H ` Y ) = ( ( ( Y - ( |_ ` Y ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
167 135 130 122 subadd23d 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ Y / x ]_ A ) ) )
168 146 166 167 3eqtr4d 
 |-  ( ph -> ( H ` Y ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )