Metamath Proof Explorer

Theorem shftval3

Description: Value of a sequence shifted by A - B . (Contributed by NM, 20-Jul-2005)

Ref Expression
Hypothesis shftfval.1 
|- F e. _V
Assertion shftval3 
|- ( ( A e. CC /\ B e. CC ) -> ( ( F shift ( A - B ) ) ` A ) = ( F ` B ) )

Proof

Step Hyp Ref Expression
1 shftfval.1 
 |-  F e. _V
2 0cn 
 |-  0 e. CC
3 1 shftval2 
 |-  ( ( A e. CC /\ B e. CC /\ 0 e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + 0 ) ) = ( F ` ( B + 0 ) ) )
4 2 3 mp3an3 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + 0 ) ) = ( F ` ( B + 0 ) ) )
5 addid1 
 |-  ( A e. CC -> ( A + 0 ) = A )
6 5 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + 0 ) = A )
7 6 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + 0 ) ) = ( ( F shift ( A - B ) ) ` A ) )
8 addid1 
 |-  ( B e. CC -> ( B + 0 ) = B )
9 8 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B + 0 ) = B )
10 9 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( F ` ( B + 0 ) ) = ( F ` B ) )
11 4 7 10 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( F shift ( A - B ) ) ` A ) = ( F ` B ) )