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	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ( 1 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		0lt1	⊢ 0 < 1
3	1 2	pm3.2i	⊢ ( 1 ∈ ℝ ∧ 0 < 1 )
4		rpregt0	⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
6		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
7		nngt0	⊢ ( 𝐴 ∈ ℕ → 0 < 𝐴 )
8	6 7	jca	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
10		lediv2	⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ ( 𝐴 / 1 ) ) )
11	3 5 9 10	mp3an2i	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ( 1 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ ( 𝐴 / 1 ) ) )
12		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
13	12	div1d	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 / 1 ) = 𝐴 )
14	13	adantr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 1 ) = 𝐴 )
15	14	breq2d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ≤ ( 𝐴 / 1 ) ↔ ( 𝐴 / 𝐵 ) ≤ 𝐴 ) )
16	11 15	bitrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ( 1 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ 𝐴 ) )