Theorem divge1

Description: The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rpgecl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to B\in {ℝ}^{+}$$
2		rpcn	$$⊢B\in {ℝ}^{+}\to B\in ℂ$$
3		rpne0	$$⊢B\in {ℝ}^{+}\to B\ne 0$$
4	2 3	dividd	$$⊢B\in {ℝ}^{+}\to \frac{B}{B}=1$$
5	4	eqcomd	$$⊢B\in {ℝ}^{+}\to 1=\frac{B}{B}$$
6	1 5	syl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to 1=\frac{B}{B}$$
7		simp3	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to A\le B$$
8		simp1	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to A\in {ℝ}^{+}$$
9	8 1 1	lediv2d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to \left(A\le B\leftrightarrow \frac{B}{B}\le \frac{B}{A}\right)$$
10	7 9	mpbid	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to \frac{B}{B}\le \frac{B}{A}$$
11	6 10	eqbrtrd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to 1\le \frac{B}{A}$$