Theorem divge1b

Description: The ratio of a real number to a positive real number is greater than or equal to 1 iff the divisor (the positive real number) is less than or equal to the dividend (the real number). (Contributed by AV, 26-May-2020)

	Ref	Expression
Assertion	divge1b	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ 1 ≤ ( 𝐵 / 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
2	1	mullidd	⊢ ( 𝐴 ∈ ℝ+ → ( 1 · 𝐴 ) = 𝐴 )
3	2	eqcomd	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 = ( 1 · 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐴 = ( 1 · 𝐴 ) )
5	4	breq1d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 1 · 𝐴 ) ≤ 𝐵 ) )
6		1red	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 1 ∈ ℝ )
7		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
8		rpregt0	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
10		lemuldiv	⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 1 · 𝐴 ) ≤ 𝐵 ↔ 1 ≤ ( 𝐵 / 𝐴 ) ) )
11	6 7 9 10	syl3anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( ( 1 · 𝐴 ) ≤ 𝐵 ↔ 1 ≤ ( 𝐵 / 𝐴 ) ) )
12	5 11	bitrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ 1 ≤ ( 𝐵 / 𝐴 ) ) )