Theorem elaz

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	Could not format assertion : No typesetting found for |- ( S e. CC -> ( A e. ( Z[] ` S ) <-> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		azval	Could not format ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) : No typesetting found for |- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) with typecode |-
2	1	eleq2d	Could not format ( S e. CC -> ( A e. ( Z[] ` S ) <-> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[] ` S ) <-> A e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) with typecode |-