Metamath Proof Explorer


Theorem avglt2

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

Ref Expression
Assertion avglt2
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
2 1 recnd
 |-  ( ( A e. RR /\ B e. RR ) -> B e. CC )
3 2times
 |-  ( B e. CC -> ( 2 x. B ) = ( B + B ) )
4 2 3 syl
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2 x. B ) = ( B + B ) )
5 4 breq2d
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) < ( 2 x. B ) <-> ( A + B ) < ( B + B ) ) )
6 readdcl
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
7 2re
 |-  2 e. RR
8 2pos
 |-  0 < 2
9 7 8 pm3.2i
 |-  ( 2 e. RR /\ 0 < 2 )
10 9 a1i
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2 e. RR /\ 0 < 2 ) )
11 ltdivmul
 |-  ( ( ( A + B ) e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( A + B ) / 2 ) < B <-> ( A + B ) < ( 2 x. B ) ) )
12 6 1 10 11 syl3anc
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) < B <-> ( A + B ) < ( 2 x. B ) ) )
13 ltadd1
 |-  ( ( A e. RR /\ B e. RR /\ B e. RR ) -> ( A < B <-> ( A + B ) < ( B + B ) ) )
14 13 3anidm23
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A + B ) < ( B + B ) ) )
15 5 12 14 3bitr4rd
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )