Theorem divle1le

Description: A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021)

	Ref	Expression
Assertion	divle1le	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) <_ 1 <-> A <_ B ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. RR /\ B e. RR+ ) -> A e. RR )
2		rpregt0	|- ( B e. RR+ -> ( B e. RR /\ 0 < B ) )
3	2	adantl	|- ( ( A e. RR /\ B e. RR+ ) -> ( B e. RR /\ 0 < B ) )
4		1re	|- 1 e. RR
5		0lt1	|- 0 < 1
6	4 5	pm3.2i	|- ( 1 e. RR /\ 0 < 1 )
7	6	a1i	|- ( ( A e. RR /\ B e. RR+ ) -> ( 1 e. RR /\ 0 < 1 ) )
8		lediv23	|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( 1 e. RR /\ 0 < 1 ) ) -> ( ( A / B ) <_ 1 <-> ( A / 1 ) <_ B ) )
9	1 3 7 8	syl3anc	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) <_ 1 <-> ( A / 1 ) <_ B ) )
10		recn	|- ( A e. RR -> A e. CC )
11	10	div1d	|- ( A e. RR -> ( A / 1 ) = A )
12	11	adantr	|- ( ( A e. RR /\ B e. RR+ ) -> ( A / 1 ) = A )
13	12	breq1d	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / 1 ) <_ B <-> A <_ B ) )
14	9 13	bitrd	|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) <_ 1 <-> A <_ B ) )