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 ) )