Description: k times k minus 1 is a complex number if k is a complex number. (Contributed by Alexander van der Vekens, 11-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | kcnktkm1cn | ⊢ ( 𝐾 ∈ ℂ → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | ⊢ ( 𝐾 ∈ ℂ → 𝐾 ∈ ℂ ) | |
2 | peano2cnm | ⊢ ( 𝐾 ∈ ℂ → ( 𝐾 − 1 ) ∈ ℂ ) | |
3 | 1 2 | mulcld | ⊢ ( 𝐾 ∈ ℂ → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) |