This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem avglt2

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

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

Proof

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