Description: The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | nndivre | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) ∈ ℝ ) |
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 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) ∈ ℝ ) |