# Metamath Proof Explorer

## Theorem elico2

Description: Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008) (Revised by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion elico2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left[{A},{B}\right)↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
2 elico1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left[{A},{B}\right)↔\left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$
3 1 2 sylan ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left[{A},{B}\right)↔\left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$
4 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
5 4 a1i ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
6 1 ad2antrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {A}\in {ℝ}^{*}$
7 simpr1 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {C}\in {ℝ}^{*}$
8 mnflt ${⊢}{A}\in ℝ\to \mathrm{-\infty }<{A}$
9 8 ad2antrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to \mathrm{-\infty }<{A}$
10 simpr2 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {A}\le {C}$
11 5 6 7 9 10 xrltletrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to \mathrm{-\infty }<{C}$
12 simplr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {B}\in {ℝ}^{*}$
13 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
14 13 a1i ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
15 simpr3 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {C}<{B}$
16 pnfge ${⊢}{B}\in {ℝ}^{*}\to {B}\le \mathrm{+\infty }$
17 16 ad2antlr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {B}\le \mathrm{+\infty }$
18 7 12 14 15 17 xrltletrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {C}<\mathrm{+\infty }$
19 xrrebnd ${⊢}{C}\in {ℝ}^{*}\to \left({C}\in ℝ↔\left(\mathrm{-\infty }<{C}\wedge {C}<\mathrm{+\infty }\right)\right)$
20 7 19 syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to \left({C}\in ℝ↔\left(\mathrm{-\infty }<{C}\wedge {C}<\mathrm{+\infty }\right)\right)$
21 11 18 20 mpbir2and ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to {C}\in ℝ$
22 21 10 15 3jca ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)\to \left({C}\in ℝ\wedge {A}\le {C}\wedge {C}<{B}\right)$
23 22 ex ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\to \left({C}\in ℝ\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$
24 rexr ${⊢}{C}\in ℝ\to {C}\in {ℝ}^{*}$
25 24 3anim1i ${⊢}\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}<{B}\right)\to \left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)$
26 23 25 impbid1 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$
27 3 26 bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left[{A},{B}\right)↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$