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	$$⊢K\in ℂ\to K\left(K-1\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢K\in ℂ\to K\in ℂ$$
2		peano2cnm	$$⊢K\in ℂ\to K-1\in ℂ$$
3	1 2	mulcld	$$⊢K\in ℂ\to K\left(K-1\right)\in ℂ$$