Metamath Proof Explorer

Theorem nn0ledivnn

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

Ref Expression
Assertion nn0ledivnn ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ → A B ≤ A

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ A ∈ ℕ 0 ↔ A ∈ ℕ ∨ A = 0
2 nnge1 ⊢ B ∈ ℕ → 1 ≤ B
3 2 adantl ⊢ A ∈ ℕ ∧ B ∈ ℕ → 1 ≤ B
4 nnrp ⊢ B ∈ ℕ → B ∈ ℝ +
5 nnledivrp ⊢ A ∈ ℕ ∧ B ∈ ℝ + → 1 ≤ B ↔ A B ≤ A
6 4 5 sylan2 ⊢ A ∈ ℕ ∧ B ∈ ℕ → 1 ≤ B ↔ A B ≤ A
7 3 6 mpbid ⊢ A ∈ ℕ ∧ B ∈ ℕ → A B ≤ A
8 7 ex ⊢ A ∈ ℕ → B ∈ ℕ → A B ≤ A
9 nncn ⊢ B ∈ ℕ → B ∈ ℂ
10 nnne0 ⊢ B ∈ ℕ → B ≠ 0
11 9 10 jca ⊢ B ∈ ℕ → B ∈ ℂ ∧ B ≠ 0
12 11 adantl ⊢ A = 0 ∧ B ∈ ℕ → B ∈ ℂ ∧ B ≠ 0
13 div0 ⊢ B ∈ ℂ ∧ B ≠ 0 → 0 B = 0
14 12 13 syl ⊢ A = 0 ∧ B ∈ ℕ → 0 B = 0
15 0le0 ⊢ 0 ≤ 0
16 14 15 eqbrtrdi ⊢ A = 0 ∧ B ∈ ℕ → 0 B ≤ 0
17 oveq1 ⊢ A = 0 → A B = 0 B
18 id ⊢ A = 0 → A = 0
19 17 18 breq12d ⊢ A = 0 → A B ≤ A ↔ 0 B ≤ 0
20 19 adantr ⊢ A = 0 ∧ B ∈ ℕ → A B ≤ A ↔ 0 B ≤ 0
21 16 20 mpbird ⊢ A = 0 ∧ B ∈ ℕ → A B ≤ A
22 21 ex ⊢ A = 0 → B ∈ ℕ → A B ≤ A
23 8 22 jaoi ⊢ A ∈ ℕ ∨ A = 0 → B ∈ ℕ → A B ≤ A
24 1 23 sylbi ⊢ A ∈ ℕ 0 → B ∈ ℕ → A B ≤ A
25 24 imp ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ → A B ≤ A