Theorem lazcn

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

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

Proof

Step	Hyp	Ref	Expression
1		ellaz	Could not format ( S e. CC -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) ) with typecode |-
2		simpl	$$⊢\left(A\in ℂ\wedge \exists a\in \mathbb{Z}\exists b\in \mathbb{Z}A=a+bS\right)\to A\in ℂ$$
3	1 2	biimtrdi	Could not format ( S e. CC -> ( A e. ( Z[]l ` S ) -> A e. CC ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[]l ` S ) -> A e. CC ) ) with typecode |-