Theorem lazcn

Description: An extended integer is a complex number. (Contributed by AV, 24-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ellaz	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )
2		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → 𝐴 ∈ ℂ )
3	1 2	biimtrdi	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → 𝐴 ∈ ℂ ) )