Metamath Proof Explorer

Theorem nn0ge0div

Description: Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion nn0ge0div ⊢ K ∈ ℕ 0 ∧ L ∈ ℕ → 0 ≤ K L

Proof

Step Hyp Ref Expression
1 nn0ge0 ⊢ K ∈ ℕ 0 → 0 ≤ K
2 1 adantr ⊢ K ∈ ℕ 0 ∧ L ∈ ℕ → 0 ≤ K
3 elnnz ⊢ L ∈ ℕ ↔ L ∈ ℤ ∧ 0 < L
4 nn0re ⊢ K ∈ ℕ 0 → K ∈ ℝ
5 4 adantr ⊢ K ∈ ℕ 0 ∧ L ∈ ℤ ∧ 0 < L → K ∈ ℝ
6 zre ⊢ L ∈ ℤ → L ∈ ℝ
7 6 ad2antrl ⊢ K ∈ ℕ 0 ∧ L ∈ ℤ ∧ 0 < L → L ∈ ℝ
8 simprr ⊢ K ∈ ℕ 0 ∧ L ∈ ℤ ∧ 0 < L → 0 < L
9 5 7 8 3jca ⊢ K ∈ ℕ 0 ∧ L ∈ ℤ ∧ 0 < L → K ∈ ℝ ∧ L ∈ ℝ ∧ 0 < L
10 3 9 sylan2b ⊢ K ∈ ℕ 0 ∧ L ∈ ℕ → K ∈ ℝ ∧ L ∈ ℝ ∧ 0 < L
11 ge0div ⊢ K ∈ ℝ ∧ L ∈ ℝ ∧ 0 < L → 0 ≤ K ↔ 0 ≤ K L
12 10 11 syl ⊢ K ∈ ℕ 0 ∧ L ∈ ℕ → 0 ≤ K ↔ 0 ≤ K L
13 2 12 mpbid ⊢ K ∈ ℕ 0 ∧ L ∈ ℕ → 0 ≤ K L