lazmulzcl

Description: The extended integers are closed under multiplication with an integer. (Contributed by AV, 25-Oct-2026)

		Ref	Expression
	Hypothesis	laznegcl.r	No typesetting found for \|- R = ( Z[]l ` S ) with typecode \|-
	Assertion	lazmulzcl	$⊢ S \in ℂ \to ((B \in ℤ \land A \in R) \to B A \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		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	3	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 \|-
5	4	adantr	Could not format ( ( S e. CC /\ B e. ZZ ) -> ( 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 /\ B e. ZZ ) -> ( A e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) with typecode \|-
6	2 5	biimtrid	$⊢ (S \in ℂ \land B \in ℤ) \to (A \in R \to \exists a \in ℤ \exists b \in ℤ A = a + b S)$
7		zcn	$⊢ B \in ℤ \to B \in ℂ$
8	7	adantl	$⊢ (S \in ℂ \land B \in ℤ) \to B \in ℂ$
9	8	adantr	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B \in ℂ$
10		zcn	$⊢ b \in ℤ \to b \in ℂ$
11	10	adantl	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℂ$
12	11	adantl	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
13		simpll	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to S \in ℂ$
14	9 12 13	mulassd	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B b S = B b S$
15	14	eqcomd	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B b S = B b S$
16	15	oveq2d	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B a + B b S = B a + B b S$
17		zmulcl	$⊢ (B \in ℤ \land a \in ℤ) \to B a \in ℤ$
18	17	ad2ant2lr	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B a \in ℤ$
19		zmulcl	$⊢ (B \in ℤ \land b \in ℤ) \to B b \in ℤ$
20	19	ad2ant2l	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B b \in ℤ$
21	18 20	jca	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to (B a \in ℤ \land B b \in ℤ)$
22		lazlinz	Could not format ( S e. CC -> ( ( ( B x. a ) e. ZZ /\ ( B x. b ) e. ZZ ) -> ( ( B x. a ) + ( ( B x. b ) x. S ) ) e. ( Z[]l ` S ) ) ) : No typesetting found for \|- ( S e. CC -> ( ( ( B x. a ) e. ZZ /\ ( B x. b ) e. ZZ ) -> ( ( B x. a ) + ( ( B x. b ) x. S ) ) e. ( Z[]l ` S ) ) ) with typecode \|-
23	13 21 22	sylc	Could not format ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) + ( ( B x. b ) x. S ) ) e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) + ( ( B x. b ) x. S ) ) e. ( Z[]l ` S ) ) with typecode \|-
24	16 23	eqeltrd	Could not format ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) + ( B x. ( b x. S ) ) ) e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) + ( B x. ( b x. S ) ) ) e. ( Z[]l ` S ) ) with typecode \|-
25		zcn	$⊢ a \in ℤ \to a \in ℂ$
26	25	adantr	$⊢ (a \in ℤ \land b \in ℤ) \to a \in ℂ$
27	26	adantl	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
28		simpl	$⊢ (S \in ℂ \land B \in ℤ) \to S \in ℂ$
29		mulcl	$⊢ (b \in ℂ \land S \in ℂ) \to b S \in ℂ$
30	11 28 29	syl2anr	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to b S \in ℂ$
31	9 27 30	adddid	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B (a + b S) = B a + B b S$
32	1	a1i	Could not format ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> R = ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> R = ( Z[]l ` S ) ) with typecode \|-
33	24 31 32	3eltr4d	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to B (a + b S) \in R$
34		oveq2	$⊢ A = a + b S \to B A = B (a + b S)$
35	34	eleq1d	$⊢ A = a + b S \to (B A \in R \leftrightarrow B (a + b S) \in R)$
36	33 35	syl5ibrcom	$⊢ ((S \in ℂ \land B \in ℤ) \land (a \in ℤ \land b \in ℤ)) \to (A = a + b S \to B A \in R)$
37	36	rexlimdvva	$⊢ (S \in ℂ \land B \in ℤ) \to (\exists a \in ℤ \exists b \in ℤ A = a + b S \to B A \in R)$
38	6 37	syld	$⊢ (S \in ℂ \land B \in ℤ) \to (A \in R \to B A \in R)$
39	38	expimpd	$⊢ S \in ℂ \to ((B \in ℤ \land A \in R) \to B A \in R)$

Metamath Proof Explorer

Theorem lazmulzcl

Proof