Theorem azcn

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

	Ref	Expression
Assertion	azcn	Could not format assertion : No typesetting found for |- ( S e. CC -> ( A e. ( Z[] ` S ) -> A e. CC ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2	1	a1i	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> CCfld e. Ring ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> CCfld e. Ring ) with typecode |-
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4	3	a1i	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> CC = ( Base ` CCfld ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> CC = ( Base ` CCfld ) ) with typecode |-
5		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
6	5	a1i	$$⊢S\in ℂ\to \mathbb{Z}\subseteq ℂ$$
7		snssi	$$⊢S\in ℂ\to \left\{S\right\}\subseteq ℂ$$
8	6 7	unssd	$$⊢S\in ℂ\to \mathbb{Z}\cup \left\{S\right\}\subseteq ℂ$$
9	8	adantr	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ZZ u. { S } ) C_ CC ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ZZ u. { S } ) C_ CC ) with typecode |-
10		eqidd	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( RingSpan ` CCfld ) = ( RingSpan ` CCfld ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( RingSpan ` CCfld ) = ( RingSpan ` CCfld ) ) with typecode |-
11		azval	Could not format ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) : No typesetting found for |- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) with typecode |-
12	11	adantr	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) with typecode |-
13	2 4 9 10 12	rgspncl	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( Z[] ` S ) e. ( SubRing ` CCfld ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( Z[] ` S ) e. ( SubRing ` CCfld ) ) with typecode |-
14	3	subrgss	Could not format ( ( Z[] ` S ) e. ( SubRing ` CCfld ) -> ( Z[] ` S ) C_ CC ) : No typesetting found for |- ( ( Z[] ` S ) e. ( SubRing ` CCfld ) -> ( Z[] ` S ) C_ CC ) with typecode |-
15		simpr	Could not format ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> ( Z[] ` S ) C_ CC ) : No typesetting found for |- ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> ( Z[] ` S ) C_ CC ) with typecode |-
16		simpl	Could not format ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> A e. ( Z[] ` S ) ) : No typesetting found for |- ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> A e. ( Z[] ` S ) ) with typecode |-
17	15 16	sseldd	Could not format ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> A e. CC ) : No typesetting found for |- ( ( A e. ( Z[] ` S ) /\ ( Z[] ` S ) C_ CC ) -> A e. CC ) with typecode |-
18	17	ex	Could not format ( A e. ( Z[] ` S ) -> ( ( Z[] ` S ) C_ CC -> A e. CC ) ) : No typesetting found for |- ( A e. ( Z[] ` S ) -> ( ( Z[] ` S ) C_ CC -> A e. CC ) ) with typecode |-
19	18	adantl	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ( Z[] ` S ) C_ CC -> A e. CC ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ( Z[] ` S ) C_ CC -> A e. CC ) ) with typecode |-
20	14 19	syl5	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ( Z[] ` S ) e. ( SubRing ` CCfld ) -> A e. CC ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> ( ( Z[] ` S ) e. ( SubRing ` CCfld ) -> A e. CC ) ) with typecode |-
21	13 20	mpd	Could not format ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> A e. CC ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[] ` S ) ) -> A e. CC ) with typecode |-
22	21	ex	Could not format ( S e. CC -> ( A e. ( Z[] ` S ) -> A e. CC ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[] ` S ) -> A e. CC ) ) with typecode |-