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)$$