Theorem adcnelaz

Description: The adjoined complex number is an extended integer. (Contributed by AV, 31-Oct-2026)

	Ref	Expression
Assertion	adcnelaz	⊢ ( 𝑆 ∈ ℂ → 𝑆 ∈ ( Z[] ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		azssid	⊢ ( 𝑆 ∈ ℂ → ( ℤ ∪ { 𝑆 } ) ⊆ ( Z[] ‘ 𝑆 ) )
2		snidg	⊢ ( 𝑆 ∈ ℂ → 𝑆 ∈ { 𝑆 } )
3	2	olcd	⊢ ( 𝑆 ∈ ℂ → ( 𝑆 ∈ ℤ ∨ 𝑆 ∈ { 𝑆 } ) )
4		elun	⊢ ( 𝑆 ∈ ( ℤ ∪ { 𝑆 } ) ↔ ( 𝑆 ∈ ℤ ∨ 𝑆 ∈ { 𝑆 } ) )
5	3 4	sylibr	⊢ ( 𝑆 ∈ ℂ → 𝑆 ∈ ( ℤ ∪ { 𝑆 } ) )
6	1 5	sseldd	⊢ ( 𝑆 ∈ ℂ → 𝑆 ∈ ( Z[] ‘ 𝑆 ) )