Theorem seqzfveq 6486

Description: Equality theorem for the recursive sequence builder.

Hypotheses

Ref	Expression
seqzfveq.1	|- S e. V
seqzfveq.2	|- F e. V
seqzfveq.3	|- G e. V

Assertion

Ref	Expression
seqzfveq	|- ((N e. (ZZ>` M) /\ A.k e. (M...N)(F` k) = (G` k)) -> ((<.M, S>. seq F)` N) = ((<.M, S>. seq G)` N))

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

Proof of Theorem seqzfveq

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . 5 |- (j = M -> (M...j) = (M...M))
2	1	raleq1d 1781	. . . 4 |- (j = M -> (A.k e. (M...j)(F` k) = (G` k) <-> A.k e. (M...M)(F` k) = (G` k)))
3		fveq2 3709	. . . . 5 |- (j = M -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` M))
4		fveq2 3709	. . . . 5 |- (j = M -> ((<.M, S>. seq G)` j) = ((<.M, S>. seq G)` M))
5	3, 4	eqeq12d 1481	. . . 4 |- (j = M -> (((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j) <-> ((<.M, S>. seq F)` M) = ((<.M, S>. seq G)` M)))
6	2, 5	imbi12d 624	. . 3 |- (j = M -> ((A.k e. (M...j)(F` k) = (G` k) -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j)) <-> (A.k e. (M...M)(F` k) = (G` k) -> ((<.M, S>. seq F)` M) = ((<.M, S>. seq G)` M))))
7		opreq2 3954	. . . . 5 |- (j = m -> (M...j) = (M...m))
8	7	raleq1d 1781	. . . 4 |- (j = m -> (A.k e. (M...j)(F` k) = (G` k) <-> A.k e. (M...m)(F` k) = (G` k)))
9		fveq2 3709	. . . . 5 |- (j = m -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` m))
10		fveq2 3709	. . . . 5 |- (j = m -> ((<.M, S>. seq G)` j) = ((<.M, S>. seq G)` m))
11	9, 10	eqeq12d 1481	. . . 4 |- (j = m -> (((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j) <-> ((<.M, S>. seq F)` m) = ((<.M, S>. seq G)` m)))
12	8, 11	imbi12d 624	. . 3 |- (j = m -> ((A.k e. (M...j)(F` k) = (G` k) -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j)) <-> (A.k e. (M...m)(F` k) = (G` k) -> ((<.M, S>. seq F)` m) = ((<.M, S>. seq G)` m))))
13		opreq2 3954	. . . . 5 |- (j = (m + 1) -> (M...j) = (M...(m + 1)))
14	13	raleq1d 1781	. . . 4 |- (j = (m + 1) -> (A.k e. (M...j)(F` k) = (G` k) <-> A.k e. (M...(m + 1))(F` k) = (G` k)))
15		fveq2 3709	. . . . 5 |- (j = (m + 1) -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` (m + 1)))
16		fveq2 3709	. . . . 5 |- (j = (m + 1) -> ((<.M, S>. seq G)` j) = ((<.M, S>. seq G)` (m + 1)))
17	15, 16	eqeq12d 1481	. . . 4 |- (j = (m + 1) -> (((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j) <-> ((<.M, S>. seq F)` (m + 1)) = ((<.M, S>. seq G)` (m + 1))))
18	14, 17	imbi12d 624	. . 3 |- (j = (m + 1) -> ((A.k e. (M...j)(F` k) = (G` k) -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j)) <-> (A.k e. (M...(m + 1))(F` k) = (G` k) -> ((<.M, S>. seq F)` (m + 1)) = ((<.M, S>. seq G)` (m + 1)))))
19		opreq2 3954	. . . . 5 |- (j = N -> (M...j) = (M...N))
20	19	raleq1d 1781	. . . 4 |- (j = N -> (A.k e. (M...j)(F` k) = (G` k) <-> A.k e. (M...N)(F` k) = (G` k)))
21		fveq2 3709	. . . . 5 |- (j = N -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` N))
22		fveq2 3709	. . . . 5 |- (j = N -> ((<.M, S>. seq G)` j) = ((<.M, S>. seq G)` N))
23	21, 22	eqeq12d 1481	. . . 4 |- (j = N -> (((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j) <-> ((<.M, S>. seq F)` N) = ((<.M, S>. seq G)` N)))
24	20, 23	imbi12d 624	. . 3 |- (j = N -> ((A.k e. (M...j)(F` k) = (G` k) -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq G)` j)) <-> (A.k e. (M...N)(F` k) = (G` k) -> ((<.M, S>. seq F)` N) = ((<.M, S>. seq G)` N))))
25		fveq2 3709	. . . . . . . 8 |- (k = M -> (F` k) = (F` M))
26		fveq2 3709	. . . . . . . 8 |- (k = M -> (G` k) = (G` M))
27	25, 26	eqeq12d 1481	. . . . . . 7 |- (k = M -> ((F` k) = (G` k) <-> (F` M) = (G` M)))
28	27	rcla4va 1866	. . . . . 6 |- ((M e. (M...M) /\ A.k e. (M...M)(F` k) = (G` k)) -> (F` M) = (G` M))
29		elfz3t 6423	. . . . . 6 |- (M e. ZZ -> M e. (M...M))
30	28, 29	sylan 448	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(F` k) = (G` k)) -> (F` M) = (G` M))
31		seqzfveq.1	. . . . . . 7 |- S e. V
32		seqzfveq.2	. . . . . . 7 |- F e. V
33	31, 32	seqz1 6479	. . . . . 6 |- (M e. ZZ -> ((<.M, S>. seq F)` M) = (F` M))
34	33	adantr 389	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(F` k) = (G` k)) -> ((<.M, S>. seq F)` M) = (F` M))
35		seqzfveq.3	. . . . . . 7 |- G e. V
36	31, 35	seqz1 6479	. . . . . 6 |- (M e. ZZ -> ((<.M, S>. seq G)` M) = (G` M))
37	36	adantr 389	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(F` k) = (G` k)) -> ((<.M, S>. seq G)` M) = (G` M))
38	30, 34, 37	3eqtr4d 1509	. . . 4 |- ((M e. ZZ /\ A.k e. (M...M)(F` k) = (G` k)) -> ((<.M, S>. seq F)` M) = ((<.M, S>. seq G)` M))
39	38	ex 373	. . 3 |- (M e. ZZ -> (A.k e. (M...M)(F` k) = (G` k) -> ((<.M, S>. seq F)` M) = ((<.M, S>. seq G)` M)))
40		fzssp1t 6438	. . . . . . . . 9 |- ((M e. ZZ /\ m e. ZZ) -> (M...m) (_ (M...(m + 1)))
41		eluzel2 6356	. . . . . . . . 9 |- (m e. (ZZ>` M) -> M e. ZZ)
42		eluzelz 6355	. . . . . . . . 9 |- (m e. (ZZ>` M) -> m e. ZZ)
43	40, 41, 42	sylanc 471	. . . . . . . 8 |- (m e. (ZZ>` M) -> (M...m) (_ (M...(m + 1)))
44	43	sseld 2057	. . . . . . 7 |- (m e. (ZZ>` M) -> (k e. (M...m) -> k e. (M...(m + 1))))
45	44	imim1d 28	. . . . . 6 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> (F` k) = (G` k)) -> (k e. (M...m) -> (F` k) = (G` k))))
46	45	r19.20dv2 1703	. . . . 5 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))(F` k) = (G` k) -> A.k e. (M...m)(F` k) = (G` k)))
47	46	imim1d 28	. . . 4 |- (m e. (ZZ>` M) -> ((A.k e. (M...m)(F` k) = (G` k) -> ((<.M