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 ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A B ≤ 1 ↔ A ≤ B

Proof

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