Theorem adcnmulzlaz

Description: The extended complex number multiplied with an integer is an extended integer. (Contributed by AV, 25-Oct-2026)

	Ref	Expression
Assertion	adcnmulzlaz	|- ( ( S e. CC /\ C e. ZZ ) -> ( C x. S ) e. ( Z[]l ` S ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	|- ( C e. ZZ -> C e. CC )
2	1	adantl	|- ( ( S e. CC /\ C e. ZZ ) -> C e. CC )
3		simpl	|- ( ( S e. CC /\ C e. ZZ ) -> S e. CC )
4	2 3	mulcld	|- ( ( S e. CC /\ C e. ZZ ) -> ( C x. S ) e. CC )
5		oveq1	|- ( a = 0 -> ( a + ( b x. S ) ) = ( 0 + ( b x. S ) ) )
6	5	eqeq2d	|- ( a = 0 -> ( ( C x. S ) = ( a + ( b x. S ) ) <-> ( C x. S ) = ( 0 + ( b x. S ) ) ) )
7		oveq1	|- ( b = C -> ( b x. S ) = ( C x. S ) )
8	7	oveq2d	|- ( b = C -> ( 0 + ( b x. S ) ) = ( 0 + ( C x. S ) ) )
9	8	eqeq2d	|- ( b = C -> ( ( C x. S ) = ( 0 + ( b x. S ) ) <-> ( C x. S ) = ( 0 + ( C x. S ) ) ) )
10		0zd	|- ( ( S e. CC /\ C e. ZZ ) -> 0 e. ZZ )
11		simpr	|- ( ( S e. CC /\ C e. ZZ ) -> C e. ZZ )
12	4	addlidd	|- ( ( S e. CC /\ C e. ZZ ) -> ( 0 + ( C x. S ) ) = ( C x. S ) )
13	12	eqcomd	|- ( ( S e. CC /\ C e. ZZ ) -> ( C x. S ) = ( 0 + ( C x. S ) ) )
14	6 9 10 11 13	2rspcedvdw	|- ( ( S e. CC /\ C e. ZZ ) -> E. a e. ZZ E. b e. ZZ ( C x. S ) = ( a + ( b x. S ) ) )
15		ellaz	|- ( S e. CC -> ( ( C x. S ) e. ( Z[]l ` S ) <-> ( ( C x. S ) e. CC /\ E. a e. ZZ E. b e. ZZ ( C x. S ) = ( a + ( b x. S ) ) ) ) )
16	15	adantr	|- ( ( S e. CC /\ C e. ZZ ) -> ( ( C x. S ) e. ( Z[]l ` S ) <-> ( ( C x. S ) e. CC /\ E. a e. ZZ E. b e. ZZ ( C x. S ) = ( a + ( b x. S ) ) ) ) )
17	4 14 16	mpbir2and	|- ( ( S e. CC /\ C e. ZZ ) -> ( C x. S ) e. ( Z[]l ` S ) )