Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( A e. RR /\ B e. RR ) -> B e. RR ) |
2 |
1
|
recnd |
|- ( ( A e. RR /\ B e. RR ) -> B e. CC ) |
3 |
|
2times |
|- ( B e. CC -> ( 2 x. B ) = ( B + B ) ) |
4 |
2 3
|
syl |
|- ( ( A e. RR /\ B e. RR ) -> ( 2 x. B ) = ( B + B ) ) |
5 |
4
|
breq2d |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) < ( 2 x. B ) <-> ( A + B ) < ( B + B ) ) ) |
6 |
|
readdcl |
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR ) |
7 |
|
2re |
|- 2 e. RR |
8 |
|
2pos |
|- 0 < 2 |
9 |
7 8
|
pm3.2i |
|- ( 2 e. RR /\ 0 < 2 ) |
10 |
9
|
a1i |
|- ( ( A e. RR /\ B e. RR ) -> ( 2 e. RR /\ 0 < 2 ) ) |
11 |
|
ltdivmul |
|- ( ( ( A + B ) e. RR /\ B e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( A + B ) / 2 ) < B <-> ( A + B ) < ( 2 x. B ) ) ) |
12 |
6 1 10 11
|
syl3anc |
|- ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) < B <-> ( A + B ) < ( 2 x. B ) ) ) |
13 |
|
ltadd1 |
|- ( ( A e. RR /\ B e. RR /\ B e. RR ) -> ( A < B <-> ( A + B ) < ( B + B ) ) ) |
14 |
13
|
3anidm23 |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A + B ) < ( B + B ) ) ) |
15 |
5 12 14
|
3bitr4rd |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( A + B ) / 2 ) < B ) ) |