# 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 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<\frac{1}{{A}}$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\in ℝ$
2 1 recnd ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\in ℂ$
3 gt0ne0 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\ne 0$
4 2 3 recne0d ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \frac{1}{{A}}\ne 0$
5 4 necomd ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0\ne \frac{1}{{A}}$
6 5 neneqd ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to ¬0=\frac{1}{{A}}$
7 0lt1 ${⊢}0<1$
8 0re ${⊢}0\in ℝ$
9 1re ${⊢}1\in ℝ$
10 8 9 ltnsymi ${⊢}0<1\to ¬1<0$
11 7 10 ax-mp ${⊢}¬1<0$
12 simpll ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to {A}\in ℝ$
13 3 adantr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to {A}\ne 0$
14 12 13 rereccld ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \frac{1}{{A}}\in ℝ$
15 14 renegcld ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to -\frac{1}{{A}}\in ℝ$
16 simpr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \frac{1}{{A}}<0$
17 1 3 rereccld ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \frac{1}{{A}}\in ℝ$
18 17 adantr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \frac{1}{{A}}\in ℝ$
19 18 lt0neg1d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \left(\frac{1}{{A}}<0↔0<-\frac{1}{{A}}\right)$
20 16 19 mpbid ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to 0<-\frac{1}{{A}}$
21 simplr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to 0<{A}$
22 15 12 20 21 mulgt0d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to 0<\left(-\frac{1}{{A}}\right){A}$
23 2 adantr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to {A}\in ℂ$
24 23 13 reccld ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \frac{1}{{A}}\in ℂ$
25 24 23 mulneg1d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \left(-\frac{1}{{A}}\right){A}=-\left(\frac{1}{{A}}\right){A}$
26 23 13 recid2d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \left(\frac{1}{{A}}\right){A}=1$
27 26 negeqd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to -\left(\frac{1}{{A}}\right){A}=-1$
28 25 27 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \left(-\frac{1}{{A}}\right){A}=-1$
29 22 28 breqtrd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to 0<-1$
30 1red ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to 1\in ℝ$
31 30 lt0neg1d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to \left(1<0↔0<-1\right)$
32 29 31 mpbird ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \frac{1}{{A}}<0\right)\to 1<0$
33 32 ex ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(\frac{1}{{A}}<0\to 1<0\right)$
34 11 33 mtoi ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to ¬\frac{1}{{A}}<0$
35 ioran ${⊢}¬\left(0=\frac{1}{{A}}\vee \frac{1}{{A}}<0\right)↔\left(¬0=\frac{1}{{A}}\wedge ¬\frac{1}{{A}}<0\right)$
36 6 34 35 sylanbrc ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to ¬\left(0=\frac{1}{{A}}\vee \frac{1}{{A}}<0\right)$
37 axlttri ${⊢}\left(0\in ℝ\wedge \frac{1}{{A}}\in ℝ\right)\to \left(0<\frac{1}{{A}}↔¬\left(0=\frac{1}{{A}}\vee \frac{1}{{A}}<0\right)\right)$
38 8 17 37 sylancr ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(0<\frac{1}{{A}}↔¬\left(0=\frac{1}{{A}}\vee \frac{1}{{A}}<0\right)\right)$
39 36 38 mpbird ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<\frac{1}{{A}}$