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