Theorem ser1add 6276

Description: The sum of two infinite series.

Hypotheses

Ref	Expression
ser1add.1	|- F:NN-->CC
ser1add.2	|- G:NN-->CC
ser1add.3	|- H e. V
ser1add.4	|- ((k e. NN /\ k <_ N) -> (H` k) = ((F` k) + (G` k)))

Assertion

Ref	Expression
ser1add	|- (N e. NN -> (( + seq1 H)` N) = ((( + seq1 F)` N) + (( + seq1 G)` N)))

Distinct variable groups:   k,F   k,G   k,H   k,N

Proof of Theorem ser1add

Step	Hyp	Ref	Expression
1		nnret 5877	. . . 4 |- (N e. NN -> N e. RR)
2		leidt 5504	. . . 4 |- (N e. RR -> N <_ N)
3	1, 2	syl 10	. . 3 |- (N e. NN -> N <_ N)
4		breq1 2612	. . . . . 6 |- (j = 1 -> (j <_ N <-> 1 <_ N))
5	4	anbi2d 614	. . . . 5 |- (j = 1 -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ 1 <_ N)))
6		fveq2 3709	. . . . . 6 |- (j = 1 -> (( + seq1 H)` j) = (( + seq1 H)` 1))
7		fveq2 3709	. . . . . . 7 |- (j = 1 -> (( + seq1 F)` j) = (( + seq1 F)` 1))
8		fveq2 3709	. . . . . . 7 |- (j = 1 -> (( + seq1 G)` j) = (( + seq1 G)` 1))
9	7, 8	opreq12d 3963	. . . . . 6 |- (j = 1 -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` 1) + (( + seq1 G)` 1)))
10	6, 9	eqeq12d 1481	. . . . 5 |- (j = 1 -> ((( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j)) <-> (( + seq1 H)` 1) = ((( + seq1 F)` 1) + (( + seq1 G)` 1))))
11	5, 10	imbi12d 624	. . . 4 |- (j = 1 -> (((N e. NN /\ j <_ N) -> (( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j))) <-> ((N e. NN /\ 1 <_ N) -> (( + seq1 H)` 1) = ((( + seq1 F)` 1) + (( + seq1 G)` 1)))))
12		breq1 2612	. . . . . 6 |- (j = m -> (j <_ N <-> m <_ N))
13	12	anbi2d 614	. . . . 5 |- (j = m -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ m <_ N)))
14		fveq2 3709	. . . . . 6 |- (j = m -> (( + seq1 H)` j) = (( + seq1 H)` m))
15		fveq2 3709	. . . . . . 7 |- (j = m -> (( + seq1 F)` j) = (( + seq1 F)` m))
16		fveq2 3709	. . . . . . 7 |- (j = m -> (( + seq1 G)` j) = (( + seq1 G)` m))
17	15, 16	opreq12d 3963	. . . . . 6 |- (j = m -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` m) + (( + seq1 G)` m)))
18	14, 17	eqeq12d 1481	. . . . 5 |- (j = m -> ((( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j)) <-> (( + seq1 H)` m) = ((( + seq1 F)` m) + (( + seq1 G)` m))))
19	13, 18	imbi12d 624	. . . 4 |- (j = m -> (((N e. NN /\ j <_ N) -> (( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j))) <-> ((N e. NN /\ m <_ N) -> (( + seq1 H)` m) = ((( + seq1 F)` m) + (( + seq1 G)` m)))))
20		breq1 2612	. . . . . 6 |- (j = (m + 1) -> (j <_ N <-> (m + 1) <_ N))
21	20	anbi2d 614	. . . . 5 |- (j = (m + 1) -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ (m + 1) <_ N)))
22		fveq2 3709	. . . . . 6 |- (j = (m + 1) -> (( + seq1 H)` j) = (( + seq1 H)` (m + 1)))
23		fveq2 3709	. . . . . . 7 |- (j = (m + 1) -> (( + seq1 F)` j) = (( + seq1 F)` (m + 1)))
24		fveq2 3709	. . . . . . 7 |- (j = (m + 1) -> (( + seq1 G)` j) = (( + seq1 G)` (m + 1)))
25	23, 24	opreq12d 3963	. . . . . 6 |- (j = (m + 1) -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` (m + 1)) + (( + seq1 G)` (m + 1))))
26	22, 25	eqeq12d 1481	. . . . 5 |- (j = (m + 1) -> ((( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j)) <-> (( + seq1 H)` (m + 1)) = ((( + seq1 F)` (m + 1)) + (( + seq1 G)` (m + 1)))))
27	21, 26	imbi12d 624	. . . 4 |- (j = (m + 1) -> (((N e. NN /\ j <_ N) -> (( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j))) <-> ((N e. NN /\ (m + 1) <_ N) -> (( + seq1 H)` (m + 1)) = ((( + seq1 F)` (m + 1)) + (( + seq1 G)` (m + 1))))))
28		breq1 2612	. . . . . 6 |- (j = N -> (j <_ N <-> N <_ N))
29	28	anbi2d 614	. . . . 5 |- (j = N -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ N <_ N)))
30		fveq2 3709	. . . . . 6 |- (j = N -> (( + seq1 H)` j) = (( + seq1 H)` N))
31		fveq2 3709	. . . . . . 7 |- (j = N -> (( + seq1 F)` j) = (( + seq1 F)` N))
32		fveq2 3709	. . . . . . 7 |- (j = N -> (( + seq1 G)` j) = (( + seq1 G)` N))
33	31, 32	opreq12d 3963	. . . . . 6 |- (j = N -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` N) + (( + seq1 G)` N)))
34	30, 33	eqeq12d 1481	. . . . 5 |- (j = N -> ((( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j)) <-> (( + seq1 H)` N) = ((( + seq1 F)` N) + (( + seq1 G)` N))))
35	29, 34	imbi12d 624	. . . 4 |- (j = N -> (((N e. NN /\ j <_ N) -> (( + seq1 H)` j) = ((( + seq1 F)` j) + (( + seq1 G)` j))) <-> ((N e. NN /\ N <_ N) -> (( + seq1 H)` N) = ((( + seq1 F)` N) + (( + seq1 G)` N)))))
36		1nn 5882	. . . . . . 7 |- 1 e. NN
37		breq1 2612	. . . . . . . . 9 |- (k = 1 -> (k <_ N <-> 1 <_ N))
38		fveq2 3709	. . . . . . . . . 10 |- (k = 1 -> (H` k) = (H` 1))
39		fveq2 3709	. . . . . . . . . . 11 |- (k = 1 -> (F` k) = (F` 1))
40		fveq2 3709	. . . . . . . . . . 11 |- (k = 1 -> (G` k) = (G` 1))
41	39, 40	opreq12d 3963	. . . . . . . . . 10 |- (k = 1 -> ((F` k) + (G` k)) = ((F` 1) + (G` 1)))
42	38, 41	eqeq12d 1481	. . . . . . . . 9 |- (k = 1 -> ((H` k) = ((F` k) + (G` k)) <-> (H` 1) = ((F` 1) + (G` 1))))
43	37, 42	imbi12d 624	. . . . . . . 8 |- (k = 1 -> ((k <_ N -> (H` k) = ((F` k) + (G` k))) <-> (1 <_ N -> (H` 1) = ((F` 1) + (G` 1)))))
44		ser1add.4	. . . . . . . . 9 |- ((k e. NN /\ k <_ N) -> (H` k) = ((F` k) + (G` k)))
45	44	ex 373	. . . . . . . 8 |- (k e. NN -> (k <_ N -> (H` k) = ((F` k) + (G` k))))
46	43, 45	vtoclga 1843	. . . . . . 7 |- (1 e. NN -> (1 <_ N -> (H` 1) = ((F` 1) + (G` 1))))
47	36, 46	ax-mp 7	. . . . . 6 |- (1 <_ N -> (H` 1) = ((F` 1) + (G` 1)))
48		addex 5289	. . . . . . 7 |- + e. V
49		ser1add.3	. . . . . . 7 |- H e. V
50	48, 49	seq11 6254	. . . . . 6 |- (( + seq1 H)` 1) = (H` 1)
51		ser1add.1	. . . . . . . . 9 |- F:NN-->CC
52		nnex 5881	. . . . . . . . 9 |- NN e. V
53		fex 3637	. . . . . . . . 9 |- ((F:NN-->CC /\ NN e. V) -> F e. V)
54	51, 52, 53	mp2an 695	. . . . . . . 8 |- F e. V
55	48, 54	seq11 6254	. . . . . . 7 |- (( + seq1 F)` 1) = (F` 1)
56		ser1add.2	. . . . . . . . 9 |- G:NN-->CC
57		fex 3637	. . . . . . . . 9 |- ((G:NN-->CC /\ NN e. V) -> G e. V)
58	56, 52, 57	mp2an 695	. . . . . . . 8 |- G e. V
59	48, 58	seq11 6254	. . . . . . 7 |- (( + seq1 G)` 1) = (