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	$$⊢\left(A\in \mathbb{N}\wedge B\in {ℝ}^{+}\right)\to \left(1\le B\leftrightarrow \frac{A}{B}\le A\right)$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		0lt1	$$⊢0<1$$
3	1 2	pm3.2i	$$⊢\left(1\in ℝ\wedge 0<1\right)$$
4		rpregt0	$$⊢B\in {ℝ}^{+}\to \left(B\in ℝ\wedge 0<B\right)$$
5	4	adantl	$$⊢\left(A\in \mathbb{N}\wedge B\in {ℝ}^{+}\right)\to \left(B\in ℝ\wedge 0<B\right)$$
6		nnre	$$⊢A\in \mathbb{N}\to A\in ℝ$$
7		nngt0	$$⊢A\in \mathbb{N}\to 0<A$$
8	6 7	jca	$$⊢A\in \mathbb{N}\to \left(A\in ℝ\wedge 0<A\right)$$
9	8	adantr	$$⊢\left(A\in \mathbb{N}\wedge B\in {ℝ}^{+}\right)\to \left(A\in ℝ\wedge 0<A\right)$$
10		lediv2	$$⊢\left(\left(1\in ℝ\wedge 0<1\right)\wedge \left(B\in ℝ\wedge 0<B\right)\wedge \left(A\in ℝ\wedge 0<A\right)\right)\to \left(1\le B\leftrightarrow \frac{A}{B}\le \frac{A}{1}\right)$$
11	3 5 9 10	mp3an2i	$$⊢\left(A\in \mathbb{N}\wedge B\in {ℝ}^{+}\right)\to \left(1\le B\leftrightarrow \frac{A}{B}\le \frac{A}{1}\right)$$
12		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
13	12	div1d	$$⊢A\in \mathbb{N}\to \frac{A}{1}=A$$
14	13	adantr	$$⊢\left(A\in \mathbb{N}\wedge B\in {ℝ}^{+}\right)\to \frac{A}{1}=A$$
15	14	breq2d	$$⊢\left(A\in \mathbb{N}\wedge B\in {ℝ}^{+}\right)\to \left(\frac{A}{B}\le \frac{A}{1}\leftrightarrow \frac{A}{B}\le A\right)$$
16	11 15	bitrd	$$⊢\left(A\in \mathbb{N}\wedge B\in {ℝ}^{+}\right)\to \left(1\le B\leftrightarrow \frac{A}{B}\le A\right)$$