Metamath Proof Explorer


Theorem 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 φ k M F k = if k A B 0
fsumsers.2 φ N M
fsumsers.3 φ k A B
fsumsers.4 φ A M N
Assertion fsumcvg2 φ seq M + F seq M + F N

Proof

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