Theorem nnledivrp

Description: Division of a positive integer by a positive number is less than or equal to the integer iff the number is greater than or equal to 1. (Contributed by AV, 19-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		1re	|- 1 e. RR
2		0lt1	|- 0 < 1
3	1 2	pm3.2i	|- ( 1 e. RR /\ 0 < 1 )
4		rpregt0	|- ( B e. RR+ -> ( B e. RR /\ 0 < B ) )
5	4	adantl	|- ( ( A e. NN /\ B e. RR+ ) -> ( B e. RR /\ 0 < B ) )
6		nnre	|- ( A e. NN -> A e. RR )
7		nngt0	|- ( A e. NN -> 0 < A )
8	6 7	jca	|- ( A e. NN -> ( A e. RR /\ 0 < A ) )
9	8	adantr	|- ( ( A e. NN /\ B e. RR+ ) -> ( A e. RR /\ 0 < A ) )
10		lediv2	|- ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( 1 <_ B <-> ( A / B ) <_ ( A / 1 ) ) )
11	3 5 9 10	mp3an2i	|- ( ( A e. NN /\ B e. RR+ ) -> ( 1 <_ B <-> ( A / B ) <_ ( A / 1 ) ) )
12		nncn	|- ( A e. NN -> A e. CC )
13	12	div1d	|- ( A e. NN -> ( A / 1 ) = A )
14	13	adantr	|- ( ( A e. NN /\ B e. RR+ ) -> ( A / 1 ) = A )
15	14	breq2d	|- ( ( A e. NN /\ B e. RR+ ) -> ( ( A / B ) <_ ( A / 1 ) <-> ( A / B ) <_ A ) )
16	11 15	bitrd	|- ( ( A e. NN /\ B e. RR+ ) -> ( 1 <_ B <-> ( A / B ) <_ A ) )