Theorem zellaz

Description: An integer is an extended integer. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	zellaz	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ( Z[]l ‘ 𝑆 ) )

Proof

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