Description: Elementhood in an adjunction of a complex number to the ring of integers. Such an element is called "extended integer" in the following. (Contributed by AV, 30-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elaz | |- ( S e. CC -> ( A e. ( Z[] ` S ) <-> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | azval | |- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) |
|
| 2 | 1 | eleq2d | |- ( S e. CC -> ( A e. ( Z[] ` S ) <-> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) |