Theorem serzrelem 6999

Description: Lemma for serzre 7000, serzim 7001 and serzcj 7002.

Hypotheses

Ref	Expression
serzre.1	|- F e. V
serzre.2	|- G e. V
serzrelem.3	|- (k e. (ZZ>` M) -> ((F` k) e. CC /\ (G` k) = (H` (F` k))))
serzrelem.4	|- ((((<.M, + >. seq F)` m) e. CC /\ (F` (m + 1)) e. CC) -> (H` (((<.M, + >. seq F)` m) + (F` (m + 1)))) = ((H` ((<.M, + >. seq F)` m)) + (H` (F` (m + 1)))))

Assertion

Ref	Expression
serzrelem	|- (N e. (ZZ>` M) -> ((<.M, + >. seq G)` N) = (H` ((<.M, + >. seq F)` N)))

Distinct variable groups:   k,F,m   k,G,m   k,H,m   k,M,m

Proof of Theorem serzrelem

Step	Hyp	Ref	Expression
1		fveq2 3709	. . 3 |- (j = M -> ((<.M, + >. seq G)` j) = ((<.M, + >. seq G)` M))
2		fveq2 3709	. . . 4 |- (j = M -> ((<.M, + >. seq F)` j) = ((<.M, + >. seq F)` M))
3	2	fveq2d 3713	. . 3 |- (j = M -> (H` ((<.M, + >. seq F)` j)) = (H` ((<.M, + >. seq F)` M)))
4	1, 3	eqeq12d 1481	. 2 |- (j = M -> (((<.M, + >. seq G)` j) = (H` ((<.M, + >. seq F)` j)) <-> ((<.M, + >. seq G)` M) = (H` ((<.M, + >. seq F)` M))))
5		fveq2 3709	. . 3 |- (j = m -> ((<.M, + >. seq G)` j) = ((<.M, + >. seq G)` m))
6		fveq2 3709	. . . 4 |- (j = m -> ((<.M, + >. seq F)` j) = ((<.M, + >. seq F)` m))
7	6	fveq2d 3713	. . 3 |- (j = m -> (H` ((<.M, + >. seq F)` j)) = (H` ((<.M, + >. seq F)` m)))
8	5, 7	eqeq12d 1481	. 2 |- (j = m -> (((<.M, + >. seq G)` j) = (H` ((<.M, + >. seq F)` j)) <-> ((<.M, + >. seq G)` m) = (H` ((<.M, + >. seq F)` m))))
9		fveq2 3709	. . 3 |- (j = (m + 1) -> ((<.M, + >. seq G)` j) = ((<.M, + >. seq G)` (m + 1)))
10		fveq2 3709	. . . 4 |- (j = (m + 1) -> ((<.M, + >. seq F)` j) = ((<.M, + >. seq F)` (m + 1)))
11	10	fveq2d 3713	. . 3 |- (j = (m + 1) -> (H` ((<.M, + >. seq F)` j)) = (H` ((<.M, + >. seq F)` (m + 1))))
12	9, 11	eqeq12d 1481	. 2 |- (j = (m + 1) -> (((<.M, + >. seq G)` j) = (H` ((<.M, + >. seq F)` j)) <-> ((<.M, + >. seq G)` (m + 1)) = (H` ((<.M, + >. seq F)` (m + 1)))))
13		fveq2 3709	. . 3 |- (j = N -> ((<.M, + >. seq G)` j) = ((<.M, + >. seq G)` N))
14		fveq2 3709	. . . 4 |- (j = N -> ((<.M, + >. seq F)` j) = ((<.M, + >. seq F)` N))
15	14	fveq2d 3713	. . 3 |- (j = N -> (H` ((<.M, + >. seq F)` j)) = (H` ((<.M, + >. seq F)` N)))
16	13, 15	eqeq12d 1481	. 2 |- (j = N -> (((<.M, + >. seq G)` j) = (H` ((<.M, + >. seq F)` j)) <-> ((<.M, + >. seq G)` N) = (H` ((<.M, + >. seq F)` N))))
17		uzidt 6359	. . . 4 |- (M e. ZZ -> M e. (ZZ>` M))
18		fveq2 3709	. . . . . 6 |- (k = M -> (G` k) = (G` M))
19		fveq2 3709	. . . . . . 7 |- (k = M -> (F` k) = (F` M))
20	19	fveq2d 3713	. . . . . 6 |- (k = M -> (H` (F` k)) = (H` (F` M)))
21	18, 20	eqeq12d 1481	. . . . 5 |- (k = M -> ((G` k) = (H` (F` k)) <-> (G` M) = (H` (F` M))))
22		serzrelem.3	. . . . . 6 |- (k e. (ZZ>` M) -> ((F` k) e. CC /\ (G` k) = (H` (F` k))))
23	22	pm3.27d 325	. . . . 5 |- (k e. (ZZ>` M) -> (G` k) = (H` (F` k)))
24	21, 23	vtoclga 1843	. . . 4 |- (M e. (ZZ>` M) -> (G` M) = (H` (F` M)))
25	17, 24	syl 10	. . 3 |- (M e. ZZ -> (G` M) = (H` (F` M)))
26		addex 5289	. . . 4 |- + e. V
27		serzre.2	. . . 4 |- G e. V
28	26, 27	seqz1 6479	. . 3 |- (M e. ZZ -> ((<.M, + >. seq G)` M) = (G` M))
29		serzre.1	. . . . 5 |- F e. V
30	26, 29	seqz1 6479	. . . 4 |- (M e. ZZ -> ((<.M, + >. seq F)` M) = (F` M))
31	30	fveq2d 3713	. . 3 |- (M e. ZZ -> (H` ((<.M, + >. seq F)` M)) = (H` (F` M)))
32	25, 28, 31	3eqtr4d 1509	. 2 |- (M e. ZZ -> ((<.M, + >. seq G)` M) = (H` ((<.M, + >. seq F)` M)))
33	26, 27	seqzp1 6480	. . . . 5 |- (m e. (ZZ>` M) -> ((<.M, + >. seq G)` (m + 1)) = (((<.M, + >. seq G)` m) + (G` (m + 1))))
34		opreq1 3953	. . . . 5 |- (((<.M, + >. seq G)` m) = (H` ((<.M, + >. seq F)` m)) -> (((<.M, + >. seq G)` m) + (G` (m + 1))) = ((H` ((<.M, + >. seq F)` m)) + (G` (m + 1))))
35	33, 34	sylan9eq 1519	. . . 4 |- ((m e. (ZZ>` M) /\ ((<.M, + >. seq G)` m) = (H` ((<.M, + >. seq F)` m))) -> ((<.M, + >. seq G)` (m + 1)) = ((H` ((<.M, + >. seq F)` m)) + (G` (m + 1))))
36		serzrelem.4	. . . . . . 7 |- ((((<.M, + >. seq F)` m) e. CC /\ (F` (m + 1)) e. CC) -> (H` (((<.M, + >. seq F)` m) + (F` (m + 1)))) = ((H` ((<.M, + >. seq F)` m)) + (H` (F` (m + 1)))))
37	22	pm3.26d 321	. . . . . . . . 9 |- (k e. (ZZ>` M) -> (F` k) e. CC)
38	37	rgen 1690	. . . . . . . 8 |- A.k e. (ZZ>` M)(F` k) e. CC
39	29	serzcl2t 6987	. . . . . . . 8 |- ((m e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> ((<.M, + >. seq F)` m) e. CC)
40	38, 39	mpan2 694	. . . . . . 7 |- (m e. (ZZ>` M) -> ((<.M, + >. seq F)` m) e. CC)
41		peano2uz 6379	. . . . . . . 8 |- (m e. (ZZ>` M) -> (m + 1) e. (ZZ>` M))
42		fveq2 3709	. . . . . . . . . 10 |- (k = (m + 1) -> (F` k) = (F` (m + 1)))
43	42	eleq1d 1532	. . . . . . . . 9 |- (k = (m + 1) -> ((F` k) e. CC <-> (F` (m + 1)) e. CC))
44	43, 37	vtoclga 1843	. . . . . . . 8 |- ((m + 1) e. (ZZ>` M) -> (F` (m + 1)) e. CC)
45	41, 44	syl 10	. . . . . . 7 |- (m e. (ZZ>` M) -> (F` (m + 1)) e. CC)
46	36, 40, 45	sylanc 471	. . . . . 6 |- (m e. (ZZ>` M) -> (H` (((<.M, + >. seq F)` m) + (F` (m + 1)))) = ((H` ((<.M, + >. seq F)` m)) + (H` (F` (m + 1)))))
47	26, 29	seqzp1 6480	. . . . . . 7 |- (m e. (ZZ>` M) -> ((<.M, + >. seq F)` (m + 1)) = (((<.M, + >. seq F)` m) + (F` (m + 1))))
48	47	fveq2d 3713	. . . . . 6 |- (m e. (ZZ>` M) -> (H` ((<.M, + >. seq F)` (m + 1))) = (H` (((<.M, + >. seq F)` m)