Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Properties of real and complex numbers
shftvalg
Next ⟩
divcnvlin
Metamath Proof Explorer
Ascii
Unicode
Theorem
shftvalg
Description:
Value of a sequence shifted by
A
.
(Contributed by
Scott Fenton
, 16-Dec-2017)
Ref
Expression
Assertion
shftvalg
⊢
F
∈
V
∧
A
∈
ℂ
∧
B
∈
ℂ
→
F
shift
A
⁡
B
=
F
⁡
B
−
A
Proof
Step
Hyp
Ref
Expression
1
oveq1
⊢
f
=
F
→
f
shift
A
=
F
shift
A
2
1
fveq1d
⊢
f
=
F
→
f
shift
A
⁡
B
=
F
shift
A
⁡
B
3
fveq1
⊢
f
=
F
→
f
⁡
B
−
A
=
F
⁡
B
−
A
4
2
3
eqeq12d
⊢
f
=
F
→
f
shift
A
⁡
B
=
f
⁡
B
−
A
↔
F
shift
A
⁡
B
=
F
⁡
B
−
A
5
4
imbi2d
⊢
f
=
F
→
A
∈
ℂ
∧
B
∈
ℂ
→
f
shift
A
⁡
B
=
f
⁡
B
−
A
↔
A
∈
ℂ
∧
B
∈
ℂ
→
F
shift
A
⁡
B
=
F
⁡
B
−
A
6
vex
⊢
f
∈
V
7
6
shftval
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
f
shift
A
⁡
B
=
f
⁡
B
−
A
8
5
7
vtoclg
⊢
F
∈
V
→
A
∈
ℂ
∧
B
∈
ℂ
→
F
shift
A
⁡
B
=
F
⁡
B
−
A
9
8
3impib
⊢
F
∈
V
∧
A
∈
ℂ
∧
B
∈
ℂ
→
F
shift
A
⁡
B
=
F
⁡
B
−
A