Metamath Proof Explorer

Theorem adcnellaz

Description: The adjoined complex number is an extended integer. (Contributed by AV, 25-Oct-2026)

Ref Expression
Assertion adcnellaz 
|- ( S e. CC -> S e. ( Z[]l ` S ) )

Proof

Step Hyp Ref Expression
1 mullid 
 |-  ( S e. CC -> ( 1 x. S ) = S )
2 1z 
 |-  1 e. ZZ
3 adcnmulzlaz 
 |-  ( ( S e. CC /\ 1 e. ZZ ) -> ( 1 x. S ) e. ( Z[]l ` S ) )
4 2 3 mpan2 
 |-  ( S e. CC -> ( 1 x. S ) e. ( Z[]l ` S ) )
5 1 4 eqeltrrd 
 |-  ( S e. CC -> S e. ( Z[]l ` S ) )