Metamath Proof Explorer


Theorem nndivre

Description: The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008)

Ref Expression
Assertion nndivre ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
2 nnne0 ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
3 1 2 jca ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ 𝑁 ≠ 0 ) )
4 redivcl ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ≠ 0 ) → ( 𝐴 / 𝑁 ) ∈ ℝ )
5 4 3expb ( ( 𝐴 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 / 𝑁 ) ∈ ℝ )
6 3 5 sylan2 ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) ∈ ℝ )