This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↔ 𝐴 ≤ 𝐵 ) )