Theorem azcn

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

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

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2	1	a1i	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ℂfld ∈ Ring )
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4	3	a1i	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ℂ = ( Base ‘ ℂfld ) )
5		zsscn	⊢ ℤ ⊆ ℂ
6	5	a1i	⊢ ( 𝑆 ∈ ℂ → ℤ ⊆ ℂ )
7		snssi	⊢ ( 𝑆 ∈ ℂ → { 𝑆 } ⊆ ℂ )
8	6 7	unssd	⊢ ( 𝑆 ∈ ℂ → ( ℤ ∪ { 𝑆 } ) ⊆ ℂ )
9	8	adantr	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ( ℤ ∪ { 𝑆 } ) ⊆ ℂ )
10		eqidd	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ( RingSpan ‘ ℂfld ) = ( RingSpan ‘ ℂfld ) )
11		azval	⊢ ( 𝑆 ∈ ℂ → ( Z[] ‘ 𝑆 ) = ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )
12	11	adantr	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ( Z[] ‘ 𝑆 ) = ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )
13	2 4 9 10 12	rgspncl	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ( Z[] ‘ 𝑆 ) ∈ ( SubRing ‘ ℂfld ) )
14	3	subrgss	⊢ ( ( Z[] ‘ 𝑆 ) ∈ ( SubRing ‘ ℂfld ) → ( Z[] ‘ 𝑆 ) ⊆ ℂ )
15		simpr	⊢ ( ( 𝐴 ∈ ( Z[] ‘ 𝑆 ) ∧ ( Z[] ‘ 𝑆 ) ⊆ ℂ ) → ( Z[] ‘ 𝑆 ) ⊆ ℂ )
16		simpl	⊢ ( ( 𝐴 ∈ ( Z[] ‘ 𝑆 ) ∧ ( Z[] ‘ 𝑆 ) ⊆ ℂ ) → 𝐴 ∈ ( Z[] ‘ 𝑆 ) )
17	15 16	sseldd	⊢ ( ( 𝐴 ∈ ( Z[] ‘ 𝑆 ) ∧ ( Z[] ‘ 𝑆 ) ⊆ ℂ ) → 𝐴 ∈ ℂ )
18	17	ex	⊢ ( 𝐴 ∈ ( Z[] ‘ 𝑆 ) → ( ( Z[] ‘ 𝑆 ) ⊆ ℂ → 𝐴 ∈ ℂ ) )
19	18	adantl	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ( ( Z[] ‘ 𝑆 ) ⊆ ℂ → 𝐴 ∈ ℂ ) )
20	14 19	syl5	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → ( ( Z[] ‘ 𝑆 ) ∈ ( SubRing ‘ ℂfld ) → 𝐴 ∈ ℂ ) )
21	13 20	mpd	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[] ‘ 𝑆 ) ) → 𝐴 ∈ ℂ )
22	21	ex	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[] ‘ 𝑆 ) → 𝐴 ∈ ℂ ) )