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