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 ⊢A∈ℝ∧B∈ℝ*→C∈AB↔C∈ℝ∧A≤C∧C<B

Proof

Step Hyp Ref Expression
1 rexr ⊢A∈ℝ→A∈ℝ*
2 elico1 ⊢A∈ℝ*∧B∈ℝ*→C∈AB↔C∈ℝ*∧A≤C∧C<B
3 1 2 sylan ⊢A∈ℝ∧B∈ℝ*→C∈AB↔C∈ℝ*∧A≤C∧C<B
4 mnfxr ⊢−∞∈ℝ*
5 4 a1i ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→−∞∈ℝ*
6 1 ad2antrr ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→A∈ℝ*
7 simpr1 ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→C∈ℝ*
8 mnflt ⊢A∈ℝ→−∞<A
9 8 ad2antrr ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→−∞<A
10 simpr2 ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→A≤C
11 5 6 7 9 10 xrltletrd ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→−∞<C
12 simplr ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→B∈ℝ*
13 pnfxr ⊢+∞∈ℝ*
14 13 a1i ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→+∞∈ℝ*
15 simpr3 ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→C<B
16 pnfge ⊢B∈ℝ*→B≤+∞
17 16 ad2antlr ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→B≤+∞
18 7 12 14 15 17 xrltletrd ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→C<+∞
19 xrrebnd ⊢C∈ℝ*→C∈ℝ↔−∞<C∧C<+∞
20 7 19 syl ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→C∈ℝ↔−∞<C∧C<+∞
21 11 18 20 mpbir2and ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→C∈ℝ
22 21 10 15 3jca ⊢A∈ℝ∧B∈ℝ*∧C∈ℝ*∧A≤C∧C<B→C∈ℝ∧A≤C∧C<B
23 22 ex ⊢A∈ℝ∧B∈ℝ*→C∈ℝ*∧A≤C∧C<B→C∈ℝ∧A≤C∧C<B
24 rexr ⊢C∈ℝ→C∈ℝ*
25 24 3anim1i ⊢C∈ℝ∧A≤C∧C<B→C∈ℝ*∧A≤C∧C<B
26 23 25 impbid1 ⊢A∈ℝ∧B∈ℝ*→C∈ℝ*∧A≤C∧C<B↔C∈ℝ∧A≤C∧C<B
27 3 26 bitrd ⊢A∈ℝ∧B∈ℝ*→C∈AB↔C∈ℝ∧A≤C∧C<B