# Metamath Proof Explorer

## Theorem shftval3

Description: Value of a sequence shifted by A - B . (Contributed by NM, 20-Jul-2005)

Ref Expression
Hypothesis shftfval.1 ${⊢}{F}\in \mathrm{V}$
Assertion shftval3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}\right)={F}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 0cn ${⊢}0\in ℂ$
3 1 shftval2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge 0\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}+0\right)={F}\left({B}+0\right)$
4 2 3 mp3an3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}+0\right)={F}\left({B}+0\right)$
5 addid1 ${⊢}{A}\in ℂ\to {A}+0={A}$
6 5 adantr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+0={A}$
7 6 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}+0\right)=\left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}\right)$
8 addid1 ${⊢}{B}\in ℂ\to {B}+0={B}$
9 8 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {B}+0={B}$
10 9 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {F}\left({B}+0\right)={F}\left({B}\right)$
11 4 7 10 3eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}\left({A}-{B}\right)\right)\left({A}\right)={F}\left({B}\right)$