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

Metamath Proof Explorer

Theorem fzosubel

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

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

Proof

Step Hyp Ref Expression
1 znegcl 
 |-  ( D e. ZZ -> -u D e. ZZ )
2 fzoaddel 
 |-  ( ( A e. ( B ..^ C ) /\ -u D e. ZZ ) -> ( A + -u D ) e. ( ( B + -u D ) ..^ ( C + -u D ) ) )
3 1 2 sylan2 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A + -u D ) e. ( ( B + -u D ) ..^ ( C + -u D ) ) )
4 elfzoelz 
 |-  ( A e. ( B ..^ C ) -> A e. ZZ )
5 4 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. ZZ )
6 5 zcnd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. CC )
7 simpr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> D e. ZZ )
8 7 zcnd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> D e. CC )
9 6 8 negsubd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A + -u D ) = ( A - D ) )
10 elfzoel1 
 |-  ( A e. ( B ..^ C ) -> B e. ZZ )
11 10 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B e. ZZ )
12 11 zcnd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B e. CC )
13 12 8 negsubd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( B + -u D ) = ( B - D ) )
14 elfzoel2 
 |-  ( A e. ( B ..^ C ) -> C e. ZZ )
15 14 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> C e. ZZ )
16 15 zcnd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> C e. CC )
17 16 8 negsubd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( C + -u D ) = ( C - D ) )
18 13 17 oveq12d 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( ( B + -u D ) ..^ ( C + -u D ) ) = ( ( B - D ) ..^ ( C - D ) ) )
19 3 9 18 3eltr3d 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A - D ) e. ( ( B - D ) ..^ ( C - D ) ) )