# Metamath Proof Explorer

## Theorem shftval5

Description: Value of a shifted sequence. (Contributed by NM, 19-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

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

### Proof

Step Hyp Ref Expression
1 shftfval.1 ${⊢}{F}\in \mathrm{V}$
2 simpr ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\right)\to {A}\in ℂ$
3 addcl ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\right)\to {B}+{A}\in ℂ$
4 1 shftval ${⊢}\left({A}\in ℂ\wedge {B}+{A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left({B}+{A}\right)={F}\left({B}+{A}-{A}\right)$
5 2 3 4 syl2anc ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left({B}+{A}\right)={F}\left({B}+{A}-{A}\right)$
6 pncan ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\right)\to {B}+{A}-{A}={B}$
7 6 fveq2d ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\right)\to {F}\left({B}+{A}-{A}\right)={F}\left({B}\right)$
8 5 7 eqtrd ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left({B}+{A}\right)={F}\left({B}\right)$
9 8 ancoms ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({F}\mathrm{shift}{A}\right)\left({B}+{A}\right)={F}\left({B}\right)$