Step |
Hyp |
Ref |
Expression |
1 |
|
letric |
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B <_ A ) ) |
2 |
1
|
orcomd |
|- ( ( A e. RR /\ B e. RR ) -> ( B <_ A \/ A <_ B ) ) |
3 |
|
avgle2 |
|- ( ( B e. RR /\ A e. RR ) -> ( B <_ A <-> ( ( B + A ) / 2 ) <_ A ) ) |
4 |
3
|
ancoms |
|- ( ( A e. RR /\ B e. RR ) -> ( B <_ A <-> ( ( B + A ) / 2 ) <_ A ) ) |
5 |
|
recn |
|- ( A e. RR -> A e. CC ) |
6 |
|
recn |
|- ( B e. RR -> B e. CC ) |
7 |
|
addcom |
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) ) |
8 |
5 6 7
|
syl2an |
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) ) |
9 |
8
|
oveq1d |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) / 2 ) = ( ( B + A ) / 2 ) ) |
10 |
9
|
breq1d |
|- ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) <_ A <-> ( ( B + A ) / 2 ) <_ A ) ) |
11 |
4 10
|
bitr4d |
|- ( ( A e. RR /\ B e. RR ) -> ( B <_ A <-> ( ( A + B ) / 2 ) <_ A ) ) |
12 |
|
avgle2 |
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( ( A + B ) / 2 ) <_ B ) ) |
13 |
11 12
|
orbi12d |
|- ( ( A e. RR /\ B e. RR ) -> ( ( B <_ A \/ A <_ B ) <-> ( ( ( A + B ) / 2 ) <_ A \/ ( ( A + B ) / 2 ) <_ B ) ) ) |
14 |
2 13
|
mpbid |
|- ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) <_ A \/ ( ( A + B ) / 2 ) <_ B ) ) |