Theorem adcnellaz

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

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

Proof

Step	Hyp	Ref	Expression
1		mullid	$$⊢S\in ℂ\to 1S=S$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		adcnmulzlaz	Could not format ( ( S e. CC /\ 1 e. ZZ ) -> ( 1 x. S ) e. ( Z[]l ` S ) ) : No typesetting found for |- ( ( S e. CC /\ 1 e. ZZ ) -> ( 1 x. S ) e. ( Z[]l ` S ) ) with typecode |-
4	2 3	mpan2	Could not format ( S e. CC -> ( 1 x. S ) e. ( Z[]l ` S ) ) : No typesetting found for |- ( S e. CC -> ( 1 x. S ) e. ( Z[]l ` S ) ) with typecode |-
5	1 4	eqeltrrd	Could not format ( S e. CC -> S e. ( Z[]l ` S ) ) : No typesetting found for |- ( S e. CC -> S e. ( Z[]l ` S ) ) with typecode |-