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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ≤ 𝐴 )

Proof

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