Theorem adcnellaz

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

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

Proof

Step	Hyp	Ref	Expression
1		mullid	⊢ ( 𝑆 ∈ ℂ → ( 1 · 𝑆 ) = 𝑆 )
2		1z	⊢ 1 ∈ ℤ
3		adcnmulzlaz	⊢ ( ( 𝑆 ∈ ℂ ∧ 1 ∈ ℤ ) → ( 1 · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) )
4	2 3	mpan2	⊢ ( 𝑆 ∈ ℂ → ( 1 · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) )
5	1 4	eqeltrrd	⊢ ( 𝑆 ∈ ℂ → 𝑆 ∈ ( Z[]l ‘ 𝑆 ) )