Metamath Proof Explorer

Theorem peano2cnm

Description: "Reverse" second Peano postulate analogue for complex numbers: A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018)

Ref Expression
Assertion peano2cnm 
|- ( N e. CC -> ( N - 1 ) e. CC )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 subcl 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N - 1 ) e. CC )
3 1 2 mpan2 
 |-  ( N e. CC -> ( N - 1 ) e. CC )