Theorem divgt1b

Description: The ratio of a real number to a positive real number is greater than 1 iff the divisor (the positive real number) is less than the dividend (the real number). (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	divgt1b	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 1 < ( 𝐵 / 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
3	2	mullidd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 1 · 𝐴 ) = 𝐴 )
4	3	eqcomd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐴 = ( 1 · 𝐴 ) )
5	4	breq1d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 1 · 𝐴 ) < 𝐵 ) )
6		1red	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 1 ∈ ℝ )
7		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
8		rpregt0	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
10		ltmuldiv	⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 1 · 𝐴 ) < 𝐵 ↔ 1 < ( 𝐵 / 𝐴 ) ) )
11	6 7 9 10	syl3anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( ( 1 · 𝐴 ) < 𝐵 ↔ 1 < ( 𝐵 / 𝐴 ) ) )
12	5 11	bitrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 1 < ( 𝐵 / 𝐴 ) ) )