Metamath Proof Explorer


Theorem avgle1

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

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

Proof

Step Hyp Ref Expression
1 avglt2
 |-  ( ( B e. RR /\ A e. RR ) -> ( B < A <-> ( ( B + A ) / 2 ) < A ) )
2 1 ancoms
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A <-> ( ( B + A ) / 2 ) < A ) )
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 breq1d
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) < A <-> ( ( B + A ) / 2 ) < A ) )
9 2 8 bitr4d
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < A <-> ( ( A + B ) / 2 ) < A ) )
10 9 notbid
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. B < A <-> -. ( ( A + B ) / 2 ) < A ) )
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 e. RR /\ ( ( A + B ) / 2 ) e. RR ) -> ( A <_ ( ( A + B ) / 2 ) <-> -. ( ( A + B ) / 2 ) < A ) )
16 14 15 syldan
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ ( ( A + B ) / 2 ) <-> -. ( ( A + B ) / 2 ) < A ) )
17 10 11 16 3bitr4d
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A <_ ( ( A + B ) / 2 ) ) )