Metamath Proof Explorer

Theorem avgle2

Description: Ordering property for average. (Contributed by Jeff Hankins, 15-Sep-2013) (Revised by Mario Carneiro, 28-May-2014)

Ref Expression
Assertion avgle2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A + B 2 ≤ B

Proof

Step Hyp Ref Expression
1 avglt1 ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A ↔ B < B + A 2
2 1 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A ↔ B < B + A 2
3 recn ⊢ A ∈ ℝ → A ∈ ℂ
4 recn ⊢ B ∈ ℝ → B ∈ ℂ
5 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
6 3 4 5 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B = B + A
7 6 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 = B + A 2
8 7 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A + B 2 ↔ B < B + A 2
9 2 8 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A ↔ B < A + B 2
10 9 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B < A ↔ ¬ B < A + B 2
11 lenlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A
12 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
13 rehalfcl ⊢ A + B ∈ ℝ → A + B 2 ∈ ℝ
14 12 13 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ∈ ℝ
15 lenlt ⊢ A + B 2 ∈ ℝ ∧ B ∈ ℝ → A + B 2 ≤ B ↔ ¬ B < A + B 2
16 14 15 sylancom ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ≤ B ↔ ¬ B < A + B 2
17 10 11 16 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A + B 2 ≤ B