Theorem elazim

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

	Ref	Expression
Assertion	elazim	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → 𝐴 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		elaz	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[] ‘ 𝑆 ) ↔ 𝐴 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) ) )
2	1	biimpa	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → 𝐴 ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )