Metamath Proof Explorer


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