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