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∈ℕ→AB≤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↔AB≤A
6 4 5 sylan2 ⊢A∈ℕ∧B∈ℕ→1≤B↔AB≤A
7 3 6 mpbid ⊢A∈ℕ∧B∈ℕ→AB≤A
8 7 ex ⊢A∈ℕ→B∈ℕ→AB≤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→0B=0
14 12 13 syl ⊢A=0∧B∈ℕ→0B=0
15 0le0 ⊢0≤0
16 14 15 eqbrtrdi ⊢A=0∧B∈ℕ→0B≤0
17 oveq1 ⊢A=0→AB=0B
18 id ⊢A=0→A=0
19 17 18 breq12d ⊢A=0→AB≤A↔0B≤0
20 19 adantr ⊢A=0∧B∈ℕ→AB≤A↔0B≤0
21 16 20 mpbird ⊢A=0∧B∈ℕ→AB≤A
22 21 ex ⊢A=0→B∈ℕ→AB≤A
23 8 22 jaoi ⊢A∈ℕ∨A=0→B∈ℕ→AB≤A
24 1 23 sylbi ⊢A∈ℕ0→B∈ℕ→AB≤A
25 24 imp ⊢A∈ℕ0∧B∈ℕ→AB≤A