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

Proof

Step	Hyp	Ref	Expression
1		elnnne0	⊢ ( 𝐿 ∈ ℕ ↔ ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≠ 0 ) )
2		nn0re	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
3	2	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≠ 0 ) ) → 𝐾 ∈ ℝ )
4		nn0re	⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
5	4	ad2antrl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≠ 0 ) ) → 𝐿 ∈ ℝ )
6		simprr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≠ 0 ) ) → 𝐿 ≠ 0 )
7	3 5 6	3jca	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ 𝐿 ≠ 0 ) ) → ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝐿 ≠ 0 ) )
8	1 7	sylan2b	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝐿 ≠ 0 ) )
9		redivcl	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝐿 ≠ 0 ) → ( 𝐾 / 𝐿 ) ∈ ℝ )
10	8 9	syl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 / 𝐿 ) ∈ ℝ )