Metamath Proof Explorer

Theorem avglt2

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

Ref Expression
Assertion avglt2 ⊢A∈ℝ∧B∈ℝ→A<B↔A+B2<B

Proof

Step Hyp Ref Expression
1 simpr ⊢A∈ℝ∧B∈ℝ→B∈ℝ
2 1 recnd ⊢A∈ℝ∧B∈ℝ→B∈ℂ
3 2times ⊢B∈ℂ→2⁢B=B+B
4 2 3 syl ⊢A∈ℝ∧B∈ℝ→2⁢B=B+B
5 4 breq2d ⊢A∈ℝ∧B∈ℝ→A+B<2⁢B↔A+B<B+B
6 readdcl ⊢A∈ℝ∧B∈ℝ→A+B∈ℝ
7 2re ⊢2∈ℝ
8 2pos ⊢0<2
9 7 8 pm3.2i ⊢2∈ℝ∧0<2
10 9 a1i ⊢A∈ℝ∧B∈ℝ→2∈ℝ∧0<2
11 ltdivmul ⊢A+B∈ℝ∧B∈ℝ∧2∈ℝ∧0<2→A+B2<B↔A+B<2⁢B
12 6 1 10 11 syl3anc ⊢A∈ℝ∧B∈ℝ→A+B2<B↔A+B<2⁢B
13 ltadd1 ⊢A∈ℝ∧B∈ℝ∧B∈ℝ→A<B↔A+B<B+B
14 13 3anidm23 ⊢A∈ℝ∧B∈ℝ→A<B↔A+B<B+B
15 5 12 14 3bitr4rd ⊢A∈ℝ∧B∈ℝ→A<B↔A+B2<B