Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
3 2 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ∈ ℂ
4 addcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A + C ∈ ℂ
5 1 shftval ⊢ A − B ∈ ℂ ∧ A + C ∈ ℂ → F shift A − B ⁡ A + C = F ⁡ A + C - A − B
6 3 4 5 3imp3i2an ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → F shift A − B ⁡ A + C = F ⁡ A + C - A − B
7 pnncan ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + C - A − B = C + B
8 7 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - A − B = C + B
9 addcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
10 9 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
11 8 10 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - A − B = B + C
12 11 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → F ⁡ A + C - A − B = F ⁡ B + C
13 6 12 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → F shift A − B ⁡ A + C = F ⁡ B + C