Metamath Proof Explorer

Theorem avglt1

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

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

Proof

Step Hyp Ref Expression
1 ltadd2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → A < B ↔ A + A < A + B
2 1 3anidm13 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A + A < A + B
3 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
4 3 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℂ
5 times2 ⊢ A ∈ ℂ → A ⋅ 2 = A + A
6 4 5 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⋅ 2 = A + A
7 6 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⋅ 2 < A + B ↔ A + A < A + B
8 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
9 2re ⊢ 2 ∈ ℝ
10 2pos ⊢ 0 < 2
11 9 10 pm3.2i ⊢ 2 ∈ ℝ ∧ 0 < 2
12 11 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ → 2 ∈ ℝ ∧ 0 < 2
13 ltmuldiv ⊢ A ∈ ℝ ∧ A + B ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 → A ⋅ 2 < A + B ↔ A < A + B 2
14 3 8 12 13 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⋅ 2 < A + B ↔ A < A + B 2
15 2 7 14 3bitr2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A < A + B 2