Metamath Proof Explorer

Theorem fzosubel2

Description: Membership in a translated half-open integer range implies translated membership in the original range. (Contributed by Stefan O'Rear, 15-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 fzosubel 
 |-  ( ( A e. ( ( B + C ) ..^ ( B + D ) ) /\ B e. ZZ ) -> ( A - B ) e. ( ( ( B + C ) - B ) ..^ ( ( B + D ) - B ) ) )
2 1 3ad2antr1 
 |-  ( ( A e. ( ( B + C ) ..^ ( B + D ) ) /\ ( B e. ZZ /\ C e. ZZ /\ D e. ZZ ) ) -> ( A - B ) e. ( ( ( B + C ) - B ) ..^ ( ( B + D ) - B ) ) )
3 zcn 
 |-  ( B e. ZZ -> B e. CC )
4 zcn 
 |-  ( C e. ZZ -> C e. CC )
5 zcn 
 |-  ( D e. ZZ -> D e. CC )
6 pncan2 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B + C ) - B ) = C )
7 6 3adant3 
 |-  ( ( B e. CC /\ C e. CC /\ D e. CC ) -> ( ( B + C ) - B ) = C )
8 pncan2 
 |-  ( ( B e. CC /\ D e. CC ) -> ( ( B + D ) - B ) = D )
9 8 3adant2 
 |-  ( ( B e. CC /\ C e. CC /\ D e. CC ) -> ( ( B + D ) - B ) = D )
10 7 9 oveq12d 
 |-  ( ( B e. CC /\ C e. CC /\ D e. CC ) -> ( ( ( B + C ) - B ) ..^ ( ( B + D ) - B ) ) = ( C ..^ D ) )
11 3 4 5 10 syl3an 
 |-  ( ( B e. ZZ /\ C e. ZZ /\ D e. ZZ ) -> ( ( ( B + C ) - B ) ..^ ( ( B + D ) - B ) ) = ( C ..^ D ) )
12 11 adantl 
 |-  ( ( A e. ( ( B + C ) ..^ ( B + D ) ) /\ ( B e. ZZ /\ C e. ZZ /\ D e. ZZ ) ) -> ( ( ( B + C ) - B ) ..^ ( ( B + D ) - B ) ) = ( C ..^ D ) )
13 2 12 eleqtrd 
 |-  ( ( A e. ( ( B + C ) ..^ ( B + D ) ) /\ ( B e. ZZ /\ C e. ZZ /\ D e. ZZ ) ) -> ( A - B ) e. ( C ..^ D ) )