Theorem recgt1

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

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

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		0lt1	$$⊢0<1$$
3		ltrec	$$⊢\left(\left(1\in ℝ\wedge 0<1\right)\wedge \left(A\in ℝ\wedge 0<A\right)\right)\to \left(1<A\leftrightarrow \frac{1}{A}<\frac{1}{1}\right)$$
4	1 2 3	mpanl12	$$⊢\left(A\in ℝ\wedge 0<A\right)\to \left(1<A\leftrightarrow \frac{1}{A}<\frac{1}{1}\right)$$
5		1div1e1	$$⊢\frac{1}{1}=1$$
6	5	breq2i	$$⊢\frac{1}{A}<\frac{1}{1}\leftrightarrow \frac{1}{A}<1$$
7	4 6	bitrdi	$$⊢\left(A\in ℝ\wedge 0<A\right)\to \left(1<A\leftrightarrow \frac{1}{A}<1\right)$$