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