Theorem ltdivgt1

Description: Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	ltdivgt1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	ltdivgt1.2	$$⊢\phi \to B\in {ℝ}^{+}$$
Assertion	ltdivgt1	$$⊢\phi \to \left(1<B\leftrightarrow \frac{A}{B}<A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltdivgt1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		ltdivgt1.2	$$⊢\phi \to B\in {ℝ}^{+}$$
3		1rp	$$⊢1\in {ℝ}^{+}$$
4	3	a1i	$$⊢\phi \to 1\in {ℝ}^{+}$$
5	4 2 1	ltdiv2d	$$⊢\phi \to \left(1<B\leftrightarrow \frac{A}{B}<\frac{A}{1}\right)$$
6	1	rpcnd	$$⊢\phi \to A\in ℂ$$
7	6	div1d	$$⊢\phi \to \frac{A}{1}=A$$
8	7	breq2d	$$⊢\phi \to \left(\frac{A}{B}<\frac{A}{1}\leftrightarrow \frac{A}{B}<A\right)$$
9	5 8	bitrd	$$⊢\phi \to \left(1<B\leftrightarrow \frac{A}{B}<A\right)$$