Theorem nn0nndivcl

Description: Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018)

	Ref	Expression
Assertion	nn0nndivcl	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to \frac{K}{L}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		elnnne0	$$⊢L\in \mathbb{N}\leftrightarrow \left(L\in {\mathbb{N}}_0\wedge L\ne 0\right)$$
2		nn0re	$$⊢K\in {\mathbb{N}}_0\to K\in ℝ$$
3	2	adantr	$$⊢\left(K\in {\mathbb{N}}_0\wedge \left(L\in {\mathbb{N}}_0\wedge L\ne 0\right)\right)\to K\in ℝ$$
4		nn0re	$$⊢L\in {\mathbb{N}}_0\to L\in ℝ$$
5	4	ad2antrl	$$⊢\left(K\in {\mathbb{N}}_0\wedge \left(L\in {\mathbb{N}}_0\wedge L\ne 0\right)\right)\to L\in ℝ$$
6		simprr	$$⊢\left(K\in {\mathbb{N}}_0\wedge \left(L\in {\mathbb{N}}_0\wedge L\ne 0\right)\right)\to L\ne 0$$
7	3 5 6	3jca	$$⊢\left(K\in {\mathbb{N}}_0\wedge \left(L\in {\mathbb{N}}_0\wedge L\ne 0\right)\right)\to \left(K\in ℝ\wedge L\in ℝ\wedge L\ne 0\right)$$
8	1 7	sylan2b	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to \left(K\in ℝ\wedge L\in ℝ\wedge L\ne 0\right)$$
9		redivcl	$$⊢\left(K\in ℝ\wedge L\in ℝ\wedge L\ne 0\right)\to \frac{K}{L}\in ℝ$$
10	8 9	syl	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to \frac{K}{L}\in ℝ$$