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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A + B 2 ∈ A B

Proof

Step Hyp Ref Expression
1 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
2 1 3ad2ant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A ∈ ℝ *
3 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
4 3 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → B ∈ ℝ *
5 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
6 5 rehalfcld ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ∈ ℝ
7 6 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A + B 2 ∈ ℝ
8 avglt1 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A < A + B 2
9 8 biimp3a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A < A + B 2
10 avglt2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A + B 2 < B
11 10 biimp3a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A + B 2 < B
12 2 4 7 9 11 eliood ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A + B 2 ∈ A B