This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shftval3

Description: Value of a sequence shifted by A - B . (Contributed by NM, 20-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ 𝐹 ∈ V
2 0cn ⊢ 0 ∈ ℂ
3 1 shftval2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ ( 𝐴 + 0 ) ) = ( 𝐹 ‘ ( 𝐵 + 0 ) ) )
4 2 3 mp3an3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ ( 𝐴 + 0 ) ) = ( 𝐹 ‘ ( 𝐵 + 0 ) ) )
5 addrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 0 ) = 𝐴 )
7 6 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ ( 𝐴 + 0 ) ) = ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ 𝐴 ) )
8 addrid ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 + 0 ) = 𝐵 )
9 8 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 + 0 ) = 𝐵 )
10 9 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ ( 𝐵 + 0 ) ) = ( 𝐹 ‘ 𝐵 ) )
11 4 7 10 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift ( 𝐴 − 𝐵 ) ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )