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

Step	Hyp	Ref	Expression
1		elnnne0	$⊢ L \in ℕ \leftrightarrow (L \in ℕ_{0} \land L \neq 0)$
2		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
3	2	adantr	$⊢ (K \in ℕ_{0} \land (L \in ℕ_{0} \land L \neq 0)) \to K \in ℝ$
4		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
5	4	ad2antrl	$⊢ (K \in ℕ_{0} \land (L \in ℕ_{0} \land L \neq 0)) \to L \in ℝ$
6		simprr	$⊢ (K \in ℕ_{0} \land (L \in ℕ_{0} \land L \neq 0)) \to L \neq 0$
7	3 5 6	3jca	$⊢ (K \in ℕ_{0} \land (L \in ℕ_{0} \land L \neq 0)) \to (K \in ℝ \land L \in ℝ \land L \neq 0)$
8	1 7	sylan2b	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to (K \in ℝ \land L \in ℝ \land L \neq 0)$
9		redivcl	$⊢ (K \in ℝ \land L \in ℝ \land L \neq 0) \to \frac{K}{L} \in ℝ$
10	8 9	syl	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to \frac{K}{L} \in ℝ$

Metamath Proof Explorer