Metamath Proof Explorer

Theorem adcnelaz

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

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

Proof

Step Hyp Ref Expression
1 azssid 
 |-  ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) )
2 snidg 
 |-  ( S e. CC -> S e. { S } )
3 2 olcd 
 |-  ( S e. CC -> ( S e. ZZ \/ S e. { S } ) )
4 elun 
 |-  ( S e. ( ZZ u. { S } ) <-> ( S e. ZZ \/ S e. { S } ) )
5 3 4 sylibr 
 |-  ( S e. CC -> S e. ( ZZ u. { S } ) )
6 1 5 sseldd 
 |-  ( S e. CC -> S e. ( Z[] ` S ) )