Theorem adcnelaz

Description: The adjoined complex number is an extended integer. (Contributed by AV, 31-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		azssid	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 |-
2		snidg	$$⊢S\in ℂ\to S\in \left\{S\right\}$$
3	2	olcd	$$⊢S\in ℂ\to \left(S\in \mathbb{Z}\vee S\in \left\{S\right\}\right)$$
4		elun	$$⊢S\in \left(\mathbb{Z}\cup \left\{S\right\}\right)\leftrightarrow \left(S\in \mathbb{Z}\vee S\in \left\{S\right\}\right)$$
5	3 4	sylibr	$$⊢S\in ℂ\to S\in \left(\mathbb{Z}\cup \left\{S\right\}\right)$$
6	1 5	sseldd	Could not format ( S e. CC -> S e. ( Z[] ` S ) ) : No typesetting found for |- ( S e. CC -> S e. ( Z[] ` S ) ) with typecode |-