Theorem dvfsumrlimf

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 )
	dvfsumrlimf.g	|- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
Assertion	dvfsumrlimf	|- ( ph -> G : S --> RR )

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