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\in ℝ$$
	recgt0i.2	$$⊢0<A$$
Assertion	recgt0ii	$$⊢0<\frac{1}{A}$$

Proof

Step	Hyp	Ref	Expression
1		ltplus1.1	$$⊢A\in ℝ$$
2		recgt0i.2	$$⊢0<A$$
3		ax-1cn	$$⊢1\in ℂ$$
4	1	recni	$$⊢A\in ℂ$$
5		ax-1ne0	$$⊢1\ne 0$$
6	1 2	gt0ne0ii	$$⊢A\ne 0$$
7	3 4 5 6	divne0i	$$⊢\frac{1}{A}\ne 0$$
8	7	nesymi	$$⊢\neg 0=\frac{1}{A}$$
9		0lt1	$$⊢0<1$$
10		0re	$$⊢0\in ℝ$$
11		1re	$$⊢1\in ℝ$$
12	10 11	ltnsymi	$$⊢0<1\to \neg 1<0$$
13	9 12	ax-mp	$$⊢\neg 1<0$$
14	1 6	rereccli	$$⊢\frac{1}{A}\in ℝ$$
15	14	renegcli	$$⊢-\frac{1}{A}\in ℝ$$
16	15 1	mulgt0i	$$⊢\left(0<-\frac{1}{A}\wedge 0<A\right)\to 0<\left(-\frac{1}{A}\right)A$$
17	2 16	mpan2	$$⊢0<-\frac{1}{A}\to 0<\left(-\frac{1}{A}\right)A$$
18	14	recni	$$⊢\frac{1}{A}\in ℂ$$
19	18 4	mulneg1i	$$⊢\left(-\frac{1}{A}\right)A=-\left(\frac{1}{A}\right)A$$
20	4 6	recidi	$$⊢A\left(\frac{1}{A}\right)=1$$
21	4 18 20	mulcomli	$$⊢\left(\frac{1}{A}\right)A=1$$
22	21	negeqi	$$⊢-\left(\frac{1}{A}\right)A=-1$$
23	19 22	eqtri	$$⊢\left(-\frac{1}{A}\right)A=-1$$
24	17 23	breqtrdi	$$⊢0<-\frac{1}{A}\to 0<-1$$
25		lt0neg1	$$⊢\frac{1}{A}\in ℝ\to \left(\frac{1}{A}<0\leftrightarrow 0<-\frac{1}{A}\right)$$
26	14 25	ax-mp	$$⊢\frac{1}{A}<0\leftrightarrow 0<-\frac{1}{A}$$
27		lt0neg1	$$⊢1\in ℝ\to \left(1<0\leftrightarrow 0<-1\right)$$
28	11 27	ax-mp	$$⊢1<0\leftrightarrow 0<-1$$
29	24 26 28	3imtr4i	$$⊢\frac{1}{A}<0\to 1<0$$
30	13 29	mto	$$⊢\neg \frac{1}{A}<0$$
31	8 30	pm3.2ni	$$⊢\neg \left(0=\frac{1}{A}\vee \frac{1}{A}<0\right)$$
32		axlttri	$$⊢\left(0\in ℝ\wedge \frac{1}{A}\in ℝ\right)\to \left(0<\frac{1}{A}\leftrightarrow \neg \left(0=\frac{1}{A}\vee \frac{1}{A}<0\right)\right)$$
33	10 14 32	mp2an	$$⊢0<\frac{1}{A}\leftrightarrow \neg \left(0=\frac{1}{A}\vee \frac{1}{A}<0\right)$$
34	31 33	mpbir	$$⊢0<\frac{1}{A}$$