Theorem lazsubcl

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

	Ref	Expression
Hypothesis	laznegcl.r	|- R = ( Z[]l ` S )
Assertion	lazsubcl	|- ( S e. CC -> ( ( A e. R /\ B e. R ) -> ( A - B ) e. R ) )

Proof

Step	Hyp	Ref	Expression
1		laznegcl.r	|- R = ( Z[]l ` S )
2	1	eleq2i	|- ( A e. R <-> A e. ( Z[]l ` S ) )
3		lazcn	|- ( S e. CC -> ( A e. ( Z[]l ` S ) -> A e. CC ) )
4	3	a1dd	|- ( S e. CC -> ( A e. ( Z[]l ` S ) -> ( B e. R -> A e. CC ) ) )
5	2 4	biimtrid	|- ( S e. CC -> ( A e. R -> ( B e. R -> A e. CC ) ) )
6	5	imp32	|- ( ( S e. CC /\ ( A e. R /\ B e. R ) ) -> A e. CC )
7	1	eleq2i	|- ( B e. R <-> B e. ( Z[]l ` S ) )
8		lazcn	|- ( S e. CC -> ( B e. ( Z[]l ` S ) -> B e. CC ) )
9	7 8	biimtrid	|- ( S e. CC -> ( B e. R -> B e. CC ) )
10	9	adantld	|- ( S e. CC -> ( ( A e. R /\ B e. R ) -> B e. CC ) )
11	10	imp	|- ( ( S e. CC /\ ( A e. R /\ B e. R ) ) -> B e. CC )
12	6 11	negsubd	|- ( ( S e. CC /\ ( A e. R /\ B e. R ) ) -> ( A + -u B ) = ( A - B ) )
13	1	laznegcl	|- ( S e. CC -> ( B e. R -> -u B e. R ) )
14	13	anim2d	|- ( S e. CC -> ( ( A e. R /\ B e. R ) -> ( A e. R /\ -u B e. R ) ) )
15	14	imp	|- ( ( S e. CC /\ ( A e. R /\ B e. R ) ) -> ( A e. R /\ -u B e. R ) )
16	1	lazaddcl	|- ( S e. CC -> ( ( A e. R /\ -u B e. R ) -> ( A + -u B ) e. R ) )
17	16	imp	|- ( ( S e. CC /\ ( A e. R /\ -u B e. R ) ) -> ( A + -u B ) e. R )
18	15 17	syldan	|- ( ( S e. CC /\ ( A e. R /\ B e. R ) ) -> ( A + -u B ) e. R )
19	12 18	eqeltrrd	|- ( ( S e. CC /\ ( A e. R /\ B e. R ) ) -> ( A - B ) e. R )
20	19	ex	|- ( S e. CC -> ( ( A e. R /\ B e. R ) -> ( A - B ) e. R ) )