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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 1 ≤ ( 𝐵 / 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rpgecl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ+ )
2		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
3		rpne0	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
4	2 3	dividd	⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 / 𝐵 ) = 1 )
5	4	eqcomd	⊢ ( 𝐵 ∈ ℝ+ → 1 = ( 𝐵 / 𝐵 ) )
6	1 5	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 1 = ( 𝐵 / 𝐵 ) )
7		simp3	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
8		simp1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ+ )
9	8 1 1	lediv2d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐵 / 𝐵 ) ≤ ( 𝐵 / 𝐴 ) ) )
10	7 9	mpbid	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 / 𝐵 ) ≤ ( 𝐵 / 𝐴 ) )
11	6 10	eqbrtrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 1 ≤ ( 𝐵 / 𝐴 ) )