Theorem zelaz

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

	Ref	Expression
Assertion	zelaz	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ( Z[] ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		azssid	⊢ ( 𝑆 ∈ ℂ → ( ℤ ∪ { 𝑆 } ) ⊆ ( Z[] ‘ 𝑆 ) )
2	1	unssad	⊢ ( 𝑆 ∈ ℂ → ℤ ⊆ ( Z[] ‘ 𝑆 ) )
3	2	sselda	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ( Z[] ‘ 𝑆 ) )