Metamath Proof Explorer

Theorem ltrec1

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

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

Proof

Step Hyp Ref Expression
1 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
2 rereccl 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
3 1 2 syldan 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
4 recgt0 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )
5 3 4 jca 
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 / A ) e. RR /\ 0 < ( 1 / A ) ) )
6 ltrec 
 |-  ( ( ( ( 1 / A ) e. RR /\ 0 < ( 1 / A ) ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / A ) < B <-> ( 1 / B ) < ( 1 / ( 1 / A ) ) ) )
7 5 6 sylan 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / A ) < B <-> ( 1 / B ) < ( 1 / ( 1 / A ) ) ) )
8 recn 
 |-  ( A e. RR -> A e. CC )
9 recrec 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = A )
10 8 9 sylan 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = A )
11 1 10 syldan 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / ( 1 / A ) ) = A )
12 11 adantr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( 1 / ( 1 / A ) ) = A )
13 12 breq2d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / B ) < ( 1 / ( 1 / A ) ) <-> ( 1 / B ) < A ) )
14 7 13 bitrd 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / A ) < B <-> ( 1 / B ) < A ) )