This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≤ 𝐵 ↔ ( 𝐴 / 𝐵 ) ≤ 𝐴 ) )