Theorem ser1add2 6338

Description: The sum of two infinite series.

Hypotheses

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

Assertion

Ref	Expression
ser1add2	|- (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 ser1add2

Step	Hyp	Ref	Expression
1		nnret 5929	. . . 4 |- (N e. NN -> N e. RR)
2		leidt 5531	. . . 4 |- (N e. RR -> N <_ N)
3	1, 2	syl 10	. . 3 |- (N e. NN -> N <_ N)
4		breq1 2622	. . . . . 6 |- (j = 1 -> (j <_ N <-> 1 <_ N))
5	4	anbi2d 616	. . . . 5 |- (j = 1 -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ 1 <_ N)))
6		fveq2 3724	. . . . . 6 |- (j = 1 -> (( + seq1 H)` j) = (( + seq1 H)` 1))
7		fveq2 3724	. . . . . . 7 |- (j = 1 -> (( + seq1 F)` j) = (( + seq1 F)` 1))
8		fveq2 3724	. . . . . . 7 |- (j = 1 -> (( + seq1 G)` j) = (( + seq1 G)` 1))
9	7, 8	opreq12d 3978	. . . . . 6 |- (j = 1 -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` 1) + (( + seq1 G)` 1)))
10	6, 9	eqeq12d 1489	. . . . 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 626	. . . 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 2622	. . . . . 6 |- (j = m -> (j <_ N <-> m <_ N))
13	12	anbi2d 616	. . . . 5 |- (j = m -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ m <_ N)))
14		fveq2 3724	. . . . . 6 |- (j = m -> (( + seq1 H)` j) = (( + seq1 H)` m))
15		fveq2 3724	. . . . . . 7 |- (j = m -> (( + seq1 F)` j) = (( + seq1 F)` m))
16		fveq2 3724	. . . . . . 7 |- (j = m -> (( + seq1 G)` j) = (( + seq1 G)` m))
17	15, 16	opreq12d 3978	. . . . . 6 |- (j = m -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` m) + (( + seq1 G)` m)))
18	14, 17	eqeq12d 1489	. . . . 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 626	. . . 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 2622	. . . . . 6 |- (j = (m + 1) -> (j <_ N <-> (m + 1) <_ N))
21	20	anbi2d 616	. . . . 5 |- (j = (m + 1) -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ (m + 1) <_ N)))
22		fveq2 3724	. . . . . 6 |- (j = (m + 1) -> (( + seq1 H)` j) = (( + seq1 H)` (m + 1)))
23		fveq2 3724	. . . . . . 7 |- (j = (m + 1) -> (( + seq1 F)` j) = (( + seq1 F)` (m + 1)))
24		fveq2 3724	. . . . . . 7 |- (j = (m + 1) -> (( + seq1 G)` j) = (( + seq1 G)` (m + 1)))
25	23, 24	opreq12d 3978	. . . . . 6 |- (j = (m + 1) -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` (m + 1)) + (( + seq1 G)` (m + 1))))
26	22, 25	eqeq12d 1489	. . . . 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 626	. . . 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 2622	. . . . . 6 |- (j = N -> (j <_ N <-> N <_ N))
29	28	anbi2d 616	. . . . 5 |- (j = N -> ((N e. NN /\ j <_ N) <-> (N e. NN /\ N <_ N)))
30		fveq2 3724	. . . . . 6 |- (j = N -> (( + seq1 H)` j) = (( + seq1 H)` N))
31		fveq2 3724	. . . . . . 7 |- (j = N -> (( + seq1 F)` j) = (( + seq1 F)` N))
32		fveq2 3724	. . . . . . 7 |- (j = N -> (( + seq1 G)` j) = (( + seq1 G)` N))
33	31, 32	opreq12d 3978	. . . . . 6 |- (j = N -> ((( + seq1 F)` j) + (( + seq1 G)` j)) = ((( + seq1 F)` N) + (( + seq1 G)` N)))
34	30, 33	eqeq12d 1489	. . . . 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 626	. . . 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 5934	. . . . . 6 |- 1 e. NN
37		breq1 2622	. . . . . . . . 9 |- (k = 1 -> (k <_ N <-> 1 <_ N))
38	37	anbi2d 616	. . . . . . . 8 |- (k = 1 -> ((N e. NN /\ k <_ N) <-> (N e. NN /\ 1 <_ N)))
39		fveq2 3724	. . . . . . . . 9 |- (k = 1 -> (H` k) = (H` 1))
40		fveq2 3724	. . . . . . . . . 10 |- (k = 1 -> (F` k) = (F` 1))
41		fveq2 3724	. . . . . . . . . 10 |- (k = 1 -> (G` k) = (G` 1))
42	40, 41	opreq12d 3978	. . . . . . . . 9 |- (k = 1 -> ((F` k) + (G` k)) = ((F` 1) + (G` 1)))
43	39, 42	eqeq12d 1489	. . . . . . . 8 |- (k = 1 -> ((H` k) = ((F` k) + (G` k)) <-> (H` 1) = ((F` 1) + (G` 1))))
44	38, 43	imbi12d 626	. . . . . . 7 |- (k = 1 -> (((N e. NN /\ k <_ N) -> (H` k) = ((F` k) + (G` k))) <-> ((N e. NN /\ 1 <_ N) -> (H` 1) = ((F` 1) + (G` 1)))))
45		ser1add2.4	. . . . . . . 8 |- ((k e. NN /\ N e. NN /\ k <_ N) -> (H` k) = ((F` k) + (G` k)))
46	45	3expib 836	. . . . . . 7 |- (k e. NN -> ((N e. NN /\ k <_ N) -> (H` k) = ((F` k) + (G` k))))
47	44, 46	vtoclga 1852	. . . . . 6 |- (1 e. NN -> ((N e. NN /\ 1 <_ N) -> (H` 1) = ((F` 1) + (G` 1))))
48	36, 47	ax-mp 7	. . . . 5 |- ((N e. NN /\ 1 <_ N) -> (H` 1) = ((F` 1) + (G` 1)))
49		addex 5317	. . . . . 6 |- + e. V
50		ser1add2.3	. . . . . 6 |- H e. V
51	49, 50	seq11 6317	. . . . 5 |- (( + seq1 H)` 1) = (H` 1)
52		ser1add2.1	. . . . . . . 8 |- F:NN-->CC
53		nnex 5933	. . . . . . . 8 |- NN e. V
54		fex 3652	. . . . . . . 8 |- ((F:NN-->CC /\ NN e. V) -> F e. V)
55	52, 53, 54	mp2an 697	. . . . . . 7 |- F e. V
56	49, 55	seq11 6317	. . . . . 6 |-