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	|- ( ( A e. RR+ /\ B e. RR ) -> ( A < B <-> 1 < ( B / A ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	|- ( A e. RR+ -> A e. CC )
2	1	adantr	|- ( ( A e. RR+ /\ B e. RR ) -> A e. CC )
3	2	mulid2d	|- ( ( A e. RR+ /\ B e. RR ) -> ( 1 x. A ) = A )
4	3	eqcomd	|- ( ( A e. RR+ /\ B e. RR ) -> A = ( 1 x. A ) )
5	4	breq1d	|- ( ( A e. RR+ /\ B e. RR ) -> ( A < B <-> ( 1 x. A ) < B ) )
6		1red	|- ( ( A e. RR+ /\ B e. RR ) -> 1 e. RR )
7		simpr	|- ( ( A e. RR+ /\ B e. RR ) -> B e. RR )
8		rpregt0	|- ( A e. RR+ -> ( A e. RR /\ 0 < A ) )
9	8	adantr	|- ( ( A e. RR+ /\ B e. RR ) -> ( A e. RR /\ 0 < A ) )
10		ltmuldiv	|- ( ( 1 e. RR /\ B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( 1 x. A ) < B <-> 1 < ( B / A ) ) )
11	6 7 9 10	syl3anc	|- ( ( A e. RR+ /\ B e. RR ) -> ( ( 1 x. A ) < B <-> 1 < ( B / A ) ) )
12	5 11	bitrd	|- ( ( A e. RR+ /\ B e. RR ) -> ( A < B <-> 1 < ( B / A ) ) )