Theorem 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	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zlidl.u	⊢ 𝑈 = ( LIdeal ‘ ℤring )
Assertion	2zlidl	⊢ 𝐸 ∈ 𝑈

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zlidl.u	⊢ 𝑈 = ( LIdeal ‘ ℤring )
3		ssrab2	⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ⊆ ℤ
4	1 3	eqsstri	⊢ 𝐸 ⊆ ℤ
5	1	0even	⊢ 0 ∈ 𝐸
6	5	ne0ii	⊢ 𝐸 ≠ ∅
7		eqeq1	⊢ ( 𝑧 = 𝑗 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑗 = ( 2 · 𝑥 ) ) )
8	7	rexbidv	⊢ ( 𝑧 = 𝑗 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) )
9	8 1	elrab2	⊢ ( 𝑗 ∈ 𝐸 ↔ ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) )
10		eqeq1	⊢ ( 𝑧 = 𝑘 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑘 = ( 2 · 𝑥 ) ) )
11	10	rexbidv	⊢ ( 𝑧 = 𝑘 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) )
12	11 1	elrab2	⊢ ( 𝑘 ∈ 𝐸 ↔ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) )
13	9 12	anbi12i	⊢ ( ( 𝑗 ∈ 𝐸 ∧ 𝑘 ∈ 𝐸 ) ↔ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) )
14		simpl	⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) ) → 𝑖 ∈ ℤ )
15		simprll	⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) ) → 𝑗 ∈ ℤ )
16	14 15	zmulcld	⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) ) → ( 𝑖 · 𝑗 ) ∈ ℤ )
17		simpl	⊢ ( ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) → 𝑘 ∈ ℤ )
18	17	adantl	⊢ ( ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) → 𝑘 ∈ ℤ )
19	18	adantl	⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) ) → 𝑘 ∈ ℤ )
20	16 19	zaddcld	⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) ) → ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ ℤ )
21		oveq2	⊢ ( 𝑥 = 𝑎 → ( 2 · 𝑥 ) = ( 2 · 𝑎 ) )
22	21	eqeq2d	⊢ ( 𝑥 = 𝑎 → ( 𝑗 = ( 2 · 𝑥 ) ↔ 𝑗 = ( 2 · 𝑎 ) ) )
23	22	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ↔ ∃ 𝑎 ∈ ℤ 𝑗 = ( 2 · 𝑎 ) )
24		oveq2	⊢ ( 𝑥 = 𝑏 → ( 2 · 𝑥 ) = ( 2 · 𝑏 ) )
25	24	eqeq2d	⊢ ( 𝑥 = 𝑏 → ( 𝑘 = ( 2 · 𝑥 ) ↔ 𝑘 = ( 2 · 𝑏 ) ) )
26	25	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ↔ ∃ 𝑏 ∈ ℤ 𝑘 = ( 2 · 𝑏 ) )
27		simpr	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℤ )
28		simprll	⊢ ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
29	28	adantr	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → 𝑎 ∈ ℤ )
30	27 29	zmulcld	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( 𝑖 · 𝑎 ) ∈ ℤ )
31		simp-4l	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → 𝑏 ∈ ℤ )
32	30 31	zaddcld	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝑖 · 𝑎 ) + 𝑏 ) ∈ ℤ )
33		simpr	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) → 𝑗 = ( 2 · 𝑎 ) )
34	33	ad2antrl	⊢ ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) → 𝑗 = ( 2 · 𝑎 ) )
35	34	oveq2d	⊢ ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) → ( 𝑖 · 𝑗 ) = ( 𝑖 · ( 2 · 𝑎 ) ) )
36		simpllr	⊢ ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) → 𝑘 = ( 2 · 𝑏 ) )
37	35 36	oveq12d	⊢ ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) → ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( ( 𝑖 · ( 2 · 𝑎 ) ) + ( 2 · 𝑏 ) ) )
38	37	adantr	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( ( 𝑖 · ( 2 · 𝑎 ) ) + ( 2 · 𝑏 ) ) )
39		oveq2	⊢ ( 𝑥 = ( ( 𝑖 · 𝑎 ) + 𝑏 ) → ( 2 · 𝑥 ) = ( 2 · ( ( 𝑖 · 𝑎 ) + 𝑏 ) ) )
40	38 39	eqeqan12d	⊢ ( ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) ∧ 𝑥 = ( ( 𝑖 · 𝑎 ) + 𝑏 ) ) → ( ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ↔ ( ( 𝑖 · ( 2 · 𝑎 ) ) + ( 2 · 𝑏 ) ) = ( 2 · ( ( 𝑖 · 𝑎 ) + 𝑏 ) ) ) )
41		zcn	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
42	41	adantl	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ )
43		2cnd	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → 2 ∈ ℂ )
44		zcn	⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
45	44	adantr	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) → 𝑎 ∈ ℂ )
46	45	ad2antrl	⊢ ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
47	46	adantr	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → 𝑎 ∈ ℂ )
48	42 43 47	mul12d	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( 𝑖 · ( 2 · 𝑎 ) ) = ( 2 · ( 𝑖 · 𝑎 ) ) )
49	48	oveq1d	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝑖 · ( 2 · 𝑎 ) ) + ( 2 · 𝑏 ) ) = ( ( 2 · ( 𝑖 · 𝑎 ) ) + ( 2 · 𝑏 ) ) )
50	42 47	mulcld	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( 𝑖 · 𝑎 ) ∈ ℂ )
51		zcn	⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
52	51	ad4antr	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → 𝑏 ∈ ℂ )
53	43 50 52	adddid	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( 2 · ( ( 𝑖 · 𝑎 ) + 𝑏 ) ) = ( ( 2 · ( 𝑖 · 𝑎 ) ) + ( 2 · 𝑏 ) ) )
54	49 53	eqtr4d	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝑖 · ( 2 · 𝑎 ) ) + ( 2 · 𝑏 ) ) = ( 2 · ( ( 𝑖 · 𝑎 ) + 𝑏 ) ) )
55	32 40 54	rspcedvd	⊢ ( ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) ) ∧ 𝑖 ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) )
56	55	exp41	⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑘 = ( 2 · 𝑏 ) ) → ( 𝑘 ∈ ℤ → ( ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) ) )
57	56	rexlimiva	⊢ ( ∃ 𝑏 ∈ ℤ 𝑘 = ( 2 · 𝑏 ) → ( 𝑘 ∈ ℤ → ( ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) ) )
58	26 57	sylbi	⊢ ( ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) → ( 𝑘 ∈ ℤ → ( ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) ) )
59	58	impcom	⊢ ( ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) → ( ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) ∧ 𝑗 ∈ ℤ ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) )
60	59	expdcom	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑗 = ( 2 · 𝑎 ) ) → ( 𝑗 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) ) )
61	60	rexlimiva	⊢ ( ∃ 𝑎 ∈ ℤ 𝑗 = ( 2 · 𝑎 ) → ( 𝑗 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) ) )
62	23 61	sylbi	⊢ ( ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) → ( 𝑗 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) ) )
63	62	impcom	⊢ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) → ( ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) ) )
64	63	imp	⊢ ( ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) → ( 𝑖 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) )
65	64	impcom	⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) ) → ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) )
66		eqeq1	⊢ ( 𝑧 = ( ( 𝑖 · 𝑗 ) + 𝑘 ) → ( 𝑧 = ( 2 · 𝑥 ) ↔ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) )
67	66	rexbidv	⊢ ( 𝑧 = ( ( 𝑖 · 𝑗 ) + 𝑘 ) → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) )
68	67 1	elrab2	⊢ ( ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ 𝐸 ↔ ( ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ ( ( 𝑖 · 𝑗 ) + 𝑘 ) = ( 2 · 𝑥 ) ) )
69	20 65 68	sylanbrc	⊢ ( ( 𝑖 ∈ ℤ ∧ ( ( 𝑗 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑗 = ( 2 · 𝑥 ) ) ∧ ( 𝑘 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑘 = ( 2 · 𝑥 ) ) ) ) → ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ 𝐸 )
70	13 69	sylan2b	⊢ ( ( 𝑖 ∈ ℤ ∧ ( 𝑗 ∈ 𝐸 ∧ 𝑘 ∈ 𝐸 ) ) → ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ 𝐸 )
71	70	ralrimivva	⊢ ( 𝑖 ∈ ℤ → ∀ 𝑗 ∈ 𝐸 ∀ 𝑘 ∈ 𝐸 ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ 𝐸 )
72	71	rgen	⊢ ∀ 𝑖 ∈ ℤ ∀ 𝑗 ∈ 𝐸 ∀ 𝑘 ∈ 𝐸 ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ 𝐸
73		zringbas	⊢ ℤ = ( Base ‘ ℤring )
74		zringplusg	⊢ + = ( +g ‘ ℤring )
75		zringmulr	⊢ · = ( .r ‘ ℤring )
76	2 73 74 75	islidl	⊢ ( 𝐸 ∈ 𝑈 ↔ ( 𝐸 ⊆ ℤ ∧ 𝐸 ≠ ∅ ∧ ∀ 𝑖 ∈ ℤ ∀ 𝑗 ∈ 𝐸 ∀ 𝑘 ∈ 𝐸 ( ( 𝑖 · 𝑗 ) + 𝑘 ) ∈ 𝐸 ) )
77	4 6 72 76	mpbir3an	⊢ 𝐸 ∈ 𝑈