Metamath Proof Explorer

Theorem lerec2

Description: Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005)

Ref Expression
Assertion lerec2 
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ ( 1 / B ) <-> B <_ ( 1 / A ) ) )

Proof

Step Hyp Ref Expression
1 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
2 rereccl 
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( 1 / B ) e. RR )
3 1 2 syldan 
 |-  ( ( B e. RR /\ 0 < B ) -> ( 1 / B ) e. RR )
4 recgt0 
 |-  ( ( B e. RR /\ 0 < B ) -> 0 < ( 1 / B ) )
5 3 4 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( ( 1 / B ) e. RR /\ 0 < ( 1 / B ) ) )
6 lerec 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( ( 1 / B ) e. RR /\ 0 < ( 1 / B ) ) ) -> ( A <_ ( 1 / B ) <-> ( 1 / ( 1 / B ) ) <_ ( 1 / A ) ) )
7 5 6 sylan2 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ ( 1 / B ) <-> ( 1 / ( 1 / B ) ) <_ ( 1 / A ) ) )
8 recn 
 |-  ( B e. RR -> B e. CC )
9 recrec 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 1 / ( 1 / B ) ) = B )
10 8 1 9 syl2an2r 
 |-  ( ( B e. RR /\ 0 < B ) -> ( 1 / ( 1 / B ) ) = B )
11 10 adantl 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( 1 / ( 1 / B ) ) = B )
12 11 breq1d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / ( 1 / B ) ) <_ ( 1 / A ) <-> B <_ ( 1 / A ) ) )
13 7 12 bitrd 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ ( 1 / B ) <-> B <_ ( 1 / A ) ) )