Metamath Proof Explorer

Theorem iooneg

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

Ref Expression
Assertion iooneg ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ - 𝐶 ∈ ( - 𝐵 (,) - 𝐴 ) ) )

Proof

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