Theorem lazsubcl

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

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

Proof

Step	Hyp	Ref	Expression
1		laznegcl.r	⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
2	1	eleq2i	⊢ ( 𝐴 ∈ 𝑅 ↔ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) )
3		lazcn	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → 𝐴 ∈ ℂ ) )
4	3	a1dd	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → ( 𝐵 ∈ 𝑅 → 𝐴 ∈ ℂ ) ) )
5	2 4	biimtrid	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ 𝑅 → ( 𝐵 ∈ 𝑅 → 𝐴 ∈ ℂ ) ) )
6	5	imp32	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ) → 𝐴 ∈ ℂ )
7	1	eleq2i	⊢ ( 𝐵 ∈ 𝑅 ↔ 𝐵 ∈ ( Z[]l ‘ 𝑆 ) )
8		lazcn	⊢ ( 𝑆 ∈ ℂ → ( 𝐵 ∈ ( Z[]l ‘ 𝑆 ) → 𝐵 ∈ ℂ ) )
9	7 8	biimtrid	⊢ ( 𝑆 ∈ ℂ → ( 𝐵 ∈ 𝑅 → 𝐵 ∈ ℂ ) )
10	9	adantld	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → 𝐵 ∈ ℂ ) )
11	10	imp	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ) → 𝐵 ∈ ℂ )
12	6 11	negsubd	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
13	1	laznegcl	⊢ ( 𝑆 ∈ ℂ → ( 𝐵 ∈ 𝑅 → - 𝐵 ∈ 𝑅 ) )
14	13	anim2d	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → ( 𝐴 ∈ 𝑅 ∧ - 𝐵 ∈ 𝑅 ) ) )
15	14	imp	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ) → ( 𝐴 ∈ 𝑅 ∧ - 𝐵 ∈ 𝑅 ) )
16	1	lazaddcl	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ 𝑅 ∧ - 𝐵 ∈ 𝑅 ) → ( 𝐴 + - 𝐵 ) ∈ 𝑅 ) )
17	16	imp	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ 𝑅 ∧ - 𝐵 ∈ 𝑅 ) ) → ( 𝐴 + - 𝐵 ) ∈ 𝑅 )
18	15 17	syldan	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ) → ( 𝐴 + - 𝐵 ) ∈ 𝑅 )
19	12 18	eqeltrrd	⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ) → ( 𝐴 − 𝐵 ) ∈ 𝑅 )
20	19	ex	⊢ ( 𝑆 ∈ ℂ → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → ( 𝐴 − 𝐵 ) ∈ 𝑅 ) )