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 ⊢ F ∈ V
Assertion shftval3 ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A − B ⁡ A = F ⁡ B

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 0cn ⊢ 0 ∈ ℂ
3 1 shftval2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ 0 ∈ ℂ → F shift A − B ⁡ A + 0 = F ⁡ B + 0
4 2 3 mp3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A − B ⁡ A + 0 = F ⁡ B + 0
5 addid1 ⊢ A ∈ ℂ → A + 0 = A
6 5 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + 0 = A
7 6 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A − B ⁡ A + 0 = F shift A − B ⁡ A
8 addid1 ⊢ B ∈ ℂ → B + 0 = B
9 8 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → B + 0 = B
10 9 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → F ⁡ B + 0 = F ⁡ B
11 4 7 10 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A − B ⁡ A = F ⁡ B