Metamath Proof Explorer


Theorem eliood

Description: Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses eliood.1 ( 𝜑𝐴 ∈ ℝ* )
eliood.2 ( 𝜑𝐵 ∈ ℝ* )
eliood.3 ( 𝜑𝐶 ∈ ℝ )
eliood.4 ( 𝜑𝐴 < 𝐶 )
eliood.5 ( 𝜑𝐶 < 𝐵 )
Assertion eliood ( 𝜑𝐶 ∈ ( 𝐴 (,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eliood.1 ( 𝜑𝐴 ∈ ℝ* )
2 eliood.2 ( 𝜑𝐵 ∈ ℝ* )
3 eliood.3 ( 𝜑𝐶 ∈ ℝ )
4 eliood.4 ( 𝜑𝐴 < 𝐶 )
5 eliood.5 ( 𝜑𝐶 < 𝐵 )
6 elioo2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶 < 𝐵 ) ) )
7 1 2 6 syl2anc ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶𝐶 < 𝐵 ) ) )
8 3 4 5 7 mpbir3and ( 𝜑𝐶 ∈ ( 𝐴 (,) 𝐵 ) )