Metamath Proof Explorer


Theorem divle1le

Description: A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
2 rpregt0 ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
3 2 adantl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
4 1re 1 ∈ ℝ
5 0lt1 0 < 1
6 4 5 pm3.2i ( 1 ∈ ℝ ∧ 0 < 1 )
7 6 a1i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 1 ∈ ℝ ∧ 0 < 1 ) )
8 lediv23 ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ ( 𝐴 / 1 ) ≤ 𝐵 ) )
9 1 3 7 8 syl3anc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ ( 𝐴 / 1 ) ≤ 𝐵 ) )
10 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
11 10 div1d ( 𝐴 ∈ ℝ → ( 𝐴 / 1 ) = 𝐴 )
12 11 adantr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 1 ) = 𝐴 )
13 12 breq1d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 1 ) ≤ 𝐵𝐴𝐵 ) )
14 9 13 bitrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ≤ 1 ↔ 𝐴𝐵 ) )