# Metamath Proof Explorer

## Theorem shftval4

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

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

### Proof

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