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

Metamath Proof Explorer

Theorem avglt1

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

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

Proof

Step Hyp Ref Expression
1 ltadd2 
 |-  ( ( A e. RR /\ B e. RR /\ A e. RR ) -> ( A < B <-> ( A + A ) < ( A + B ) ) )
2 1 3anidm13 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A + A ) < ( A + B ) ) )
3 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
4 3 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. CC )
5 times2 
 |-  ( A e. CC -> ( A x. 2 ) = ( A + A ) )
6 4 5 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. 2 ) = ( A + A ) )
7 6 breq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. 2 ) < ( A + B ) <-> ( A + A ) < ( A + B ) ) )
8 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
9 2re 
 |-  2 e. RR
10 2pos 
 |-  0 < 2
11 9 10 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
12 11 a1i 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2 e. RR /\ 0 < 2 ) )
13 ltmuldiv 
 |-  ( ( A e. RR /\ ( A + B ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( A x. 2 ) < ( A + B ) <-> A < ( ( A + B ) / 2 ) ) )
14 3 8 12 13 syl3anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. 2 ) < ( A + B ) <-> A < ( ( A + B ) / 2 ) ) )
15 2 7 14 3bitr2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A < ( ( A + B ) / 2 ) ) )