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

Metamath Proof Explorer

Theorem avgle2

Description: Ordering property for average. (Contributed by Jeff Hankins, 15-Sep-2013) (Revised by Mario Carneiro, 28-May-2014)

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

Proof

Step Hyp Ref Expression
1 avglt1 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B < A <-> B < ( ( B + A ) / 2 ) ) )
2 1 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A <-> B < ( ( B + A ) / 2 ) ) )
3 recn 
 |-  ( A e. RR -> A e. CC )
4 recn 
 |-  ( B e. RR -> B e. CC )
5 addcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
6 3 4 5 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
7 6 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) / 2 ) = ( ( B + A ) / 2 ) )
8 7 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < ( ( A + B ) / 2 ) <-> B < ( ( B + A ) / 2 ) ) )
9 2 8 bitr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A <-> B < ( ( A + B ) / 2 ) ) )
10 9 notbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. B < A <-> -. B < ( ( A + B ) / 2 ) ) )
11 lenlt 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
12 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
13 rehalfcl 
 |-  ( ( A + B ) e. RR -> ( ( A + B ) / 2 ) e. RR )
14 12 13 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) / 2 ) e. RR )
15 lenlt 
 |-  ( ( ( ( A + B ) / 2 ) e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) <_ B <-> -. B < ( ( A + B ) / 2 ) ) )
16 14 15 sylancom 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) <_ B <-> -. B < ( ( A + B ) / 2 ) ) )
17 10 11 16 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( ( A + B ) / 2 ) <_ B ) )