Theorem divlt1lt

Description: A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020)

	Ref	Expression
Assertion	divlt1lt	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(\frac{A}{B}<1\leftrightarrow A<B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\in ℝ$$
2		rpregt0	$$⊢B\in {ℝ}^{+}\to \left(B\in ℝ\wedge 0<B\right)$$
3	2	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(B\in ℝ\wedge 0<B\right)$$
4		1re	$$⊢1\in ℝ$$
5		0lt1	$$⊢0<1$$
6	4 5	pm3.2i	$$⊢\left(1\in ℝ\wedge 0<1\right)$$
7	6	a1i	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(1\in ℝ\wedge 0<1\right)$$
8		ltdiv23	$$⊢\left(A\in ℝ\wedge \left(B\in ℝ\wedge 0<B\right)\wedge \left(1\in ℝ\wedge 0<1\right)\right)\to \left(\frac{A}{B}<1\leftrightarrow \frac{A}{1}<B\right)$$
9	1 3 7 8	syl3anc	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(\frac{A}{B}<1\leftrightarrow \frac{A}{1}<B\right)$$
10		recn	$$⊢A\in ℝ\to A\in ℂ$$
11	10	div1d	$$⊢A\in ℝ\to \frac{A}{1}=A$$
12	11	adantr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{1}=A$$
13	12	breq1d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(\frac{A}{1}<B\leftrightarrow A<B\right)$$
14	9 13	bitrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(\frac{A}{B}<1\leftrightarrow A<B\right)$$