Theorem lazlinz

Description: Construct an extended integer. (Contributed by AV, 25-Oct-2026)

	Ref	Expression
Assertion	lazlinz	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℂ )
3	2	adantl	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
4		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
6	5	adantl	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
7		simpl	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
8	6 7	mulcld	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐵 · 𝑆 ) ∈ ℂ )
9	3 8	addcld	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ℂ )
10		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( 𝐴 + ( 𝑏 · 𝑆 ) ) )
11	10	eqeq2d	⊢ ( 𝑎 = 𝐴 → ( ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ↔ ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝐴 + ( 𝑏 · 𝑆 ) ) ) )
12		oveq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 · 𝑆 ) = ( 𝐵 · 𝑆 ) )
13	12	oveq2d	⊢ ( 𝑏 = 𝐵 → ( 𝐴 + ( 𝑏 · 𝑆 ) ) = ( 𝐴 + ( 𝐵 · 𝑆 ) ) )
14	13	eqeq2d	⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝐴 + ( 𝑏 · 𝑆 ) ) ↔ ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝐴 + ( 𝐵 · 𝑆 ) ) ) )
15		simpl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
16	15	adantl	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
17		simprr	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
18		eqidd	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝐴 + ( 𝐵 · 𝑆 ) ) )
19	11 14 16 17 18	2rspcedvdw	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
20		ellaz	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) ↔ ( ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )
21	20	adantr	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) ↔ ( ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 + ( 𝐵 · 𝑆 ) ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )
22	9 19 21	mpbir2and	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) )
23	22	ex	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + ( 𝐵 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) ) )