Definition df-laz

Description: Define the mapping yielding the adjunctions of a complex number to the ring of integers. Analogous to df-gz . (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	df-laz	Could not format assertion : No typesetting found for |- Z[]l = ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		claz	Could not format Z[]l : No typesetting found for class Z[]l with typecode class
1		vs	$$setvars$$
2		cc	$$classℂ$$
3		vx	$$setvarx$$
4		va	$$setvara$$
5		cz	$$class\mathbb{Z}$$
6		vb	$$setvarb$$
7	3	cv	$$setvarx$$
8	4	cv	$$setvara$$
9		caddc	$$class+$$
10	6	cv	$$setvarb$$
11		cmul	$$class\times$$
12	1	cv	$$setvars$$
13	10 12 11	co	$$classbs$$
14	8 13 9	co	$$class\left(a+bs\right)$$
15	7 14	wceq	$$wffx=a+bs$$
16	15 6 5	wrex	$$wff\exists b\in \mathbb{Z}x=a+bs$$
17	16 4 5	wrex	$$wff\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bs$$
18	17 3 2	crab	$$class\left\{x\in ℂ|\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bs\right\}$$
19	1 2 18	cmpt	$$class\left(s\in ℂ⟼\left\{x\in ℂ|\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bs\right\}\right)$$
20	0 19	wceq	Could not format Z[]l = ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } ) : No typesetting found for wff Z[]l = ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } ) with typecode wff