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	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to 1 \leq \frac{B}{A}$

Step	Hyp	Ref	Expression
1		rpgecl	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to B \in ℝ^{+}$
2		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
3		rpne0	$⊢ B \in ℝ^{+} \to B \neq 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	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to 1 = \frac{B}{B}$
7		simp3	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to A \leq B$
8		simp1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to A \in ℝ^{+}$
9	8 1 1	lediv2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to (A \leq B \leftrightarrow \frac{B}{B} \leq \frac{B}{A})$
10	7 9	mpbid	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to \frac{B}{B} \leq \frac{B}{A}$
11	6 10	eqbrtrd	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to 1 \leq \frac{B}{A}$

Metamath Proof Explorer