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 ⊢ A ∈ ℕ ∧ B ∈ ℝ + → 1 ≤ B ↔ A B ≤ A

Proof

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