Theorem shftval2

Description: Value of a sequence shifted by A - B . (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 5-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	⊢ 𝐹 ∈ V
Assertion	shftval2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ ( 𝐴 + 𝐶 ) ) = ( 𝐹 ‘ ( 𝐵 + 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	⊢ 𝐹 ∈ V
2		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
3	2	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
4		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + 𝐶 ) ∈ ℂ )
5	1	shftval	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐴 + 𝐶 ) ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ ( 𝐴 + 𝐶 ) ) = ( 𝐹 ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 − 𝐵 ) ) ) )
6	3 4 5	3imp3i2an	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ ( 𝐴 + 𝐶 ) ) = ( 𝐹 ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 − 𝐵 ) ) ) )
7		pnncan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐶 ) − ( 𝐴 − 𝐵 ) ) = ( 𝐶 + 𝐵 ) )
8	7	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐶 ) − ( 𝐴 − 𝐵 ) ) = ( 𝐶 + 𝐵 ) )
9		addcom	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + 𝐶 ) = ( 𝐶 + 𝐵 ) )
10	9	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + 𝐶 ) = ( 𝐶 + 𝐵 ) )
11	8 10	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐶 ) − ( 𝐴 − 𝐵 ) ) = ( 𝐵 + 𝐶 ) )
12	11	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐹 ‘ ( ( 𝐴 + 𝐶 ) − ( 𝐴 − 𝐵 ) ) ) = ( 𝐹 ‘ ( 𝐵 + 𝐶 ) ) )
13	6 12	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ ( 𝐴 + 𝐶 ) ) = ( 𝐹 ‘ ( 𝐵 + 𝐶 ) ) )