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	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		lazval	Could not format ( S e. CC -> ( Z[]l ` S ) = { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } ) : No typesetting found for |- ( S e. CC -> ( Z[]l ` S ) = { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } ) with typecode |-
2	1	eleq2d	Could not format ( 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 ) ) } ) ) : No typesetting found for |- ( 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 ) ) } ) ) with typecode |-
3		eqeq1	$$⊢x=A\to \left(x=a+bS\leftrightarrow A=a+bS\right)$$
4	3	2rexbidv	$$⊢x=A\to \left(\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bS\leftrightarrow \exists a\in \mathbb{Z}\exists b\in \mathbb{Z}A=a+bS\right)$$
5		eqid	$$⊢\left\{x\in ℂ|\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bS\right\}=\left\{x\in ℂ|\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bS\right\}$$
6	4 5	elrab2	$$⊢A\in \left\{x\in ℂ|\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bS\right\}\leftrightarrow \left(A\in ℂ\wedge \exists a\in \mathbb{Z}\exists b\in \mathbb{Z}A=a+bS\right)$$
7	2 6	bitrdi	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 |-