# Metamath Proof Explorer

## 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 ${⊢}{E}=\left\{{z}\in ℤ|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{z}=2{x}\right\}$
2zlidl.u ${⊢}{U}=\mathrm{LIdeal}\left({ℤ}_{\mathrm{ring}}\right)$
Assertion 2zlidl ${⊢}{E}\in {U}$

### Proof

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