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\leftrightarrow 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\leftrightarrow \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)$$