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∈AB↔−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∈AB↔C∈ℝ∧A≤C∧C≤B
15 14 3adant3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈AB↔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∈AB↔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∈AB↔−C∈−B−A