fsumcvg2

Description: The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014)

	Ref	Expression
Hypotheses	fsumsers.1	\|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
	fsumsers.2	\|- ( ph -> N e. ( ZZ>= ` M ) )
	fsumsers.3	\|- ( ( ph /\ k e. A ) -> B e. CC )
	fsumsers.4	\|- ( ph -> A C_ ( M ... N ) )
Assertion	fsumcvg2	\|- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )

Proof

Step	Hyp	Ref	Expression
1		fsumsers.1	\|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
2		fsumsers.2	\|- ( ph -> N e. ( ZZ>= ` M ) )
3		fsumsers.3	\|- ( ( ph /\ k e. A ) -> B e. CC )
4		fsumsers.4	\|- ( ph -> A C_ ( M ... N ) )
5		nfcv	\|- F/_ m if ( k e. A , B , 0 )
6		nfv	\|- F/ k m e. A
7		nfcsb1v	\|- F/_ k [_ m / k ]_ B
8		nfcv	\|- F/_ k 0
9	6 7 8	nfif	\|- F/_ k if ( m e. A , [_ m / k ]_ B , 0 )
10		eleq1w	\|- ( k = m -> ( k e. A <-> m e. A ) )
11		csbeq1a	\|- ( k = m -> B = [_ m / k ]_ B )
12	10 11	ifbieq1d	\|- ( k = m -> if ( k e. A , B , 0 ) = if ( m e. A , [_ m / k ]_ B , 0 ) )
13	5 9 12	cbvmpt	\|- ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) = ( m e. ZZ \|-> if ( m e. A , [_ m / k ]_ B , 0 ) )
14	3	ralrimiva	\|- ( ph -> A. k e. A B e. CC )
15	7	nfel1	\|- F/ k [_ m / k ]_ B e. CC
16	11	eleq1d	\|- ( k = m -> ( B e. CC <-> [_ m / k ]_ B e. CC ) )
17	15 16	rspc	\|- ( m e. A -> ( A. k e. A B e. CC -> [_ m / k ]_ B e. CC ) )
18	14 17	mpan9	\|- ( ( ph /\ m e. A ) -> [_ m / k ]_ B e. CC )
19	13 18 2 4	fsumcvg	\|- ( ph -> seq M ( + , ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ) ~~> ( seq M ( + , ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ) ` N ) )
20		eluzel2	\|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
21	2 20	syl	\|- ( ph -> M e. ZZ )
22		eluzelz	\|- ( k e. ( ZZ>= ` M ) -> k e. ZZ )
23		iftrue	\|- ( k e. A -> if ( k e. A , B , 0 ) = B )
24	23	adantl	\|- ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) = B )
25	24 3	eqeltrd	\|- ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) e. CC )
26	25	ex	\|- ( ph -> ( k e. A -> if ( k e. A , B , 0 ) e. CC ) )
27		iffalse	\|- ( -. k e. A -> if ( k e. A , B , 0 ) = 0 )
28		0cn	\|- 0 e. CC
29	27 28	eqeltrdi	\|- ( -. k e. A -> if ( k e. A , B , 0 ) e. CC )
30	26 29	pm2.61d1	\|- ( ph -> if ( k e. A , B , 0 ) e. CC )
31		eqid	\|- ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) = ( k e. ZZ \|-> if ( k e. A , B , 0 ) )
32	31	fvmpt2	\|- ( ( k e. ZZ /\ if ( k e. A , B , 0 ) e. CC ) -> ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` k ) = if ( k e. A , B , 0 ) )
33	22 30 32	syl2anr	\|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` k ) = if ( k e. A , B , 0 ) )
34	1 33	eqtr4d	\|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` k ) )
35	34	ralrimiva	\|- ( ph -> A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` k ) )
36		nffvmpt1	\|- F/_ k ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` n )
37	36	nfeq2	\|- F/ k ( F ` n ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` n )
38		fveq2	\|- ( k = n -> ( F ` k ) = ( F ` n ) )
39		fveq2	\|- ( k = n -> ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` k ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` n ) )
40	38 39	eqeq12d	\|- ( k = n -> ( ( F ` k ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` k ) <-> ( F ` n ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` n ) ) )
41	37 40	rspc	\|- ( n e. ( ZZ>= ` M ) -> ( A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` k ) -> ( F ` n ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` n ) ) )
42	35 41	mpan9	\|- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( F ` n ) = ( ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ` n ) )
43	21 42	seqfeq	\|- ( ph -> seq M ( + , F ) = seq M ( + , ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ) )
44	43	fveq1d	\|- ( ph -> ( seq M ( + , F ) ` N ) = ( seq M ( + , ( k e. ZZ \|-> if ( k e. A , B , 0 ) ) ) ` N ) )
45	19 43 44	3brtr4d	\|- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )

Metamath Proof Explorer

Theorem fsumcvg2

Proof