Metamath Proof Explorer

Theorem iccneg

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

Ref Expression
Assertion iccneg ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\in \left[{A},{B}\right]↔-{C}\in \left[-{B},-{A}\right]\right)$

Proof

Step Hyp Ref Expression
1 renegcl ${⊢}{C}\in ℝ\to -{C}\in ℝ$
2 ax-1 ${⊢}{C}\in ℝ\to \left(-{C}\in ℝ\to {C}\in ℝ\right)$
3 1 2 impbid2 ${⊢}{C}\in ℝ\to \left({C}\in ℝ↔-{C}\in ℝ\right)$
4 3 3ad2ant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\in ℝ↔-{C}\in ℝ\right)$
5 ancom ${⊢}\left({C}\le {B}\wedge {A}\le {C}\right)↔\left({A}\le {C}\wedge {C}\le {B}\right)$
6 leneg ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\right)\to \left({C}\le {B}↔-{B}\le -{C}\right)$
7 6 ancoms ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\le {B}↔-{B}\le -{C}\right)$
8 7 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\le {B}↔-{B}\le -{C}\right)$
9 leneg ${⊢}\left({A}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}\le {C}↔-{C}\le -{A}\right)$
10 9 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}\le {C}↔-{C}\le -{A}\right)$
11 8 10 anbi12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({C}\le {B}\wedge {A}\le {C}\right)↔\left(-{B}\le -{C}\wedge -{C}\le -{A}\right)\right)$
12 5 11 syl5bbr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({A}\le {C}\wedge {C}\le {B}\right)↔\left(-{B}\le -{C}\wedge -{C}\le -{A}\right)\right)$
13 4 12 anbi12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(\left({C}\in ℝ\wedge \left({A}\le {C}\wedge {C}\le {B}\right)\right)↔\left(-{C}\in ℝ\wedge \left(-{B}\le -{C}\wedge -{C}\le -{A}\right)\right)\right)$
14 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({C}\in \left[{A},{B}\right]↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}\le {B}\right)\right)$
15 14 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\in \left[{A},{B}\right]↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}\le {B}\right)\right)$
16 3anass ${⊢}\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}\le {B}\right)↔\left({C}\in ℝ\wedge \left({A}\le {C}\wedge {C}\le {B}\right)\right)$
17 15 16 syl6bb ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\in \left[{A},{B}\right]↔\left({C}\in ℝ\wedge \left({A}\le {C}\wedge {C}\le {B}\right)\right)\right)$
18 renegcl ${⊢}{B}\in ℝ\to -{B}\in ℝ$
19 renegcl ${⊢}{A}\in ℝ\to -{A}\in ℝ$
20 elicc2 ${⊢}\left(-{B}\in ℝ\wedge -{A}\in ℝ\right)\to \left(-{C}\in \left[-{B},-{A}\right]↔\left(-{C}\in ℝ\wedge -{B}\le -{C}\wedge -{C}\le -{A}\right)\right)$
21 18 19 20 syl2anr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(-{C}\in \left[-{B},-{A}\right]↔\left(-{C}\in ℝ\wedge -{B}\le -{C}\wedge -{C}\le -{A}\right)\right)$
22 21 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(-{C}\in \left[-{B},-{A}\right]↔\left(-{C}\in ℝ\wedge -{B}\le -{C}\wedge -{C}\le -{A}\right)\right)$
23 3anass ${⊢}\left(-{C}\in ℝ\wedge -{B}\le -{C}\wedge -{C}\le -{A}\right)↔\left(-{C}\in ℝ\wedge \left(-{B}\le -{C}\wedge -{C}\le -{A}\right)\right)$
24 22 23 syl6bb ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(-{C}\in \left[-{B},-{A}\right]↔\left(-{C}\in ℝ\wedge \left(-{B}\le -{C}\wedge -{C}\le -{A}\right)\right)\right)$
25 13 17 24 3bitr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({C}\in \left[{A},{B}\right]↔-{C}\in \left[-{B},-{A}\right]\right)$