lazcjcl

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

		Ref	Expression
	Hypothesis	laznegcl.r	No typesetting found for \|- R = ( Z[]l ` S ) with typecode \|-
	Assertion	lazcjcl	$⊢ (S \in ℂ \land \overline{S} \in R) \to (A \in R \to \overline{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 /\ ( * ` S ) e. R ) -> ( 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 /\ ( * ` S ) e. R ) -> ( 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 \overline{S} \in R) \to (A \in R \to \exists a \in ℤ \exists b \in ℤ A = a + b S)$
7		fveq2	$⊢ A = a + b S \to \overline{A} = \overline{a + b S}$
8		zcn	$⊢ a \in ℤ \to a \in ℂ$
9	8	ad2antrl	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
10		zcn	$⊢ b \in ℤ \to b \in ℂ$
11	10	adantl	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℂ$
12		simpl	$⊢ (S \in ℂ \land \overline{S} \in R) \to S \in ℂ$
13		mulcl	$⊢ (b \in ℂ \land S \in ℂ) \to b S \in ℂ$
14	11 12 13	syl2anr	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to b S \in ℂ$
15	9 14	cjaddd	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{a + b S} = \overline{a} + \overline{b S}$
16		zre	$⊢ a \in ℤ \to a \in ℝ$
17	16	ad2antrl	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to a \in ℝ$
18	17	cjred	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{a} = a$
19	11	adantl	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
20	12	adantr	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to S \in ℂ$
21	19 20	cjmuld	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{b S} = \overline{b} \overline{S}$
22		zre	$⊢ b \in ℤ \to b \in ℝ$
23	22	adantl	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℝ$
24	23	adantl	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to b \in ℝ$
25	24	cjred	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{b} = b$
26	25	oveq1d	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{b} \overline{S} = b \overline{S}$
27	21 26	eqtrd	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{b S} = b \overline{S}$
28	18 27	oveq12d	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{a} + \overline{b S} = a + b \overline{S}$
29	15 28	eqtrd	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to \overline{a + b S} = a + b \overline{S}$
30	7 29	sylan9eqr	$⊢ (((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \land A = a + b S) \to \overline{A} = a + b \overline{S}$
31		zellaz	Could not format ( ( S e. CC /\ a e. ZZ ) -> a e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( S e. CC /\ a e. ZZ ) -> a e. ( Z[]l ` S ) ) with typecode \|-
32	31	ad2ant2r	Could not format ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ( Z[]l ` S ) ) with typecode \|-
33	32 1	eleqtrrdi	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to a \in R$
34		simpr	$⊢ (S \in ℂ \land \overline{S} \in R) \to \overline{S} \in R$
35		simpr	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℤ$
36	34 35	anim12ci	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to (b \in ℤ \land \overline{S} \in R)$
37	1	lazmulzcl	$⊢ S \in ℂ \to ((b \in ℤ \land \overline{S} \in R) \to b \overline{S} \in R)$
38	20 36 37	sylc	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to b \overline{S} \in R$
39	33 38	jca	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to (a \in R \land b \overline{S} \in R)$
40	1	lazaddcl	$⊢ S \in ℂ \to ((a \in R \land b \overline{S} \in R) \to a + b \overline{S} \in R)$
41	20 39 40	sylc	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to a + b \overline{S} \in R$
42	41	adantr	$⊢ (((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \land A = a + b S) \to a + b \overline{S} \in R$
43	30 42	eqeltrd	$⊢ (((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \land A = a + b S) \to \overline{A} \in R$
44	43	ex	$⊢ ((S \in ℂ \land \overline{S} \in R) \land (a \in ℤ \land b \in ℤ)) \to (A = a + b S \to \overline{A} \in R)$
45	44	rexlimdvva	$⊢ (S \in ℂ \land \overline{S} \in R) \to (\exists a \in ℤ \exists b \in ℤ A = a + b S \to \overline{A} \in R)$
46	6 45	syld	$⊢ (S \in ℂ \land \overline{S} \in R) \to (A \in R \to \overline{A} \in R)$

Metamath Proof Explorer

Theorem lazcjcl

Proof