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