Metamath Proof Explorer

Theorem elicc2

Description: Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007) (Revised by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A ≤ C ∧ C ≤ B

Proof

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