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∈AB↔−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∈AB↔A<C∧C<B
12 8 9 10 11 syl3an ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈AB↔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∈AB↔−C∈−B−A