Metamath Proof Explorer

Theorem recgt0

Description: The reciprocal of a positive number is positive. Exercise 4 of Apostol p. 21. (Contributed by NM, 25-Aug-1999) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. RR )
2 1 recnd 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. CC )
3 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
4 2 3 recne0d 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) =/= 0 )
5 4 necomd 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 =/= ( 1 / A ) )
6 5 neneqd 
 |-  ( ( A e. RR /\ 0 < A ) -> -. 0 = ( 1 / A ) )
7 0lt1 
 |-  0 < 1
8 0re 
 |-  0 e. RR
9 1re 
 |-  1 e. RR
10 8 9 ltnsymi 
 |-  ( 0 < 1 -> -. 1 < 0 )
11 7 10 ax-mp 
 |-  -. 1 < 0
12 simpll 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> A e. RR )
13 3 adantr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> A =/= 0 )
14 12 13 rereccld 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( 1 / A ) e. RR )
15 14 renegcld 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> -u ( 1 / A ) e. RR )
16 simpr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( 1 / A ) < 0 )
17 1 3 rereccld 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
18 17 adantr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( 1 / A ) e. RR )
19 18 lt0neg1d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( ( 1 / A ) < 0 <-> 0 < -u ( 1 / A ) ) )
20 16 19 mpbid 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> 0 < -u ( 1 / A ) )
21 simplr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> 0 < A )
22 15 12 20 21 mulgt0d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> 0 < ( -u ( 1 / A ) x. A ) )
23 2 adantr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> A e. CC )
24 23 13 reccld 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( 1 / A ) e. CC )
25 24 23 mulneg1d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( -u ( 1 / A ) x. A ) = -u ( ( 1 / A ) x. A ) )
26 23 13 recid2d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( ( 1 / A ) x. A ) = 1 )
27 26 negeqd 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> -u ( ( 1 / A ) x. A ) = -u 1 )
28 25 27 eqtrd 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( -u ( 1 / A ) x. A ) = -u 1 )
29 22 28 breqtrd 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> 0 < -u 1 )
30 1red 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> 1 e. RR )
31 30 lt0neg1d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> ( 1 < 0 <-> 0 < -u 1 ) )
32 29 31 mpbird 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( 1 / A ) < 0 ) -> 1 < 0 )
33 32 ex 
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 / A ) < 0 -> 1 < 0 ) )
34 11 33 mtoi 
 |-  ( ( A e. RR /\ 0 < A ) -> -. ( 1 / A ) < 0 )
35 ioran 
 |-  ( -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) <-> ( -. 0 = ( 1 / A ) /\ -. ( 1 / A ) < 0 ) )
36 6 34 35 sylanbrc 
 |-  ( ( A e. RR /\ 0 < A ) -> -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) )
37 axlttri 
 |-  ( ( 0 e. RR /\ ( 1 / A ) e. RR ) -> ( 0 < ( 1 / A ) <-> -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) ) )
38 8 17 37 sylancr 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 0 < ( 1 / A ) <-> -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) ) )
39 36 38 mpbird 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )