Theorem laznegcl

Description: The extended integers are closed under negation. (Contributed by AV, 25-Oct-2026)

	Ref	Expression
Hypothesis	laznegcl.r	⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
Assertion	laznegcl	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ 𝑅 → - 𝐴 ∈ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		laznegcl.r	⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
2	1	eleq2i	⊢ ( 𝐴 ∈ 𝑅 ↔ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) )
3		ellazim	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
4		negeq	⊢ ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → - 𝐴 = - ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
5		zcn	⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
6	5	adantr	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℂ )
7	6	adantl	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
8		zcn	⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
9	8	adantl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℂ )
10		simpl	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) → 𝑆 ∈ ℂ )
11		mulcl	⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 𝑏 · 𝑆 ) ∈ ℂ )
12	9 10 11	syl2anr	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · 𝑆 ) ∈ ℂ )
13	7 12	negdid	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → - ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( - 𝑎 + - ( 𝑏 · 𝑆 ) ) )
14	9	adantl	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
15	10	adantr	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
16	14 15	mulneg1d	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( - 𝑏 · 𝑆 ) = - ( 𝑏 · 𝑆 ) )
17	16	eqcomd	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → - ( 𝑏 · 𝑆 ) = ( - 𝑏 · 𝑆 ) )
18	17	oveq2d	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( - 𝑎 + - ( 𝑏 · 𝑆 ) ) = ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) )
19	13 18	eqtrd	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → - ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) )
20	4 19	sylan9eqr	⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → - 𝐴 = ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) )
21		znegcl	⊢ ( 𝑎 ∈ ℤ → - 𝑎 ∈ ℤ )
22		znegcl	⊢ ( 𝑏 ∈ ℤ → - 𝑏 ∈ ℤ )
23	21 22	anim12i	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( - 𝑎 ∈ ℤ ∧ - 𝑏 ∈ ℤ ) )
24		lazlinz	⊢ ( 𝑆 ∈ ℂ → ( ( - 𝑎 ∈ ℤ ∧ - 𝑏 ∈ ℤ ) → ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) ) )
25	24	imp	⊢ ( ( 𝑆 ∈ ℂ ∧ ( - 𝑎 ∈ ℤ ∧ - 𝑏 ∈ ℤ ) ) → ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) )
26	10 23 25	syl2an	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) ∈ ( Z[]l ‘ 𝑆 ) )
27	26 1	eleqtrrdi	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) ∈ 𝑅 )
28	27	adantr	⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → ( - 𝑎 + ( - 𝑏 · 𝑆 ) ) ∈ 𝑅 )
29	20 28	eqeltrd	⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → - 𝐴 ∈ 𝑅 )
30	29	ex	⊢ ( ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → - 𝐴 ∈ 𝑅 ) )
31	30	rexlimdvva	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → - 𝐴 ∈ 𝑅 ) )
32	3 31	mpd	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) → - 𝐴 ∈ 𝑅 )
33	32	ex	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → - 𝐴 ∈ 𝑅 ) )
34	2 33	biimtrid	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ 𝑅 → - 𝐴 ∈ 𝑅 ) )