Theorem avglt1

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

	Ref	Expression
Assertion	avglt1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) ) )

Proof

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