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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) ∈ ℝ )