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∈ℂ→FshiftA−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∈ℂ→FshiftA−B⁡A+C=F⁡A+C-A−B
6 3 4 5 3imp3i2an ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→FshiftA−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∈ℂ→FshiftA−B⁡A+C=F⁡B+C