Theorem laznegcl

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

	Ref	Expression
Hypothesis	laznegcl.r	No typesetting found for |- R = ( Z[]l ` S ) with typecode |-
Assertion	laznegcl	$$⊢S\in ℂ\to \left(A\in R\to -A\in R\right)$$

Proof

Step	Hyp	Ref	Expression
1		laznegcl.r	Could not format R = ( Z[]l ` S ) : No typesetting found for |- R = ( Z[]l ` S ) with typecode |-
2	1	eleq2i	Could not format ( A e. R <-> A e. ( Z[]l ` S ) ) : No typesetting found for |- ( A e. R <-> A e. ( Z[]l ` S ) ) with typecode |-
3		ellazim	Could not format ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) with typecode |-
4		negeq	$$⊢A=a+bS\to -A=-\left(a+bS\right)$$
5		zcn	$$⊢a\in \mathbb{Z}\to a\in ℂ$$
6	5	adantr	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to a\in ℂ$$
7	6	adantl	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC ) with typecode |-
8		zcn	$$⊢b\in \mathbb{Z}\to b\in ℂ$$
9	8	adantl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to b\in ℂ$$
10		simpl	Could not format ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> S e. CC ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> S e. CC ) with typecode |-
11		mulcl	$$⊢\left(b\in ℂ\wedge S\in ℂ\right)\to bS\in ℂ$$
12	9 10 11	syl2anr	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. S ) e. CC ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. S ) e. CC ) with typecode |-
13	7 12	negdid	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( a + ( b x. S ) ) = ( -u a + -u ( b x. S ) ) ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( a + ( b x. S ) ) = ( -u a + -u ( b x. S ) ) ) with typecode |-
14	9	adantl	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC ) with typecode |-
15	10	adantr	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> S e. CC ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> S e. CC ) with typecode |-
16	14 15	mulneg1d	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u b x. S ) = -u ( b x. S ) ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u b x. S ) = -u ( b x. S ) ) with typecode |-
17	16	eqcomd	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( b x. S ) = ( -u b x. S ) ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( b x. S ) = ( -u b x. S ) ) with typecode |-
18	17	oveq2d	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + -u ( b x. S ) ) = ( -u a + ( -u b x. S ) ) ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + -u ( b x. S ) ) = ( -u a + ( -u b x. S ) ) ) with typecode |-
19	13 18	eqtrd	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( a + ( b x. S ) ) = ( -u a + ( -u b x. S ) ) ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( a + ( b x. S ) ) = ( -u a + ( -u b x. S ) ) ) with typecode |-
20	4 19	sylan9eqr	Could not format ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> -u A = ( -u a + ( -u b x. S ) ) ) : No typesetting found for |- ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> -u A = ( -u a + ( -u b x. S ) ) ) with typecode |-
21		znegcl	$$⊢a\in \mathbb{Z}\to -a\in \mathbb{Z}$$
22		znegcl	$$⊢b\in \mathbb{Z}\to -b\in \mathbb{Z}$$
23	21 22	anim12i	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to \left(-a\in \mathbb{Z}\wedge -b\in \mathbb{Z}\right)$$
24		lazlinz	Could not format ( S e. CC -> ( ( -u a e. ZZ /\ -u b e. ZZ ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) ) ) : No typesetting found for |- ( S e. CC -> ( ( -u a e. ZZ /\ -u b e. ZZ ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) ) ) with typecode |-
25	24	imp	Could not format ( ( S e. CC /\ ( -u a e. ZZ /\ -u b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) ) : No typesetting found for |- ( ( S e. CC /\ ( -u a e. ZZ /\ -u b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) ) with typecode |-
26	10 23 25	syl2an	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) ) with typecode |-
27	26 1	eleqtrrdi	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. R ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. R ) with typecode |-
28	27	adantr	Could not format ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> ( -u a + ( -u b x. S ) ) e. R ) : No typesetting found for |- ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> ( -u a + ( -u b x. S ) ) e. R ) with typecode |-
29	20 28	eqeltrd	Could not format ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> -u A e. R ) : No typesetting found for |- ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> -u A e. R ) with typecode |-
30	29	ex	Could not format ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A = ( a + ( b x. S ) ) -> -u A e. R ) ) : No typesetting found for |- ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A = ( a + ( b x. S ) ) -> -u A e. R ) ) with typecode |-
31	30	rexlimdvva	Could not format ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) -> -u A e. R ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) -> -u A e. R ) ) with typecode |-
32	3 31	mpd	Could not format ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> -u A e. R ) : No typesetting found for |- ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> -u A e. R ) with typecode |-
33	32	ex	Could not format ( S e. CC -> ( A e. ( Z[]l ` S ) -> -u A e. R ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[]l ` S ) -> -u A e. R ) ) with typecode |-
34	2 33	biimtrid	$$⊢S\in ℂ\to \left(A\in R\to -A\in R\right)$$