Step |
Hyp |
Ref |
Expression |
1 |
|
1red |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 1 e. RR ) |
2 |
|
simprl |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> B e. RR ) |
3 |
|
simpll |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> A e. RR ) |
4 |
|
simplr |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < A ) |
5 |
|
ltmuldiv |
|- ( ( 1 e. RR /\ B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( 1 x. A ) < B <-> 1 < ( B / A ) ) ) |
6 |
1 2 3 4 5
|
syl112anc |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 x. A ) < B <-> 1 < ( B / A ) ) ) |
7 |
3
|
recnd |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> A e. CC ) |
8 |
7
|
mulid2d |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( 1 x. A ) = A ) |
9 |
8
|
breq1d |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 x. A ) < B <-> A < B ) ) |
10 |
2
|
recnd |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> B e. CC ) |
11 |
4
|
gt0ne0d |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> A =/= 0 ) |
12 |
10 7 11
|
divrecd |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( B / A ) = ( B x. ( 1 / A ) ) ) |
13 |
12
|
breq2d |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( 1 < ( B / A ) <-> 1 < ( B x. ( 1 / A ) ) ) ) |
14 |
6 9 13
|
3bitr3d |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A < B <-> 1 < ( B x. ( 1 / A ) ) ) ) |
15 |
3 11
|
rereccld |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( 1 / A ) e. RR ) |
16 |
|
simprr |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < B ) |
17 |
|
ltdivmul |
|- ( ( 1 e. RR /\ ( 1 / A ) e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / B ) < ( 1 / A ) <-> 1 < ( B x. ( 1 / A ) ) ) ) |
18 |
1 15 2 16 17
|
syl112anc |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / B ) < ( 1 / A ) <-> 1 < ( B x. ( 1 / A ) ) ) ) |
19 |
14 18
|
bitr4d |
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) ) |