Metamath Proof Explorer

Theorem iccneg

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

Ref Expression
Assertion iccneg ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ A B ↔ − C ∈ − B − A

Proof

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