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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )

Proof

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