Theorem azssid

Description: The union of the integers and the adjoined complex number are a subset of the adjunction. (Contributed by AV, 31-Oct-2026)

	Ref	Expression
Assertion	azssid	Could not format assertion : No typesetting found for |- ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
2	1	a1i	$$⊢S\in ℂ\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4	3	a1i	$$⊢S\in ℂ\to ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
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		eqidd	$$⊢S\in ℂ\to \mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)$$
10		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 |-
11	2 4 8 9 10	rgspnssid	Could not format ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) ) : No typesetting found for |- ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) ) with typecode |-