HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem seqzp1 6548
Description: Value of the arbitrary-based recursive sequence builder at a successor value.
Hypotheses
Ref Expression
seq0val.1 |- S e. V
seq0val.2 |- F e. V
Assertion
Ref Expression
seqzp1 |- (N e. (ZZ>` M) -> ((<.M, S>. seq F)` (N + 1)) = (((<.M, S>. seq F)` N)S(F` (N + 1))))
Proof of Theorem seqzp1
StepHypRef Expression
1 eluzel2 6424 . . 3 |- (N e. (ZZ>` M) -> M e. ZZ)
2 seq0val.1 . . . . 5 |- S e. V
3 seq0val.2 . . . . 5 |- F e. V
42, 3seqzfval 6537 . . . 4 |- (M e. ZZ -> (<.M, S>. seq F) = (((S seq1 (F shift (1 - M))) shift (M - 1)) |` {k e. ZZ | M <_ k}))
54fveq1d 3726 . . 3 |- (M e. ZZ -> ((<.M, S>. seq F)` (N + 1)) = ((((S seq1 (F shift (1 - M))) shift (M - 1)) |` {k e. ZZ | M <_ k})` (N + 1)))
61, 5syl 10 . 2 |- (N e. (ZZ>` M) -> ((<.M, S>. seq F)` (N + 1)) = ((((S seq1 (F shift (1 - M))) shift (M - 1)) |` {k e. ZZ | M <_ k})` (N + 1)))
7 peano2uz 6447 . . . 4 |- (N e. (ZZ>` M) -> (N + 1) e. (ZZ>` M))
8 eluzel2 6424 . . . . . . 7 |- ((N + 1) e. (ZZ>` M) -> M e. ZZ)
9 uzvalt 6419 . . . . . . 7 |- (M e. ZZ -> (ZZ>` M) = {k e. ZZ | M <_ k})
108, 9syl 10 . . . . . 6 |- ((N + 1) e. (ZZ>` M) -> (ZZ>` M) = {k e. ZZ | M <_ k})
1110eleq2d 1541 . . . . 5 |- ((N + 1) e. (ZZ>` M) -> ((N + 1) e. (ZZ>` M) <-> (N + 1) e. {k e. ZZ | M <_ k}))
1211ibi 592 . . . 4 |- ((N + 1) e. (ZZ>` M) -> (N + 1) e. {k e. ZZ | M <_ k})
13 fvres 3734 . . . 4 |- ((N + 1) e. {k e. ZZ | M <_ k} -> ((((S seq1 (F shift (1 - M))) shift (M - 1)) |` {k e. ZZ | M <_ k})` (N + 1)) = (((S seq1 (F shift (1 - M))) shift (M - 1))` (N + 1)))
147, 12, 133syl 20 . . 3 |- (N e. (ZZ>` M) -> ((((S seq1 (F shift (1 - M))) shift (M - 1)) |` {k e. ZZ | M <_ k})` (N + 1)) = (((S seq1 (F shift (1 - M))) shift (M - 1))` (N + 1)))
15 oprex 3983 . . . . . . . 8 |- (S seq1 (F shift (1 - M))) e. V
1615shftvalt 6346 . . . . . . 7 |- (((M - 1) e. CC /\ (N + 1) e. CC) -> (((S seq1 (F shift (1 - M))) shift (M - 1))` (N + 1)) = ((S seq1 (F shift (1 - M)))` ((N + 1) - (M - 1))))
17 ax1cn 5269 . . . . . . . 8 |- 1 e. CC
18 subclt 5367 . . . . . . . 8 |- ((M e. CC /\ 1 e. CC) -> (M - 1) e. CC)
1917, 18mpan2 696 . . . . . . 7 |- (M e. CC -> (M - 1) e. CC)
20 peano2cn 5344 . . . . . . 7 |- (N e. CC -> (N + 1) e. CC)
2116, 19, 20syl2an 454 . . . . . 6 |- ((M e. CC /\ N e. CC) -> (((S seq1 (F shift (1 - M))) shift (M - 1))` (N + 1)) = ((S seq1 (F shift (1 - M)))` ((N + 1) - (M - 1))))
2219anim2i 335 . . . . . . . . 9 |- ((N e. CC /\ M e. CC) -> (N e. CC /\ (M - 1) e. CC))
2322ancoms 436 . . . . . . . 8 |- ((M e. CC /\ N e. CC) -> (N e. CC /\ (M - 1) e. CC))
24 addsubt 5384 . . . . . . . . 9 |- ((N e. CC /\ 1 e. CC /\ (M - 1) e. CC) -> ((N + 1) - (M - 1)) = ((N - (M - 1)) + 1))
2517, 24mp3an2 904 . . . . . . . 8 |- ((N e. CC /\ (M - 1) e. CC) -> ((N + 1) - (M - 1)) = ((N - (M - 1)) + 1))
2623, 25syl 10 . . . . . . 7 |- ((M e. CC /\ N e. CC) -> ((N + 1) - (M - 1)) = ((N - (M - 1)) + 1))
2726fveq2d 3728 . . . . . 6 |- ((M e. CC /\ N e. CC) -> ((S seq1 (F shift (1 - M)))` ((N + 1) - (M - 1))) = ((S seq1 (F shift (1 - M)))` ((N - (M - 1)) + 1)))
2821, 27eqtrd 1507 . . . . 5 |- ((M e. CC /\ N e. CC) -> (((S seq1 (F shift (1 - M))) shift (M - 1))` (N + 1)) = ((S seq1 (F shift (1 - M)))` ((N - (M - 1)) + 1)))
29 zcnt 6140 . . . . . 6 |- (M e. ZZ -> M e. CC)
301, 29syl 10 . . . . 5 |- (N e. (ZZ>` M) -> M e. CC)
31 eluzelz 6423 . . . . . 6 |- (N e. (ZZ>` M) -> N e. ZZ)
32 zcnt 6140 . . . . . 6 |- (N e. ZZ -> N e. CC)
3331, 32syl 10 . . . . 5 |- (N e. (ZZ>` M) -> N e. CC)
3428, 30, 33sylanc 471 . . . 4 |- (N e. (ZZ>` M) -> (((S seq1 (F shift (1 - M))) shift (M - 1))` (N + 1)) = ((S seq1 (F shift (1 - M)))` ((N - (M - 1)) + 1)))
35 eluz2t 6421 . . . . . 6 |- (N e. (ZZ>` M) <-> (M e. ZZ /\ N e. ZZ /\ M <_ N))
36 subsubt 5462 . . . . . . . . . . 11 |- ((N e. CC /\ M e. CC /\ 1 e. CC) -> (N - (M - 1)) = ((N - M) + 1))
3717, 36mp3an3 905 . . . . . . . . . 10 |- ((N e. CC /\ M e. CC) -> (N - (M - 1)) = ((N - M) + 1))
3837, 32, 29syl2an 454 . . . . . . . . 9 |- ((N e. ZZ /\ M e. ZZ) -> (N - (M - 1)) = ((N - M) + 1))
3938ancoms 436 . . . . . . . 8 |- ((M e. ZZ /\ N e. ZZ) -> (N - (M - 1)) = ((N - M) + 1))
40393adant3 799 . . . . . . 7 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N - (M - 1)) = ((N - M) + 1))
41 znn0sub2t 6179 . . . . . . . 8 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N - M) e. NN0)
42 nn0p1nnt 6175 . . . . . . . 8 |- ((N - M) e. NN0 -> ((N - M) + 1) e. NN)
4341, 42syl 10 . . . . . . 7 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ((N - M) + 1) e. NN)
4440, 43eqeltrd 1548 . . . . . 6 |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N - (M - 1)) e. NN)
4535, 44sylbi 199 . . . . 5 |- (N e. (ZZ>` M) -> (N - (M - 1)) e. NN)
46 oprex 3983 . . . . . 6 |- (F shift (1 - M)) e. V
472, 46seq1p1 6318 . . . . 5 |- ((N - (M - 1)) e. NN -> ((S seq1 (F shift (1 - M)))` ((N - (M - 1)) + 1)) = (((S seq1 (F shift (1 - M)))` (N - (M - 1)))S((F shift (1 - M))` ((N - (M - 1)) + 1))))
4845, 47syl 10 . . . 4 |- (N e. (ZZ>` M) -> ((S seq1 (F shift (1 - M)))` ((N - (M - 1)) + 1)) = (((S seq1 (F shift (1 - M)))` (N - (M - 1)))S((F shift (1 - M))` ((N - (M - 1)) + 1))))
493shftvalt 6346 . . . . . . . 8 |- (((1 - M) e. CC /\ ((N - (M - 1)) + 1) e. CC) -> ((F shift (1 - M))` ((N - (M - 1)) + 1)) = (F` (((N - (M - 1)) + 1) - (1 - M))))
50 subclt 5367 . . . . . . . . . 10 |- ((1 e. CC /\ M e. CC) -> (1 - M) e. CC)
5117, 50mpan 695 . . . . . . . . 9 |- (M e. CC -> (1 - M) e. CC)
5251adantr 389 . . . . . . . 8 |- ((M e. CC /\ N e. CC) -> (1 - M) e. CC)
53 subclt 5367 . . . . . . . . . . 11 |- ((N e. CC /\ (M - 1) e. CC) -> (N - (M - 1)) e. CC)
5453, 19sylan2 451 . . . . . . . . . 10 |- ((N e. CC /\ M e. CC) -> (N - (M - 1)) e. CC)
5554ancoms 436 . . . . . . . . 9 |- ((M e. CC /\ N e. CC) -> (N - (M - 1)) e. CC)
56 peano2cn 5344 . . . . . . . . 9 |- ((N - (M - 1)) e. CC -> (