lazmulcl

Description: The extended integers are closed under multiplication if the square of the adjoined complex number is an extended integer. (Contributed by AV, 25-Oct-2026)

		Ref	Expression
	Hypothesis	laznegcl.r	No typesetting found for \|- R = ( Z[]l ` S ) with typecode \|-
	Assertion	lazmulcl	$⊢ (S \in ℂ \land S^{2} \in R) \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	6 8	anim12d	Could not format ( S e. CC -> ( ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) /\ E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) ) ) : No typesetting found for \|- ( S e. CC -> ( ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) /\ E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) ) ) with typecode \|-
10	4 9	biimtrid	$⊢ S \in ℂ \to ((A \in R \land B \in R) \to (\exists a \in ℤ \exists b \in ℤ A = a + b S \land \exists c \in ℤ \exists d \in ℤ B = c + d S))$
11	10	adantr	$⊢ (S \in ℂ \land S^{2} \in R) \to ((A \in R \land B \in R) \to (\exists a \in ℤ \exists b \in ℤ A = a + b S \land \exists c \in ℤ \exists d \in ℤ B = c + d S))$
12		oveq12	$⊢ (A = a + b S \land B = c + d S) \to A B = (a + b S) (c + d S)$
13	12	ancoms	$⊢ (B = c + d S \land A = a + b S) \to A B = (a + b S) (c + d S)$
14	13	adantl	$⊢ ((((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + d S \land A = a + b S)) \to A B = (a + b S) (c + d S)$
15		zcn	$⊢ a \in ℤ \to a \in ℂ$
16	15	ad2antrl	$⊢ ((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
17	16	adantr	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a \in ℂ$
18		zcn	$⊢ b \in ℤ \to b \in ℂ$
19	18	ad2antll	$⊢ ((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
20	19	adantr	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to b \in ℂ$
21		simplll	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to S \in ℂ$
22		zcn	$⊢ c \in ℤ \to c \in ℂ$
23	22	ad2antrl	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to c \in ℂ$
24		zcn	$⊢ d \in ℤ \to d \in ℂ$
25	24	ad2antll	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to d \in ℂ$
26	17 20 21 23 25	addmuldir2d	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (a + b S) (c + d S) = a c + (a d + c b) S + b d S^{2}$
27		simpl	$⊢ (a \in ℤ \land b \in ℤ) \to a \in ℤ$
28	27	adantl	$⊢ ((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
29		simpl	$⊢ (c \in ℤ \land d \in ℤ) \to c \in ℤ$
30		zmulcl	$⊢ (a \in ℤ \land c \in ℤ) \to a c \in ℤ$
31	28 29 30	syl2an	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a c \in ℤ$
32		zellaz	Could not format ( ( S e. CC /\ ( a x. c ) e. ZZ ) -> ( a x. c ) e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( S e. CC /\ ( a x. c ) e. ZZ ) -> ( a x. c ) e. ( Z[]l ` S ) ) with typecode \|-
33	21 31 32	syl2anc	Could not format ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a x. c ) e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a x. c ) e. ( Z[]l ` S ) ) with typecode \|-
34	33 1	eleqtrrdi	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a c \in R$
35		simpr	$⊢ (c \in ℤ \land d \in ℤ) \to d \in ℤ$
36		zmulcl	$⊢ (a \in ℤ \land d \in ℤ) \to a d \in ℤ$
37	28 35 36	syl2an	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a d \in ℤ$
38		simpr	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℤ$
39	38	adantl	$⊢ ((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \to b \in ℤ$
40		zmulcl	$⊢ (c \in ℤ \land b \in ℤ) \to c b \in ℤ$
41	29 39 40	syl2anr	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to c b \in ℤ$
42	37 41	zaddcld	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a d + c b \in ℤ$
43		adcnmulzlaz	Could not format ( ( S e. CC /\ ( ( a x. d ) + ( c x. b ) ) e. ZZ ) -> ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( S e. CC /\ ( ( a x. d ) + ( c x. b ) ) e. ZZ ) -> ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. ( Z[]l ` S ) ) with typecode \|-
44	21 42 43	syl2anc	Could not format ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. ( Z[]l ` S ) ) with typecode \|-
45	44 1	eleqtrrdi	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (a d + c b) S \in R$
46	34 45	jca	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (a c \in R \land (a d + c b) S \in R)$
47	1	lazaddcl	$⊢ S \in ℂ \to ((a c \in R \land (a d + c b) S \in R) \to a c + (a d + c b) S \in R)$
48	21 46 47	sylc	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a c + (a d + c b) S \in R$
49		zmulcl	$⊢ (b \in ℤ \land d \in ℤ) \to b d \in ℤ$
50	39 35 49	syl2an	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to b d \in ℤ$
51		simpllr	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to S^{2} \in R$
52	50 51	jca	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (b d \in ℤ \land S^{2} \in R)$
53	1	lazmulzcl	$⊢ S \in ℂ \to ((b d \in ℤ \land S^{2} \in R) \to b d S^{2} \in R)$
54	21 52 53	sylc	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to b d S^{2} \in R$
55	48 54	jca	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (a c + (a d + c b) S \in R \land b d S^{2} \in R)$
56	1	lazaddcl	$⊢ S \in ℂ \to ((a c + (a d + c b) S \in R \land b d S^{2} \in R) \to a c + (a d + c b) S + b d S^{2} \in R)$
57	21 55 56	sylc	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to a c + (a d + c b) S + b d S^{2} \in R$
58	26 57	eqeltrd	$⊢ (((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (a + b S) (c + d S) \in R$
59	58	adantr	$⊢ ((((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + d S \land A = a + b S)) \to (a + b S) (c + d S) \in R$
60	14 59	eqeltrd	$⊢ ((((S \in ℂ \land S^{2} \in R) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \land (B = c + d S \land A = a + b S)) \to A B \in R$
61	60	exp32	$⊢ (((S \in ℂ \land S^{2} \in R) \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))$
62	61	rexlimdvva	$⊢ ((S \in ℂ \land S^{2} \in R) \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))$
63	62	com23	$⊢ ((S \in ℂ \land S^{2} \in R) \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))$
64	63	rexlimdvva	$⊢ (S \in ℂ \land S^{2} \in R) \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))$
65	64	impd	$⊢ (S \in ℂ \land S^{2} \in R) \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)$
66	11 65	syld	$⊢ (S \in ℂ \land S^{2} \in R) \to ((A \in R \land B \in R) \to A B \in R)$

Metamath Proof Explorer

Theorem lazmulcl

Proof