Metamath Proof Explorer


Theorem iooltubd

Description: An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 iooltubd.1 ( 𝜑𝐴 ∈ ℝ* )
2 iooltubd.2 ( 𝜑𝐵 ∈ ℝ* )
3 iooltubd.3 ( 𝜑𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
4 iooltub ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 < 𝐵 )
5 1 2 3 4 syl3anc ( 𝜑𝐶 < 𝐵 )