Metamath Proof Explorer

Theorem fzoaddel

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

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

Proof

Step Hyp Ref Expression
1 elfzoel1 
 |-  ( A e. ( B ..^ C ) -> B e. ZZ )
2 1 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B e. ZZ )
3 2 zred 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B e. RR )
4 elfzoelz 
 |-  ( A e. ( B ..^ C ) -> A e. ZZ )
5 4 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. ZZ )
6 5 zred 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. RR )
7 simpr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> D e. ZZ )
8 7 zred 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> D e. RR )
9 elfzole1 
 |-  ( A e. ( B ..^ C ) -> B <_ A )
10 9 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B <_ A )
11 3 6 8 10 leadd1dd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( B + D ) <_ ( A + D ) )
12 elfzoel2 
 |-  ( A e. ( B ..^ C ) -> C e. ZZ )
13 12 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> C e. ZZ )
14 13 zred 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> C e. RR )
15 elfzolt2 
 |-  ( A e. ( B ..^ C ) -> A < C )
16 15 adantr 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A < C )
17 6 14 8 16 ltadd1dd 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A + D ) < ( C + D ) )
18 zaddcl 
 |-  ( ( A e. ZZ /\ D e. ZZ ) -> ( A + D ) e. ZZ )
19 4 18 sylan 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A + D ) e. ZZ )
20 zaddcl 
 |-  ( ( B e. ZZ /\ D e. ZZ ) -> ( B + D ) e. ZZ )
21 1 20 sylan 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( B + D ) e. ZZ )
22 zaddcl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( C + D ) e. ZZ )
23 12 22 sylan 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( C + D ) e. ZZ )
24 elfzo 
 |-  ( ( ( A + D ) e. ZZ /\ ( B + D ) e. ZZ /\ ( C + D ) e. ZZ ) -> ( ( A + D ) e. ( ( B + D ) ..^ ( C + D ) ) <-> ( ( B + D ) <_ ( A + D ) /\ ( A + D ) < ( C + D ) ) ) )
25 19 21 23 24 syl3anc 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( ( A + D ) e. ( ( B + D ) ..^ ( C + D ) ) <-> ( ( B + D ) <_ ( A + D ) /\ ( A + D ) < ( C + D ) ) ) )
26 11 17 25 mpbir2and 
 |-  ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A + D ) e. ( ( B + D ) ..^ ( C + D ) ) )