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	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → 0 ≤ ( 𝐾 / 𝐿 ) )

Proof

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