Theorem reclt1

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

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

Proof

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