Metamath Proof Explorer

Theorem fzoaddel2

Description: Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzoaddel2 
|- ( ( A e. ( 0 ..^ ( B - C ) ) /\ B e. ZZ /\ C e. ZZ ) -> ( A + C ) e. ( C ..^ B ) )

Proof

Step Hyp Ref Expression
1 fzoaddel 
 |-  ( ( A e. ( 0 ..^ ( B - C ) ) /\ C e. ZZ ) -> ( A + C ) e. ( ( 0 + C ) ..^ ( ( B - C ) + C ) ) )
2 1 3adant2 
 |-  ( ( A e. ( 0 ..^ ( B - C ) ) /\ B e. ZZ /\ C e. ZZ ) -> ( A + C ) e. ( ( 0 + C ) ..^ ( ( B - C ) + C ) ) )
3 zcn 
 |-  ( B e. ZZ -> B e. CC )
4 zcn 
 |-  ( C e. ZZ -> C e. CC )
5 addid2 
 |-  ( C e. CC -> ( 0 + C ) = C )
6 5 adantl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( 0 + C ) = C )
7 npcan 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B - C ) + C ) = B )
8 6 7 oveq12d 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( 0 + C ) ..^ ( ( B - C ) + C ) ) = ( C ..^ B ) )
9 3 4 8 syl2an 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( ( 0 + C ) ..^ ( ( B - C ) + C ) ) = ( C ..^ B ) )
10 9 3adant1 
 |-  ( ( A e. ( 0 ..^ ( B - C ) ) /\ B e. ZZ /\ C e. ZZ ) -> ( ( 0 + C ) ..^ ( ( B - C ) + C ) ) = ( C ..^ B ) )
11 2 10 eleqtrd 
 |-  ( ( A e. ( 0 ..^ ( B - C ) ) /\ B e. ZZ /\ C e. ZZ ) -> ( A + C ) e. ( C ..^ B ) )