Theorem ellaz

Description: Elementhood in an adjunction of a complex number to the ring of integers. Such an element is also called "extended integer" in the following. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	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 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lazval	|- ( S e. CC -> ( Z[]l ` S ) = { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } )
2	1	eleq2d	|- ( S e. CC -> ( A e. ( Z[]l ` S ) <-> A e. { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } ) )
3		eqeq1	|- ( x = A -> ( x = ( a + ( b x. S ) ) <-> A = ( a + ( b x. S ) ) ) )
4	3	2rexbidv	|- ( x = A -> ( E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) <-> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
5		eqid	|- { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } = { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) }
6	4 5	elrab2	|- ( A e. { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
7	2 6	bitrdi	|- ( S e. CC -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) )