Metamath Proof Explorer

Theorem iccneg

Description: Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007)

Ref Expression
Assertion iccneg ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ - 𝐶 ∈ ( - 𝐵 [,] - 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 renegcl ⊢ ( 𝐶 ∈ ℝ → - 𝐶 ∈ ℝ )
2 ax-1 ⊢ ( 𝐶 ∈ ℝ → ( - 𝐶 ∈ ℝ → 𝐶 ∈ ℝ ) )
3 1 2 impbid2 ⊢ ( 𝐶 ∈ ℝ → ( 𝐶 ∈ ℝ ↔ - 𝐶 ∈ ℝ ) )
4 3 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ℝ ↔ - 𝐶 ∈ ℝ ) )
5 ancom ⊢ ( ( 𝐶 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) )
6 leneg ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝐶 ) )
7 6 ancoms ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝐶 ) )
8 7 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝐶 ) )
9 leneg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐶 ↔ - 𝐶 ≤ - 𝐴 ) )
10 9 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐶 ↔ - 𝐶 ≤ - 𝐴 ) )
11 8 10 anbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) ↔ ( - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) )
12 5 11 bitr3id ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ↔ ( - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) )
13 4 12 anbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) ↔ ( - 𝐶 ∈ ℝ ∧ ( - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) ) )
14 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
15 14 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
16 3anass ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
17 15 16 bitrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) ) )
18 renegcl ⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
19 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
20 elicc2 ⊢ ( ( - 𝐵 ∈ ℝ ∧ - 𝐴 ∈ ℝ ) → ( - 𝐶 ∈ ( - 𝐵 [,] - 𝐴 ) ↔ ( - 𝐶 ∈ ℝ ∧ - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) )
21 18 19 20 syl2anr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐶 ∈ ( - 𝐵 [,] - 𝐴 ) ↔ ( - 𝐶 ∈ ℝ ∧ - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) )
22 21 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( - 𝐶 ∈ ( - 𝐵 [,] - 𝐴 ) ↔ ( - 𝐶 ∈ ℝ ∧ - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) )
23 3anass ⊢ ( ( - 𝐶 ∈ ℝ ∧ - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ↔ ( - 𝐶 ∈ ℝ ∧ ( - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) )
24 22 23 bitrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( - 𝐶 ∈ ( - 𝐵 [,] - 𝐴 ) ↔ ( - 𝐶 ∈ ℝ ∧ ( - 𝐵 ≤ - 𝐶 ∧ - 𝐶 ≤ - 𝐴 ) ) ) )
25 13 17 24 3bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ - 𝐶 ∈ ( - 𝐵 [,] - 𝐴 ) ) )