| 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 |
|
dvfsumrlimf.g |
|- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) |
| 13 |
|
fzfid |
|- ( ( ph /\ x e. S ) -> ( M ... ( |_ ` x ) ) e. Fin ) |
| 14 |
9
|
ralrimiva |
|- ( ph -> A. x e. Z B e. RR ) |
| 15 |
14
|
adantr |
|- ( ( ph /\ x e. S ) -> A. x e. Z B e. RR ) |
| 16 |
|
elfzuz |
|- ( k e. ( M ... ( |_ ` x ) ) -> k e. ( ZZ>= ` M ) ) |
| 17 |
16 2
|
eleqtrrdi |
|- ( k e. ( M ... ( |_ ` x ) ) -> k e. Z ) |
| 18 |
11
|
eleq1d |
|- ( x = k -> ( B e. RR <-> C e. RR ) ) |
| 19 |
18
|
rspccva |
|- ( ( A. x e. Z B e. RR /\ k e. Z ) -> C e. RR ) |
| 20 |
15 17 19
|
syl2an |
|- ( ( ( ph /\ x e. S ) /\ k e. ( M ... ( |_ ` x ) ) ) -> C e. RR ) |
| 21 |
13 20
|
fsumrecl |
|- ( ( ph /\ x e. S ) -> sum_ k e. ( M ... ( |_ ` x ) ) C e. RR ) |
| 22 |
21 7
|
resubcld |
|- ( ( ph /\ x e. S ) -> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) e. RR ) |
| 23 |
22 12
|
fmptd |
|- ( ph -> G : S --> RR ) |