Theorem divge1b

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

	Ref	Expression
Assertion	divge1b	|- ( ( 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	mulid2d	|- ( A e. RR+ -> ( 1 x. A ) = A )
3	2	eqcomd	|- ( A e. RR+ -> A = ( 1 x. A ) )
4	3	adantr	|- ( ( 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		lemuldiv	|- ( ( 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 ) ) )