Metamath Proof Explorer

Theorem zelaz

Description: An integer is an extended integer. (Contributed by AV, 31-Oct-2026)

Ref Expression
Assertion zelaz 
|- ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[] ` S ) )

Proof

Step Hyp Ref Expression
1 azssid 
 |-  ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) )
2 1 unssad 
 |-  ( S e. CC -> ZZ C_ ( Z[] ` S ) )
3 2 sselda 
 |-  ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[] ` S ) )