Metamath Proof Explorer

Theorem avgle1

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

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

Proof

Step Hyp Ref Expression
1 avglt2 ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A ↔ B + A 2 < A
2 1 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A ↔ B + A 2 < A
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 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B 2 < A ↔ B + A 2 < A
9 2 8 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A ↔ A + B 2 < A
10 9 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B < A ↔ ¬ A + B 2 < A
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 ∈ ℝ ∧ A + B 2 ∈ ℝ → A ≤ A + B 2 ↔ ¬ A + B 2 < A
16 14 15 syldan ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ A + B 2 ↔ ¬ A + B 2 < A
17 10 11 16 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A ≤ A + B 2