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	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → ( 𝐶 · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
2	1	adantl	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
3		simpl	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → 𝑆 ∈ ℂ )
4	2 3	mulcld	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → ( 𝐶 · 𝑆 ) ∈ ℂ )
5		oveq1	⊢ ( 𝑎 = 0 → ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( 0 + ( 𝑏 · 𝑆 ) ) )
6	5	eqeq2d	⊢ ( 𝑎 = 0 → ( ( 𝐶 · 𝑆 ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ↔ ( 𝐶 · 𝑆 ) = ( 0 + ( 𝑏 · 𝑆 ) ) ) )
7		oveq1	⊢ ( 𝑏 = 𝐶 → ( 𝑏 · 𝑆 ) = ( 𝐶 · 𝑆 ) )
8	7	oveq2d	⊢ ( 𝑏 = 𝐶 → ( 0 + ( 𝑏 · 𝑆 ) ) = ( 0 + ( 𝐶 · 𝑆 ) ) )
9	8	eqeq2d	⊢ ( 𝑏 = 𝐶 → ( ( 𝐶 · 𝑆 ) = ( 0 + ( 𝑏 · 𝑆 ) ) ↔ ( 𝐶 · 𝑆 ) = ( 0 + ( 𝐶 · 𝑆 ) ) ) )
10		0zd	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → 0 ∈ ℤ )
11		simpr	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℤ )
12	4	addlidd	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → ( 0 + ( 𝐶 · 𝑆 ) ) = ( 𝐶 · 𝑆 ) )
13	12	eqcomd	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → ( 𝐶 · 𝑆 ) = ( 0 + ( 𝐶 · 𝑆 ) ) )
14	6 9 10 11 13	2rspcedvdw	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐶 · 𝑆 ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
15		ellaz	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐶 · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) ↔ ( ( 𝐶 · 𝑆 ) ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐶 · 𝑆 ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )
16	15	adantr	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐶 · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) ↔ ( ( 𝐶 · 𝑆 ) ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐶 · 𝑆 ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )
17	4 14 16	mpbir2and	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐶 ∈ ℤ ) → ( 𝐶 · 𝑆 ) ∈ ( Z[]l ‘ 𝑆 ) )