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

Metamath Proof Explorer

Theorem shftval

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

Ref Expression
Hypothesis shftfval.1 ⊢ F ∈ V
Assertion shftval ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A ⁡ B = F ⁡ B − A

Proof

Step Hyp Ref Expression
1 shftfval.1 ⊢ F ∈ V
2 1 shftfib ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A B = F B − A
3 2 eleq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → x ∈ F shift A B ↔ x ∈ F B − A
4 3 iotabidv ⊢ A ∈ ℂ ∧ B ∈ ℂ → ι x | x ∈ F shift A B = ι x | x ∈ F B − A
5 dffv3 ⊢ F shift A ⁡ B = ι x | x ∈ F shift A B
6 dffv3 ⊢ F ⁡ B − A = ι x | x ∈ F B − A
7 4 5 6 3eqtr4g ⊢ A ∈ ℂ ∧ B ∈ ℂ → F shift A ⁡ B = F ⁡ B − A