Metamath Proof Explorer

Theorem iooneg

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

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

Proof

Step Hyp Ref Expression
1 ltneg ⊢ A ∈ ℝ ∧ C ∈ ℝ → A < C ↔ − C < − A
2 1 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C ↔ − C < − A
3 ltneg ⊢ C ∈ ℝ ∧ B ∈ ℝ → C < B ↔ − B < − C
4 3 ancoms ⊢ B ∈ ℝ ∧ C ∈ ℝ → C < B ↔ − B < − C
5 4 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C < B ↔ − B < − C
6 2 5 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C ∧ C < B ↔ − C < − A ∧ − B < − C
7 6 biancomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C ∧ C < B ↔ − B < − C ∧ − C < − A
8 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
9 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
10 rexr ⊢ C ∈ ℝ → C ∈ ℝ *
11 elioo5 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A < C ∧ C < B
12 8 9 10 11 syl3an ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ A B ↔ A < C ∧ C < B
13 renegcl ⊢ B ∈ ℝ → − B ∈ ℝ
14 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
15 renegcl ⊢ C ∈ ℝ → − C ∈ ℝ
16 rexr ⊢ − B ∈ ℝ → − B ∈ ℝ *
17 rexr ⊢ − A ∈ ℝ → − A ∈ ℝ *
18 rexr ⊢ − C ∈ ℝ → − C ∈ ℝ *
19 elioo5 ⊢ − B ∈ ℝ * ∧ − A ∈ ℝ * ∧ − C ∈ ℝ * → − C ∈ − B − A ↔ − B < − C ∧ − C < − A
20 16 17 18 19 syl3an ⊢ − B ∈ ℝ ∧ − A ∈ ℝ ∧ − C ∈ ℝ → − C ∈ − B − A ↔ − B < − C ∧ − C < − A
21 13 14 15 20 syl3an ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ → − C ∈ − B − A ↔ − B < − C ∧ − C < − A
22 21 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → − C ∈ − B − A ↔ − B < − C ∧ − C < − A
23 7 12 22 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ A B ↔ − C ∈ − B − A