Theorem seq0p1 6552

Description: Value of the 0-based recursive sequence builder at a successor.

Hypotheses

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

Assertion

Ref	Expression
seq0p1	|- (N e. NN0 -> ((S seq0 F)` (N + 1)) = (((S seq0 F)` N)S(F` (N + 1))))

Proof of Theorem seq0p1

Step	Hyp	Ref	Expression
1		peano2nn0 6126	. . . 4 |- (N e. NN0 -> (N + 1) e. NN0)
2		fvres 3740	. . . 4 |- ((N + 1) e. NN0 -> ((((S seq1 (F shift 1)) shift -u1) |` NN0)` (N + 1)) = (((S seq1 (F shift 1)) shift -u1)` (N + 1)))
3	1, 2	syl 10	. . 3 |- (N e. NN0 -> ((((S seq1 (F shift 1)) shift -u1) |` NN0)` (N + 1)) = (((S seq1 (F shift 1)) shift -u1)` (N + 1)))
4		nn0cnt 6111	. . . . 5 |- (N e. NN0 -> N e. CC)
5		peano2cn 5356	. . . . 5 |- (N e. CC -> (N + 1) e. CC)
6		ax1cn 5281	. . . . . . 7 |- 1 e. CC
7	6	negcl 5381	. . . . . 6 |- -u1 e. CC
8		oprex 3989	. . . . . . 7 |- (S seq1 (F shift 1)) e. V
9	8	shftvalt 6347	. . . . . 6 |- ((-u1 e. CC /\ (N + 1) e. CC) -> (((S seq1 (F shift 1)) shift -u1)` (N + 1)) = ((S seq1 (F shift 1))` ((N + 1) - -u1)))
10	7, 9	mpan 697	. . . . 5 |- ((N + 1) e. CC -> (((S seq1 (F shift 1)) shift -u1)` (N + 1)) = ((S seq1 (F shift 1))` ((N + 1) - -u1)))
11	4, 5, 10	3syl 20	. . . 4 |- (N e. NN0 -> (((S seq1 (F shift 1)) shift -u1)` (N + 1)) = ((S seq1 (F shift 1))` ((N + 1) - -u1)))
12		addsubt 5396	. . . . . . 7 |- ((N e. CC /\ 1 e. CC /\ -u1 e. CC) -> ((N + 1) - -u1) = ((N - -u1) + 1))
13	6, 7, 12	mp3an23 910	. . . . . 6 |- (N e. CC -> ((N + 1) - -u1) = ((N - -u1) + 1))
14	4, 13	syl 10	. . . . 5 |- (N e. NN0 -> ((N + 1) - -u1) = ((N - -u1) + 1))
15	14	fveq2d 3734	. . . 4 |- (N e. NN0 -> ((S seq1 (F shift 1))` ((N + 1) - -u1)) = ((S seq1 (F shift 1))` ((N - -u1) + 1)))
16		subnegt 5406	. . . . . . . . 9 |- ((N e. CC /\ 1 e. CC) -> (N - -u1) = (N + 1))
17	6, 16	mpan2 698	. . . . . . . 8 |- (N e. CC -> (N - -u1) = (N + 1))
18	4, 17	syl 10	. . . . . . 7 |- (N e. NN0 -> (N - -u1) = (N + 1))
19		nn0p1nnt 6177	. . . . . . 7 |- (N e. NN0 -> (N + 1) e. NN)
20	18, 19	eqeltrd 1551	. . . . . 6 |- (N e. NN0 -> (N - -u1) e. NN)
21		seq0val.1	. . . . . . 7 |- S e. V
22		oprex 3989	. . . . . . 7 |- (F shift 1) e. V
23	21, 22	seq1p1 6319	. . . . . 6 |- ((N - -u1) e. NN -> ((S seq1 (F shift 1))` ((N - -u1) + 1)) = (((S seq1 (F shift 1))` (N - -u1))S((F shift 1)` ((N - -u1) + 1))))
24	20, 23	syl 10	. . . . 5 |- (N e. NN0 -> ((S seq1 (F shift 1))` ((N - -u1) + 1)) = (((S seq1 (F shift 1))` (N - -u1))S((F shift 1)` ((N - -u1) + 1))))
25		subclt 5379	. . . . . . . . . 10 |- ((N e. CC /\ -u1 e. CC) -> (N - -u1) e. CC)
26	7, 25	mpan2 698	. . . . . . . . 9 |- (N e. CC -> (N - -u1) e. CC)
27	4, 26	syl 10	. . . . . . . 8 |- (N e. NN0 -> (N - -u1) e. CC)
28		peano2cn 5356	. . . . . . . 8 |- ((N - -u1) e. CC -> ((N - -u1) + 1) e. CC)
29		seq0val.2	. . . . . . . . . 10 |- F e. V
30	29	shftvalt 6347	. . . . . . . . 9 |- ((1 e. CC /\ ((N - -u1) + 1) e. CC) -> ((F shift 1)` ((N - -u1) + 1)) = (F` (((N - -u1) + 1) - 1)))
31	6, 30	mpan 697	. . . . . . . 8 |- (((N - -u1) + 1) e. CC -> ((F shift 1)` ((N - -u1) + 1)) = (F` (((N - -u1) + 1) - 1)))
32	27, 28, 31	3syl 20	. . . . . . 7 |- (N e. NN0 -> ((F shift 1)` ((N - -u1) + 1)) = (F` (((N - -u1) + 1) - 1)))
33		pncant 5409	. . . . . . . . . . . 12 |- (((N - -u1) e. CC /\ 1 e. CC) -> (((N - -u1) + 1) - 1) = (N - -u1))
34	6, 33	mpan2 698	. . . . . . . . . . 11 |- ((N - -u1) e. CC -> (((N - -u1) + 1) - 1) = (N - -u1))
35	26, 34	syl 10	. . . . . . . . . 10 |- (N e. CC -> (((N - -u1) + 1) - 1) = (N - -u1))
36	35, 17	eqtrd 1510	. . . . . . . . 9 |- (N e. CC -> (((N - -u1) + 1) - 1) = (N + 1))
37	4, 36	syl 10	. . . . . . . 8 |- (N e. NN0 -> (((N - -u1) + 1) - 1) = (N + 1))
38	37	fveq2d 3734	. . . . . . 7 |- (N e. NN0 -> (F` (((N - -u1) + 1) - 1)) = (F` (N + 1)))
39	32, 38	eqtrd 1510	. . . . . 6 |- (N e. NN0 -> ((F shift 1)` ((N - -u1) + 1)) = (F` (N + 1)))
40	39	opreq2d 3982	. . . . 5 |- (N e. NN0 -> (((S seq1 (F shift 1))` (N - -u1))S((F shift 1)` ((N - -u1) + 1))) = (((S seq1 (F shift 1))` (N - -u1))S(F` (N + 1))))
41	24, 40	eqtrd 1510	. . . 4 |- (N e. NN0 -> ((S seq1 (F shift 1))` ((N - -u1) + 1)) = (((S seq1 (F shift 1))` (N - -u1))S(F` (N + 1))))
42	11, 15, 41	3eqtrd 1514	. . 3 |- (N e. NN0 -> (((S seq1 (F shift 1)) shift -u1)` (N + 1)) = (((S seq1 (F shift 1))` (N - -u1))S(F` (N + 1))))
43		fvres 3740	. . . . . 6 |- (N e. NN0 -> ((((S seq1 (F shift 1)) shift -u1) |` NN0)` N) = (((S seq1 (F shift 1)) shift -u1)` N))
44	8	shftvalt 6347	. . . . . . . 8 |- ((-u1 e. CC /\ N e. CC) -> (((S seq1 (F shift 1)) shift -u1)` N) = ((S seq1 (F shift 1))` (N - -u1)))
45	7, 44	mpan 697	. . . . . . 7 |- (N e. CC -> (((S seq1 (F shift 1)) shift -u1)` N) = ((S seq1 (F shift 1))` (N - -u1)))
46	4, 45	syl 10	. . . . . 6 |- (N e. NN0 -> (((S seq1 (F shift 1)) shift -u1)` N) = ((S seq1 (F shift 1))` (N - -u1)))
47	43, 46	eqtrd 1510	. . . . 5 |- (N e. NN0 -> ((((S seq1 (F shift 1)) shift -u1) |` NN0)` N) = ((S seq1 (F shift 1))` (N - -u1)))
48	21, 29	seq0fval 6536	. . . . . 6 |- (S seq0 F) = (((S seq1 (F shift 1)) shift -u1) |` NN0)
49	48	fveq1i 3731	. . . . 5 |- ((S seq0 F)` N) = ((((S seq1 (F shift 1)) shift -u1) |` NN0)` N)
50	47, 49	syl5req 1523	. . . 4 |- (N e. NN0 -> ((S seq1 (F shift 1))` (N - -u1)) = ((S seq0 F)` N))
51	50	opreq1d 3981	. . 3 |- (N e. NN0 -> (((S seq1 (F shift 1))` (N - -u1))S(F` (N + 1))) = (((S seq0 F)` N)S(F` (N + 1))))
52	3, 42, 51	3eqtrd 1514	. 2 |- (N e. NN0 -> ((((S seq1 (F shift 1)) shift -u1) |` NN0)` (N + 1)) = (((S seq0 F)` N)S(F` (N + 1))))
53	48	fveq1i 3731	. 2 |- ((S seq0 F)` (N + 1)) = ((((S seq1 (F shift 1)) shift -u1) |` NN0)` (N + 1))
54	52, 53	syl5eq 1522	1 |- (N e. NN0 -> ((S seq0 F)` (N + 1)) = (((S seq0 F)` N)S(F` (N + 1))))

Syntax hints:   -> wi 3   = wceq 958   e. wcel 960  Vcvv 1814   |` cres 3178  ` cfv 3188  (class class class)co 3969  CCcc 5244  1c1 5247   + caddc 5249   - cmin 5304  -ucneg 5305  NNcn 5308  NN0cn0 5309   seq1 cseq1 6308   shift cshi 6341   seq0 cseq0 6533

This theorem is referenced by:  seq01 6553  ser0cl1 6565  ser0p1 6568

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12