# 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\in \left({B}\dots {C}\right)↔-{A}\in \left(-{C}\dots -{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ancom ${⊢}\left({B}\le {A}\wedge {A}\le {C}\right)↔\left({A}\le {C}\wedge {B}\le {A}\right)$
2 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
3 2 3ad2ant1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {A}\in ℝ$
4 zre ${⊢}{C}\in ℤ\to {C}\in ℝ$
5 4 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {C}\in ℝ$
6 3 5 lenegd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\le {C}↔-{C}\le -{A}\right)$
7 zre ${⊢}{B}\in ℤ\to {B}\in ℝ$
8 7 3ad2ant2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to {B}\in ℝ$
9 8 3 lenegd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({B}\le {A}↔-{A}\le -{B}\right)$
10 6 9 anbi12d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left(\left({A}\le {C}\wedge {B}\le {A}\right)↔\left(-{C}\le -{A}\wedge -{A}\le -{B}\right)\right)$
11 1 10 syl5bb ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left(\left({B}\le {A}\wedge {A}\le {C}\right)↔\left(-{C}\le -{A}\wedge -{A}\le -{B}\right)\right)$
12 elfz ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\in \left({B}\dots {C}\right)↔\left({B}\le {A}\wedge {A}\le {C}\right)\right)$
13 znegcl ${⊢}{A}\in ℤ\to -{A}\in ℤ$
14 znegcl ${⊢}{C}\in ℤ\to -{C}\in ℤ$
15 znegcl ${⊢}{B}\in ℤ\to -{B}\in ℤ$
16 elfz ${⊢}\left(-{A}\in ℤ\wedge -{C}\in ℤ\wedge -{B}\in ℤ\right)\to \left(-{A}\in \left(-{C}\dots -{B}\right)↔\left(-{C}\le -{A}\wedge -{A}\le -{B}\right)\right)$
17 13 14 15 16 syl3an ${⊢}\left({A}\in ℤ\wedge {C}\in ℤ\wedge {B}\in ℤ\right)\to \left(-{A}\in \left(-{C}\dots -{B}\right)↔\left(-{C}\le -{A}\wedge -{A}\le -{B}\right)\right)$
18 17 3com23 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left(-{A}\in \left(-{C}\dots -{B}\right)↔\left(-{C}\le -{A}\wedge -{A}\le -{B}\right)\right)$
19 11 12 18 3bitr4d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\to \left({A}\in \left({B}\dots {C}\right)↔-{A}\in \left(-{C}\dots -{B}\right)\right)$