This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem recgt0ii

Description: The reciprocal of a positive number is positive. Exercise 4 of Apostol p. 21. (Contributed by NM, 15-May-1999)

Ref Expression
Hypotheses ltplus1.1 
|- A e. RR
recgt0i.2 
|- 0 < A
Assertion recgt0ii 
|- 0 < ( 1 / A )

Proof

Step Hyp Ref Expression
1 ltplus1.1 
 |-  A e. RR
2 recgt0i.2 
 |-  0 < A
3 ax-1cn 
 |-  1 e. CC
4 1 recni 
 |-  A e. CC
5 ax-1ne0 
 |-  1 =/= 0
6 1 2 gt0ne0ii 
 |-  A =/= 0
7 3 4 5 6 divne0i 
 |-  ( 1 / A ) =/= 0
8 7 nesymi 
 |-  -. 0 = ( 1 / A )
9 0lt1 
 |-  0 < 1
10 0re 
 |-  0 e. RR
11 1re 
 |-  1 e. RR
12 10 11 ltnsymi 
 |-  ( 0 < 1 -> -. 1 < 0 )
13 9 12 ax-mp 
 |-  -. 1 < 0
14 1 6 rereccli 
 |-  ( 1 / A ) e. RR
15 14 renegcli 
 |-  -u ( 1 / A ) e. RR
16 15 1 mulgt0i 
 |-  ( ( 0 < -u ( 1 / A ) /\ 0 < A ) -> 0 < ( -u ( 1 / A ) x. A ) )
17 2 16 mpan2 
 |-  ( 0 < -u ( 1 / A ) -> 0 < ( -u ( 1 / A ) x. A ) )
18 14 recni 
 |-  ( 1 / A ) e. CC
19 18 4 mulneg1i 
 |-  ( -u ( 1 / A ) x. A ) = -u ( ( 1 / A ) x. A )
20 4 6 recidi 
 |-  ( A x. ( 1 / A ) ) = 1
21 4 18 20 mulcomli 
 |-  ( ( 1 / A ) x. A ) = 1
22 21 negeqi 
 |-  -u ( ( 1 / A ) x. A ) = -u 1
23 19 22 eqtri 
 |-  ( -u ( 1 / A ) x. A ) = -u 1
24 17 23 breqtrdi 
 |-  ( 0 < -u ( 1 / A ) -> 0 < -u 1 )
25 lt0neg1 
 |-  ( ( 1 / A ) e. RR -> ( ( 1 / A ) < 0 <-> 0 < -u ( 1 / A ) ) )
26 14 25 ax-mp 
 |-  ( ( 1 / A ) < 0 <-> 0 < -u ( 1 / A ) )
27 lt0neg1 
 |-  ( 1 e. RR -> ( 1 < 0 <-> 0 < -u 1 ) )
28 11 27 ax-mp 
 |-  ( 1 < 0 <-> 0 < -u 1 )
29 24 26 28 3imtr4i 
 |-  ( ( 1 / A ) < 0 -> 1 < 0 )
30 13 29 mto 
 |-  -. ( 1 / A ) < 0
31 8 30 pm3.2ni 
 |-  -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 )
32 axlttri 
 |-  ( ( 0 e. RR /\ ( 1 / A ) e. RR ) -> ( 0 < ( 1 / A ) <-> -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) ) )
33 10 14 32 mp2an 
 |-  ( 0 < ( 1 / A ) <-> -. ( 0 = ( 1 / A ) \/ ( 1 / A ) < 0 ) )
34 31 33 mpbir 
 |-  0 < ( 1 / A )