Metamath Proof Explorer

Theorem avglt2

Description: Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Assertion avglt2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A + B 2 < B

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ∈ ℝ
2 1 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ∈ ℂ
3 2times ⊢ B ∈ ℂ → 2 ⁢ B = B + B
4 2 3 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → 2 ⁢ B = B + B
5 4 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B < 2 ⁢ B ↔ A + B < B + B
6 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
7 2re ⊢ 2 ∈ ℝ
8 2pos ⊢ 0 < 2
9 7 8 pm3.2i ⊢ 2 ∈ ℝ ∧ 0 < 2
10 9 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ → 2 ∈ ℝ ∧ 0 < 2
11 ltdivmul ⊢ A + B ∈ ℝ ∧ B ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 → A + B 2 < B ↔ A + B < 2 ⁢ B
12 6 1 10 11 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 < B ↔ A + B < 2 ⁢ B
13 ltadd1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A + B < B + B
14 13 3anidm23 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A + B < B + B
15 5 12 14 3bitr4rd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A + B 2 < B