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