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

Proof

Step Hyp Ref Expression
1 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
2 elico1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ * ∧ A ≤ C ∧ C < B
3 1 2 sylan ⊢ A ∈ ℝ ∧ B ∈ ℝ * → C ∈ A B ↔ 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 ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C < B