2zlidl

Description: The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020)

	Ref	Expression
Hypotheses	2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
	2zlidl.u	$⊢ U = LIdeal (ℤ_{ring})$
Assertion	2zlidl	$⊢ E \in U$

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
2		2zlidl.u	$⊢ U = LIdeal (ℤ_{ring})$
3		ssrab2	$⊢ \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \subseteq ℤ$
4	1 3	eqsstri	$⊢ E \subseteq ℤ$
5	1	0even	$⊢ 0 \in E$
6	5	ne0ii	$⊢ E \neq \emptyset$
7		eqeq1	$⊢ z = j \to (z = 2 x \leftrightarrow j = 2 x)$
8	7	rexbidv	$⊢ z = j \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ j = 2 x)$
9	8 1	elrab2	$⊢ j \in E \leftrightarrow (j \in ℤ \land \exists x \in ℤ j = 2 x)$
10		eqeq1	$⊢ z = k \to (z = 2 x \leftrightarrow k = 2 x)$
11	10	rexbidv	$⊢ z = k \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ k = 2 x)$
12	11 1	elrab2	$⊢ k \in E \leftrightarrow (k \in ℤ \land \exists x \in ℤ k = 2 x)$
13	9 12	anbi12i	$⊢ (j \in E \land k \in E) \leftrightarrow ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))$
14		simpl	$⊢ (i \in ℤ \land ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))) \to i \in ℤ$
15		simprll	$⊢ (i \in ℤ \land ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))) \to j \in ℤ$
16	14 15	zmulcld	$⊢ (i \in ℤ \land ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))) \to i j \in ℤ$
17		simpl	$⊢ (k \in ℤ \land \exists x \in ℤ k = 2 x) \to k \in ℤ$
18	17	adantl	$⊢ ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x)) \to k \in ℤ$
19	18	adantl	$⊢ (i \in ℤ \land ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))) \to k \in ℤ$
20	16 19	zaddcld	$⊢ (i \in ℤ \land ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))) \to i j + k \in ℤ$
21		oveq2	$⊢ x = a \to 2 x = 2 a$
22	21	eqeq2d	$⊢ x = a \to (j = 2 x \leftrightarrow j = 2 a)$
23	22	cbvrexvw	$⊢ \exists x \in ℤ j = 2 x \leftrightarrow \exists a \in ℤ j = 2 a$
24		oveq2	$⊢ x = b \to 2 x = 2 b$
25	24	eqeq2d	$⊢ x = b \to (k = 2 x \leftrightarrow k = 2 b)$
26	25	cbvrexvw	$⊢ \exists x \in ℤ k = 2 x \leftrightarrow \exists b \in ℤ k = 2 b$
27		simpr	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i \in ℤ$
28		simprll	$⊢ (((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \to a \in ℤ$
29	28	adantr	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to a \in ℤ$
30	27 29	zmulcld	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i a \in ℤ$
31		simp-4l	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to b \in ℤ$
32	30 31	zaddcld	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i a + b \in ℤ$
33		simpr	$⊢ (a \in ℤ \land j = 2 a) \to j = 2 a$
34	33	ad2antrl	$⊢ (((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \to j = 2 a$
35	34	oveq2d	$⊢ (((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \to i j = i 2 a$
36		simpllr	$⊢ (((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \to k = 2 b$
37	35 36	oveq12d	$⊢ (((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \to i j + k = i 2 a + 2 b$
38	37	adantr	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i j + k = i 2 a + 2 b$
39		oveq2	$⊢ x = i a + b \to 2 x = 2 (i a + b)$
40	38 39	eqeqan12d	$⊢ (((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \land x = i a + b) \to (i j + k = 2 x \leftrightarrow i 2 a + 2 b = 2 (i a + b))$
41		zcn	$⊢ i \in ℤ \to i \in ℂ$
42	41	adantl	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i \in ℂ$
43		2cnd	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to 2 \in ℂ$
44		zcn	$⊢ a \in ℤ \to a \in ℂ$
45	44	adantr	$⊢ (a \in ℤ \land j = 2 a) \to a \in ℂ$
46	45	ad2antrl	$⊢ (((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \to a \in ℂ$
47	46	adantr	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to a \in ℂ$
48	42 43 47	mul12d	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i 2 a = 2 i a$
49	48	oveq1d	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i 2 a + 2 b = 2 i a + 2 b$
50	42 47	mulcld	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i a \in ℂ$
51		zcn	$⊢ b \in ℤ \to b \in ℂ$
52	51	ad4antr	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to b \in ℂ$
53	43 50 52	adddid	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to 2 (i a + b) = 2 i a + 2 b$
54	49 53	eqtr4d	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to i 2 a + 2 b = 2 (i a + b)$
55	32 40 54	rspcedvd	$⊢ ((((b \in ℤ \land k = 2 b) \land k \in ℤ) \land ((a \in ℤ \land j = 2 a) \land j \in ℤ)) \land i \in ℤ) \to \exists x \in ℤ i j + k = 2 x$
56	55	exp41	$⊢ (b \in ℤ \land k = 2 b) \to (k \in ℤ \to (((a \in ℤ \land j = 2 a) \land j \in ℤ) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x)))$
57	56	rexlimiva	$⊢ \exists b \in ℤ k = 2 b \to (k \in ℤ \to (((a \in ℤ \land j = 2 a) \land j \in ℤ) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x)))$
58	26 57	sylbi	$⊢ \exists x \in ℤ k = 2 x \to (k \in ℤ \to (((a \in ℤ \land j = 2 a) \land j \in ℤ) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x)))$
59	58	impcom	$⊢ (k \in ℤ \land \exists x \in ℤ k = 2 x) \to (((a \in ℤ \land j = 2 a) \land j \in ℤ) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x))$
60	59	expdcom	$⊢ (a \in ℤ \land j = 2 a) \to (j \in ℤ \to ((k \in ℤ \land \exists x \in ℤ k = 2 x) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x)))$
61	60	rexlimiva	$⊢ \exists a \in ℤ j = 2 a \to (j \in ℤ \to ((k \in ℤ \land \exists x \in ℤ k = 2 x) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x)))$
62	23 61	sylbi	$⊢ \exists x \in ℤ j = 2 x \to (j \in ℤ \to ((k \in ℤ \land \exists x \in ℤ k = 2 x) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x)))$
63	62	impcom	$⊢ (j \in ℤ \land \exists x \in ℤ j = 2 x) \to ((k \in ℤ \land \exists x \in ℤ k = 2 x) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x))$
64	63	imp	$⊢ ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x)) \to (i \in ℤ \to \exists x \in ℤ i j + k = 2 x)$
65	64	impcom	$⊢ (i \in ℤ \land ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))) \to \exists x \in ℤ i j + k = 2 x$
66		eqeq1	$⊢ z = i j + k \to (z = 2 x \leftrightarrow i j + k = 2 x)$
67	66	rexbidv	$⊢ z = i j + k \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ i j + k = 2 x)$
68	67 1	elrab2	$⊢ i j + k \in E \leftrightarrow (i j + k \in ℤ \land \exists x \in ℤ i j + k = 2 x)$
69	20 65 68	sylanbrc	$⊢ (i \in ℤ \land ((j \in ℤ \land \exists x \in ℤ j = 2 x) \land (k \in ℤ \land \exists x \in ℤ k = 2 x))) \to i j + k \in E$
70	13 69	sylan2b	$⊢ (i \in ℤ \land (j \in E \land k \in E)) \to i j + k \in E$
71	70	ralrimivva	$⊢ i \in ℤ \to \forall j \in E \forall k \in E i j + k \in E$
72	71	rgen	$⊢ \forall i \in ℤ \forall j \in E \forall k \in E i j + k \in E$
73		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
74		zringplusg	$⊢ + = +_{ℤ_{ring}}$
75		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
76	2 73 74 75	islidl	$⊢ E \in U \leftrightarrow (E \subseteq ℤ \land E \neq \emptyset \land \forall i \in ℤ \forall j \in E \forall k \in E i j + k \in E)$
77	4 6 72 76	mpbir3an	$⊢ E \in U$

Metamath Proof Explorer

Theorem 2zlidl

Proof