Theorem recgt1i

Description: The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005)

	Ref	Expression
Assertion	recgt1i	$$⊢\left(A\in ℝ\wedge 1<A\right)\to \left(0<\frac{1}{A}\wedge \frac{1}{A}<1\right)$$

Proof

Step	Hyp	Ref	Expression
1		0lt1	$$⊢0<1$$
2		0re	$$⊢0\in ℝ$$
3		1re	$$⊢1\in ℝ$$
4		lttr	$$⊢\left(0\in ℝ\wedge 1\in ℝ\wedge A\in ℝ\right)\to \left(\left(0<1\wedge 1<A\right)\to 0<A\right)$$
5	2 3 4	mp3an12	$$⊢A\in ℝ\to \left(\left(0<1\wedge 1<A\right)\to 0<A\right)$$
6	1 5	mpani	$$⊢A\in ℝ\to \left(1<A\to 0<A\right)$$
7	6	imdistani	$$⊢\left(A\in ℝ\wedge 1<A\right)\to \left(A\in ℝ\wedge 0<A\right)$$
8		recgt0	$$⊢\left(A\in ℝ\wedge 0<A\right)\to 0<\frac{1}{A}$$
9	7 8	syl	$$⊢\left(A\in ℝ\wedge 1<A\right)\to 0<\frac{1}{A}$$
10		recgt1	$$⊢\left(A\in ℝ\wedge 0<A\right)\to \left(1<A\leftrightarrow \frac{1}{A}<1\right)$$
11	10	biimpa	$$⊢\left(\left(A\in ℝ\wedge 0<A\right)\wedge 1<A\right)\to \frac{1}{A}<1$$
12	7 11	sylancom	$$⊢\left(A\in ℝ\wedge 1<A\right)\to \frac{1}{A}<1$$
13	9 12	jca	$$⊢\left(A\in ℝ\wedge 1<A\right)\to \left(0<\frac{1}{A}\wedge \frac{1}{A}<1\right)$$