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 ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ B … C ↔ − A ∈ − C … − B

Proof

Step Hyp Ref Expression
1 ancom ⊢ B ≤ A ∧ A ≤ C ↔ A ≤ C ∧ B ≤ A
2 zre ⊢ A ∈ ℤ → A ∈ ℝ
3 2 3ad2ant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℝ
4 zre ⊢ C ∈ ℤ → C ∈ ℝ
5 4 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → C ∈ ℝ
6 3 5 lenegd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ≤ C ↔ − C ≤ − A
7 zre ⊢ B ∈ ℤ → B ∈ ℝ
8 7 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∈ ℝ
9 8 3 lenegd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ≤ A ↔ − A ≤ − B
10 6 9 anbi12d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ≤ C ∧ B ≤ A ↔ − C ≤ − A ∧ − A ≤ − B
11 1 10 bitrid ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ≤ A ∧ A ≤ C ↔ − C ≤ − A ∧ − A ≤ − B
12 elfz ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ B … C ↔ B ≤ A ∧ A ≤ C
13 znegcl ⊢ A ∈ ℤ → − A ∈ ℤ
14 znegcl ⊢ C ∈ ℤ → − C ∈ ℤ
15 znegcl ⊢ B ∈ ℤ → − B ∈ ℤ
16 elfz ⊢ − A ∈ ℤ ∧ − C ∈ ℤ ∧ − B ∈ ℤ → − A ∈ − C … − B ↔ − C ≤ − A ∧ − A ≤ − B
17 13 14 15 16 syl3an ⊢ A ∈ ℤ ∧ C ∈ ℤ ∧ B ∈ ℤ → − A ∈ − C … − B ↔ − C ≤ − A ∧ − A ≤ − B
18 17 3com23 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → − A ∈ − C … − B ↔ − C ≤ − A ∧ − A ≤ − B
19 11 12 18 3bitr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ B … C ↔ − A ∈ − C … − B