This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzosubel3

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

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> A e. ( B ..^ ( B + D ) ) )
2 elfzoel1 
 |-  ( A e. ( B ..^ ( B + D ) ) -> B e. ZZ )
3 2 adantr 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> B e. ZZ )
4 3 zcnd 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> B e. CC )
5 4 addridd 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> ( B + 0 ) = B )
6 5 oveq1d 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> ( ( B + 0 ) ..^ ( B + D ) ) = ( B ..^ ( B + D ) ) )
7 1 6 eleqtrrd 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> A e. ( ( B + 0 ) ..^ ( B + D ) ) )
8 0zd 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> 0 e. ZZ )
9 simpr 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> D e. ZZ )
10 fzosubel2 
 |-  ( ( A e. ( ( B + 0 ) ..^ ( B + D ) ) /\ ( B e. ZZ /\ 0 e. ZZ /\ D e. ZZ ) ) -> ( A - B ) e. ( 0 ..^ D ) )
11 7 3 8 9 10 syl13anc 
 |-  ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> ( A - B ) e. ( 0 ..^ D ) )