Theorem lazcn

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

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

Proof

Step	Hyp	Ref	Expression
1		ellaz	|- ( S e. CC -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) )
2		simpl	|- ( ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) -> A e. CC )
3	1 2	biimtrdi	|- ( S e. CC -> ( A e. ( Z[]l ` S ) -> A e. CC ) )