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 |
|
ltdiv23 |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 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 ↔ 𝐴 < 𝐵 ) ) |