Theorem fzneg

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

	Ref	Expression
Assertion	fzneg	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∈ ( 𝐵 ... 𝐶 ) ↔ - 𝐴 ∈ ( - 𝐶 ... - 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐶 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐴 ) )
2		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
3	2	3ad2ant1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℝ )
4		zre	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℝ )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℝ )
6	3 5	lenegd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ≤ 𝐶 ↔ - 𝐶 ≤ - 𝐴 ) )
7		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
8	7	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℝ )
9	8 3	lenegd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 ↔ - 𝐴 ≤ - 𝐵 ) )
10	6 9	anbi12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐴 ) ↔ ( - 𝐶 ≤ - 𝐴 ∧ - 𝐴 ≤ - 𝐵 ) ) )
11	1 10	bitrid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐶 ) ↔ ( - 𝐶 ≤ - 𝐴 ∧ - 𝐴 ≤ - 𝐵 ) ) )
12		elfz	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∈ ( 𝐵 ... 𝐶 ) ↔ ( 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐶 ) ) )
13		znegcl	⊢ ( 𝐴 ∈ ℤ → - 𝐴 ∈ ℤ )
14		znegcl	⊢ ( 𝐶 ∈ ℤ → - 𝐶 ∈ ℤ )
15		znegcl	⊢ ( 𝐵 ∈ ℤ → - 𝐵 ∈ ℤ )
16		elfz	⊢ ( ( - 𝐴 ∈ ℤ ∧ - 𝐶 ∈ ℤ ∧ - 𝐵 ∈ ℤ ) → ( - 𝐴 ∈ ( - 𝐶 ... - 𝐵 ) ↔ ( - 𝐶 ≤ - 𝐴 ∧ - 𝐴 ≤ - 𝐵 ) ) )
17	13 14 15 16	syl3an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( - 𝐴 ∈ ( - 𝐶 ... - 𝐵 ) ↔ ( - 𝐶 ≤ - 𝐴 ∧ - 𝐴 ≤ - 𝐵 ) ) )
18	17	3com23	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( - 𝐴 ∈ ( - 𝐶 ... - 𝐵 ) ↔ ( - 𝐶 ≤ - 𝐴 ∧ - 𝐴 ≤ - 𝐵 ) ) )
19	11 12 18	3bitr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∈ ( 𝐵 ... 𝐶 ) ↔ - 𝐴 ∈ ( - 𝐶 ... - 𝐵 ) ) )