Theorem lazval

Description: An adjunction of a complex number to the ring of integers. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	lazval	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢s=S\to bs=bS$$
2	1	oveq2d	$$⊢s=S\to a+bs=a+bS$$
3	2	eqeq2d	$$⊢s=S\to \left(x=a+bs\leftrightarrow x=a+bS\right)$$
4	3	2rexbidv	$$⊢s=S\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}x=a+bS\right)$$
5	4	rabbidv	$$⊢s=S\to \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		df-laz	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 |- Z[]l = ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } ) with typecode |-
7		cnex	$$⊢ℂ\in \mathrm{V}$$
8	7	rabex	$$⊢\left\{x\in ℂ|\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}x=a+bS\right\}\in \mathrm{V}$$
9	5 6 8	fvmpt	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 |-