This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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