Metamath Proof Explorer


Theorem kcnktkm1cn

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 ) ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 id ( 𝐾 ∈ ℂ → 𝐾 ∈ ℂ )
2 peano2cnm ( 𝐾 ∈ ℂ → ( 𝐾 − 1 ) ∈ ℂ )
3 1 2 mulcld ( 𝐾 ∈ ℂ → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ )