Metamath Proof Explorer

Theorem elazim

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

Ref Expression
Assertion elazim 
|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )

Proof

Step Hyp Ref Expression
1 elaz 
 |-  ( S e. CC -> ( A e. ( Z[] ` S ) <-> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) )
2 1 biimpa 
 |-  ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )