Theorem azcn

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

	Ref	Expression
Assertion	azcn	|- ( S e. CC -> ( A e. ( Z[] ` S ) -> A e. CC ) )

Proof

Step	Hyp	Ref	Expression
1		cnring	|- CCfld e. Ring
2	1	a1i	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> CCfld e. Ring )
3		cnfldbas	|- CC = ( Base ` CCfld )
4	3	a1i	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> CC = ( Base ` CCfld ) )
5		zsscn	|- ZZ C_ CC
6	5	a1i	|- ( S e. CC -> ZZ C_ CC )
7		snssi	|- ( S e. CC -> { S } C_ CC )
8	6 7	unssd	|- ( S e. CC -> ( ZZ u. { S } ) C_ CC )
9	8	adantr	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ZZ u. { S } ) C_ CC )
10		eqidd	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( RingSpan ` CCfld ) = ( RingSpan ` CCfld ) )
11		azval	|- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )
12	11	adantr	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )
13	2 4 9 10 12	rgspncl	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( Z[] ` S ) e. ( SubRing ` CCfld ) )
14	3	subrgss	|- ( ( Z[] ` S ) e. ( SubRing ` CCfld ) -> ( Z[] ` S ) C_ CC )
15		simpr	|- ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> ( Z[] ` S ) C_ CC )
16		simpl	|- ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> A e. ( Z[] ` S ) )
17	15 16	sseldd	|- ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> A e. CC )
18	17	ex	|- ( A e. ( Z[] ` S ) -> ( ( Z[] ` S ) C_ CC -> A e. CC ) )
19	18	adantl	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ( Z[] ` S ) C_ CC -> A e. CC ) )
20	14 19	syl5	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ( Z[] ` S ) e. ( SubRing ` CCfld ) -> A e. CC ) )
21	13 20	mpd	|- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> A e. CC )
22	21	ex	|- ( S e. CC -> ( A e. ( Z[] ` S ) -> A e. CC ) )