Metamath Proof Explorer


Theorem shftval4

Description: Value of a sequence shifted by -u A . (Contributed by NM, 18-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

Ref Expression
Hypothesis shftfval.1 FV
Assertion shftval4 ABFshiftAB=FA+B

Proof

Step Hyp Ref Expression
1 shftfval.1 FV
2 negcl AA
3 1 shftval ABFshiftAB=FBA
4 2 3 sylan ABFshiftAB=FBA
5 subneg BABA=B+A
6 5 ancoms ABBA=B+A
7 addcom ABA+B=B+A
8 6 7 eqtr4d ABBA=A+B
9 8 fveq2d ABFBA=FA+B
10 4 9 eqtrd ABFshiftAB=FA+B