Metamath Proof Explorer

Theorem fzneg

Description: Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion fzneg 
|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A e. ( B ... C ) <-> -u A e. ( -u C ... -u B ) ) )

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( B <_ A /\ A <_ C ) <-> ( A <_ C /\ B <_ A ) )
2 zre 
 |-  ( A e. ZZ -> A e. RR )
3 2 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. RR )
4 zre 
 |-  ( C e. ZZ -> C e. RR )
5 4 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. RR )
6 3 5 lenegd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A <_ C <-> -u C <_ -u A ) )
7 zre 
 |-  ( B e. ZZ -> B e. RR )
8 7 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. RR )
9 8 3 lenegd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B <_ A <-> -u A <_ -u B ) )
10 6 9 anbi12d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A <_ C /\ B <_ A ) <-> ( -u C <_ -u A /\ -u A <_ -u B ) ) )
11 1 10 bitrid 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( B <_ A /\ A <_ C ) <-> ( -u C <_ -u A /\ -u A <_ -u B ) ) )
12 elfz 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A e. ( B ... C ) <-> ( B <_ A /\ A <_ C ) ) )
13 znegcl 
 |-  ( A e. ZZ -> -u A e. ZZ )
14 znegcl 
 |-  ( C e. ZZ -> -u C e. ZZ )
15 znegcl 
 |-  ( B e. ZZ -> -u B e. ZZ )
16 elfz 
 |-  ( ( -u A e. ZZ /\ -u C e. ZZ /\ -u B e. ZZ ) -> ( -u A e. ( -u C ... -u B ) <-> ( -u C <_ -u A /\ -u A <_ -u B ) ) )
17 13 14 15 16 syl3an 
 |-  ( ( A e. ZZ /\ C e. ZZ /\ B e. ZZ ) -> ( -u A e. ( -u C ... -u B ) <-> ( -u C <_ -u A /\ -u A <_ -u B ) ) )
18 17 3com23 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( -u A e. ( -u C ... -u B ) <-> ( -u C <_ -u A /\ -u A <_ -u B ) ) )
19 11 12 18 3bitr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A e. ( B ... C ) <-> -u A e. ( -u C ... -u B ) ) )