Metamath Proof Explorer

Theorem avgle

Description: The average of two numbers is less than or equal to at least one of them. (Contributed by NM, 9-Dec-2005) (Revised by Mario Carneiro, 28-May-2014)

Ref Expression
Assertion avgle ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ≤ A ∨ A + B 2 ≤ B

Proof

Step Hyp Ref Expression
1 letric ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∨ B ≤ A
2 1 orcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ∨ A ≤ B
3 avgle2 ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A ↔ B + A 2 ≤ A
4 3 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ↔ B + A 2 ≤ A
5 recn ⊢ A ∈ ℝ → A ∈ ℂ
6 recn ⊢ B ∈ ℝ → B ∈ ℂ
7 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
8 5 6 7 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B = B + A
9 8 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 = B + A 2
10 9 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ≤ A ↔ B + A 2 ≤ A
11 4 10 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ↔ A + B 2 ≤ A
12 avgle2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A + B 2 ≤ B
13 11 12 orbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ∨ A ≤ B ↔ A + B 2 ≤ A ∨ A + B 2 ≤ B
14 2 13 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 ≤ A ∨ A + B 2 ≤ B