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 
|- ( K e. CC -> ( K x. ( K - 1 ) ) e. CC )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( K e. CC -> K e. CC )
2 peano2cnm 
 |-  ( K e. CC -> ( K - 1 ) e. CC )
3 1 2 mulcld 
 |-  ( K e. CC -> ( K x. ( K - 1 ) ) e. CC )