lazaddcl

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

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

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	1	eleq2i	Could not format ( B e. R <-> B e. ( Z[]l ` S ) ) : No typesetting found for \|- ( B e. R <-> B e. ( Z[]l ` S ) ) with typecode \|-
4	2 3	anbi12i	Could not format ( ( A e. R /\ B e. R ) <-> ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) ) : No typesetting found for \|- ( ( A e. R /\ B e. R ) <-> ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) ) with typecode \|-
5		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 \|-
6	5	ex	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 \|-
7		ellazim	Could not format ( ( S e. CC /\ B e. ( Z[]l ` S ) ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) : No typesetting found for \|- ( ( S e. CC /\ B e. ( Z[]l ` S ) ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) with typecode \|-
8	7	ex	Could not format ( S e. CC -> ( B e. ( Z[]l ` S ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) ) : No typesetting found for \|- ( S e. CC -> ( B e. ( Z[]l ` S ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) ) with typecode \|-
9		simpl	$⊢ (S \in ℂ \land (a \in ℤ \land b \in ℤ)) \to S \in ℂ$
10	9	adantr	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to S \in ℂ$
11		simpl	$⊢ (a \in ℤ \land b \in ℤ) \to a \in ℤ$
12	11	adantl	$⊢ (S \in ℂ \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
13		simpl	$⊢ (c \in ℤ \land d \in ℤ) \to c \in ℤ$
14		zaddcl	$⊢ (a \in ℤ \land c \in ℤ) \to a + c \in ℤ$
15	12 13 14	syl2an	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a + c \in ℤ$
16		simpr	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℤ$
17	16	adantl	$⊢ (S \in ℂ \land (a \in ℤ \land b \in ℤ)) \to b \in ℤ$
18		simpr	$⊢ (c \in ℤ \land d \in ℤ) \to d \in ℤ$
19		zaddcl	$⊢ (b \in ℤ \land d \in ℤ) \to b + d \in ℤ$
20	17 18 19	syl2an	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to b + d \in ℤ$
21	15 20	jca	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (a + c \in ℤ \land b + d \in ℤ)$
22		lazlinz	Could not format ( S e. CC -> ( ( ( a + c ) e. ZZ /\ ( b + d ) e. ZZ ) -> ( ( a + c ) + ( ( b + d ) x. S ) ) e. ( Z[]l ` S ) ) ) : No typesetting found for \|- ( S e. CC -> ( ( ( a + c ) e. ZZ /\ ( b + d ) e. ZZ ) -> ( ( a + c ) + ( ( b + d ) x. S ) ) e. ( Z[]l ` S ) ) ) with typecode \|-
23	10 21 22	sylc	Could not format ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + c ) + ( ( b + d ) x. S ) ) e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + c ) + ( ( b + d ) x. S ) ) e. ( Z[]l ` S ) ) with typecode \|-
24		zcn	$⊢ a \in ℤ \to a \in ℂ$
25	24	ad2antrl	$⊢ (S \in ℂ \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
26	25	adantr	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a \in ℂ$
27		zcn	$⊢ b \in ℤ \to b \in ℂ$
28	27	ad2antll	$⊢ (S \in ℂ \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
29	28	adantr	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to b \in ℂ$
30	29 10	mulcld	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to b S \in ℂ$
31		zcn	$⊢ c \in ℤ \to c \in ℂ$
32	31	ad2antrl	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to c \in ℂ$
33		zcn	$⊢ d \in ℤ \to d \in ℂ$
34	33	ad2antll	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to d \in ℂ$
35	34 10	mulcld	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to d S \in ℂ$
36	26 30 32 35	add4d	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a + b S + c + d S = a + c + b S + d S$
37	29 34 10	adddird	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (b + d) S = b S + d S$
38	37	eqcomd	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to b S + d S = (b + d) S$
39	38	oveq2d	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a + c + b S + d S = a + c + (b + d) S$
40	36 39	eqtrd	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a + b S + c + d S = a + c + (b + d) S$
41	1	a1i	Could not format ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> R = ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> R = ( Z[]l ` S ) ) with typecode \|-
42	23 40 41	3eltr4d	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a + b S + c + d S \in R$
43		oveq12	$⊢ (A = a + b S \land B = c + d S) \to A + B = a + b S + c + d S$
44	43	eleq1d	$⊢ (A = a + b S \land B = c + d S) \to (A + B \in R \leftrightarrow a + b S + c + d S \in R)$
45	44	ancoms	$⊢ (B = c + d S \land A = a + b S) \to (A + B \in R \leftrightarrow a + b S + c + d S \in R)$
46	42 45	syl5ibrcom	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to ((B = c + d S \land A = a + b S) \to A + B \in R)$
47	46	expd	$⊢ ((S \in ℂ \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (B = c + d S \to (A = a + b S \to A + B \in R))$
48	47	rexlimdvva	$⊢ (S \in ℂ \land (a \in ℤ \land b \in ℤ)) \to (\exists c \in ℤ \exists d \in ℤ B = c + d S \to (A = a + b S \to A + B \in R))$
49	48	com23	$⊢ (S \in ℂ \land (a \in ℤ \land b \in ℤ)) \to (A = a + b S \to (\exists c \in ℤ \exists d \in ℤ B = c + d S \to A + B \in R))$
50	49	rexlimdvva	$⊢ S \in ℂ \to (\exists a \in ℤ \exists b \in ℤ A = a + b S \to (\exists c \in ℤ \exists d \in ℤ B = c + d S \to A + B \in R))$
51	50	impd	$⊢ S \in ℂ \to ((\exists a \in ℤ \exists b \in ℤ A = a + b S \land \exists c \in ℤ \exists d \in ℤ B = c + d S) \to A + B \in R)$
52	6 8 51	syl2and	Could not format ( S e. CC -> ( ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) -> ( A + B ) e. R ) ) : No typesetting found for \|- ( S e. CC -> ( ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) -> ( A + B ) e. R ) ) with typecode \|-
53	4 52	biimtrid	$⊢ S \in ℂ \to ((A \in R \land B \in R) \to A + B \in R)$

Metamath Proof Explorer

Theorem lazaddcl

Proof