Metamath Proof Explorer

Theorem ioomidp

Description: The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion ioomidp ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \frac{{A}+{B}}{2}\in \left({A},{B}\right)$

Proof

Step Hyp Ref Expression
1 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
2 1 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}\in {ℝ}^{*}$
3 rexr ${⊢}{B}\in ℝ\to {B}\in {ℝ}^{*}$
4 3 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}\in {ℝ}^{*}$
5 readdcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}+{B}\in ℝ$
6 5 rehalfcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \frac{{A}+{B}}{2}\in ℝ$
7 6 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \frac{{A}+{B}}{2}\in ℝ$
8 avglt1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔{A}<\frac{{A}+{B}}{2}\right)$
9 8 biimp3a ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}<\frac{{A}+{B}}{2}$
10 avglt2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔\frac{{A}+{B}}{2}<{B}\right)$
11 10 biimp3a ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \frac{{A}+{B}}{2}<{B}$
12 2 4 7 9 11 eliood ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \frac{{A}+{B}}{2}\in \left({A},{B}\right)$