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 \in ℕ_{0} \land L \in ℕ) \to 0 \leq \frac{K}{L}$

Step	Hyp	Ref	Expression
1		nn0ge0	$⊢ K \in ℕ_{0} \to 0 \leq K$
2	1	adantr	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to 0 \leq K$
3		elnnz	$⊢ L \in ℕ \leftrightarrow (L \in ℤ \land 0 < L)$
4		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
5	4	adantr	$⊢ (K \in ℕ_{0} \land (L \in ℤ \land 0 < L)) \to K \in ℝ$
6		zre	$⊢ L \in ℤ \to L \in ℝ$
7	6	ad2antrl	$⊢ (K \in ℕ_{0} \land (L \in ℤ \land 0 < L)) \to L \in ℝ$
8		simprr	$⊢ (K \in ℕ_{0} \land (L \in ℤ \land 0 < L)) \to 0 < L$
9	5 7 8	3jca	$⊢ (K \in ℕ_{0} \land (L \in ℤ \land 0 < L)) \to (K \in ℝ \land L \in ℝ \land 0 < L)$
10	3 9	sylan2b	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to (K \in ℝ \land L \in ℝ \land 0 < L)$
11		ge0div	$⊢ (K \in ℝ \land L \in ℝ \land 0 < L) \to (0 \leq K \leftrightarrow 0 \leq \frac{K}{L})$
12	10 11	syl	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to (0 \leq K \leftrightarrow 0 \leq \frac{K}{L})$
13	2 12	mpbid	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to 0 \leq \frac{K}{L}$

Metamath Proof Explorer