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

Metamath Proof Explorer

Theorem divlt1lt

Description: A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion divlt1lt ⊢ 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 ltdiv23 ⊢ 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