Theorem seqzval2t 6553

Description: Value of the arbitrary-based recursive sequence builder operation.

Hypotheses

Ref	Expression
seq0val.1	|- S e. V
seq0val.2	|- F e. V

Assertion

Ref	Expression
seqzval2t	|- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ((<.M, S>. seq F)` N) = (((S seq0 (F shift -uM)) shift M)` N))

Proof of Theorem seqzval2t

Step	Hyp	Ref	Expression
1		zcnt 6140	. . . . 5 |- (N e. ZZ -> N e. CC)
2		oprex 3983	. . . . . 6 |- (M - 1) e. V
3		oprex 3983	. . . . . . 7 |- (S seq1 (F shift (1 - M))) e. V
4	3	shftvalt 6346	. . . . . 6 |- (((M - 1) e. V /\ N e. CC) -> (((S seq1 (F shift (1 - M))) shift (M - 1))` N) = ((S seq1 (F shift (1 - M)))` (N - (M - 1))))
5	2, 4	mpan 695	. . . . 5 |- (N e. CC -> (((S seq1 (F shift (1 - M))) shift (M - 1))` N) = ((S seq1 (F shift (1 - M)))` (N - (M - 1))))
6	1, 5	syl 10	. . . 4 |- (N e. ZZ -> (((S seq1 (F shift (1 - M))) shift (M - 1))` N) = ((S seq1 (F shift (1 - M)))` (N - (M - 1))))
7	6	3ad2ant2 801	. . 3 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (((S seq1 (F shift (1 - M))) shift (M - 1))` N) = ((S seq1 (F shift (1 - M)))` (N - (M - 1))))
8		zcnt 6140	. . . . . . . 8 |- (M e. ZZ -> M e. CC)
9		negclt 5368	. . . . . . . . . 10 |- (M e. CC -> -uM e. CC)
10		ax1cn 5269	. . . . . . . . . . 11 |- 1 e. CC
11		seq0val.2	. . . . . . . . . . . 12 |- F e. V
12	11	2shft 6352	. . . . . . . . . . 11 |- ((-uM e. CC /\ 1 e. CC) -> ((F shift -uM) shift 1) = (F shift (-uM + 1)))
13	10, 12	mpan2 696	. . . . . . . . . 10 |- (-uM e. CC -> ((F shift -uM) shift 1) = (F shift (-uM + 1)))
14	9, 13	syl 10	. . . . . . . . 9 |- (M e. CC -> ((F shift -uM) shift 1) = (F shift (-uM + 1)))
15		axaddcom 5275	. . . . . . . . . . . . 13 |- ((-uM e. CC /\ 1 e. CC) -> (-uM + 1) = (1 + -uM))
16	10, 15	mpan2 696	. . . . . . . . . . . 12 |- (-uM e. CC -> (-uM + 1) = (1 + -uM))
17	9, 16	syl 10	. . . . . . . . . . 11 |- (M e. CC -> (-uM + 1) = (1 + -uM))
18		negsubt 5382	. . . . . . . . . . . 12 |- ((1 e. CC /\ M e. CC) -> (1 + -uM) = (1 - M))
19	10, 18	mpan 695	. . . . . . . . . . 11 |- (M e. CC -> (1 + -uM) = (1 - M))
20	17, 19	eqtrd 1507	. . . . . . . . . 10 |- (M e. CC -> (-uM + 1) = (1 - M))
21	20	opreq2d 3976	. . . . . . . . 9 |- (M e. CC -> (F shift (-uM + 1)) = (F shift (1 - M)))
22	14, 21	eqtrd 1507	. . . . . . . 8 |- (M e. CC -> ((F shift -uM) shift 1) = (F shift (1 - M)))
23	8, 22	syl 10	. . . . . . 7 |- (M e. ZZ -> ((F shift -uM) shift 1) = (F shift (1 - M)))
24	23	opreq2d 3976	. . . . . 6 |- (M e. ZZ -> (S seq1 ((F shift -uM) shift 1)) = (S seq1 (F shift (1 - M))))
25	24	fveq1d 3726	. . . . 5 |- (M e. ZZ -> ((S seq1 ((F shift -uM) shift 1))` (N - (M - 1))) = ((S seq1 (F shift (1 - M)))` (N - (M - 1))))
26	25	3ad2ant1 800	. . . 4 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ((S seq1 ((F shift -uM) shift 1))` (N - (M - 1))) = ((S seq1 (F shift (1 - M)))` (N - (M - 1))))
27		subsubt 5462	. . . . . . . . . 10 |- ((N e. CC /\ M e. CC /\ 1 e. CC) -> (N - (M - 1)) = ((N - M) + 1))
28	10, 27	mp3an3 905	. . . . . . . . 9 |- ((N e. CC /\ M e. CC) -> (N - (M - 1)) = ((N - M) + 1))
29	28, 1, 8	syl2an 454	. . . . . . . 8 |- ((N e. ZZ /\ M e. ZZ) -> (N - (M - 1)) = ((N - M) + 1))
30	29	ancoms 436	. . . . . . 7 |- ((M e. ZZ /\ N e. ZZ) -> (N - (M - 1)) = ((N - M) + 1))
31	30	3adant3 799	. . . . . 6 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N - (M - 1)) = ((N - M) + 1))
32		znn0sub2t 6179	. . . . . . 7 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N - M) e. NN0)
33		nn0p1nnt 6175	. . . . . . 7 |- ((N - M) e. NN0 -> ((N - M) + 1) e. NN)
34	32, 33	syl 10	. . . . . 6 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ((N - M) + 1) e. NN)
35	31, 34	eqeltrd 1548	. . . . 5 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N - (M - 1)) e. NN)
36		seq0val.1	. . . . . 6 |- S e. V
37		oprex 3983	. . . . . 6 |- (F shift -uM) e. V
38	36, 37	seq1seq02t 6543	. . . . 5 |- ((N - (M - 1)) e. NN -> ((S seq1 ((F shift -uM) shift 1))` (N - (M - 1))) = (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))))
39	35, 38	syl 10	. . . 4 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ((S seq1 ((F shift -uM) shift 1))` (N - (M - 1))) = (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))))
40	26, 39	eqtr3d 1509	. . 3 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ((S seq1 (F shift (1 - M)))` (N - (M - 1))) = (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))))
41		subclt 5367	. . . . . . . . 9 |- ((N e. CC /\ (M - 1) e. CC) -> (N - (M - 1)) e. CC)
42		subclt 5367	. . . . . . . . . 10 |- ((M e. CC /\ 1 e. CC) -> (M - 1) e. CC)
43	10, 42	mpan2 696	. . . . . . . . 9 |- (M e. CC -> (M - 1) e. CC)
44	41, 43	sylan2 451	. . . . . . . 8 |- ((N e. CC /\ M e. CC) -> (N - (M - 1)) e. CC)
45		oprex 3983	. . . . . . . . . 10 |- (S seq0 (F shift -uM)) e. V
46	45	shftvalt 6346	. . . . . . . . 9 |- ((1 e. CC /\ (N - (M - 1)) e. CC) -> (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))) = ((S seq0 (F shift -uM))` ((N - (M - 1)) - 1)))
47	10, 46	mpan 695	. . . . . . . 8 |- ((N - (M - 1)) e. CC -> (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))) = ((S seq0 (F shift -uM))` ((N - (M - 1)) - 1)))
48	44, 47	syl 10	. . . . . . 7 |- ((N e. CC /\ M e. CC) -> (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))) = ((S seq0 (F shift -uM))` ((N - (M - 1)) - 1)))
49		nnncant 5466	. . . . . . . . 9 |- ((N e. CC /\ M e. CC /\ 1 e. CC) -> ((N - (M - 1)) - 1) = (N - M))
50	10, 49	mp3an3 905	. . . . . . . 8 |- ((N e. CC /\ M e. CC) -> ((N - (M - 1)) - 1) = (N - M))
51	50	fveq2d 3728	. . . . . . 7 |- ((N e. CC /\ M e. CC) -> ((S seq0 (F shift -uM))` ((N - (M - 1)) - 1)) = ((S seq0 (F shift -uM))` (N - M)))
52	48, 51	eqtrd 1507	. . . . . 6 |- ((N e. CC /\ M e. CC) -> (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))) = ((S seq0 (F shift -uM))` (N - M)))
53	52	ancoms 436	. . . . 5 |- ((M e. CC /\ N e. CC) -> (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))) = ((S seq0 (F shift -uM))` (N - M)))
54	53, 8, 1	syl2an 454	. . . 4 |- ((M e. ZZ /\ N e. ZZ) -> (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))) = ((S seq0 (F shift -uM))` (N - M)))
55	54	3adant3 799	. . 3 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (((S seq0 (F shift -uM)) shift 1)` (N - (M - 1))) = ((S seq0 (F shift -uM))` (N - M)))
56	7, 40, 55	3eqtrd 1511	. 2 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (((S seq1 (F shift (1 - M))) shift