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 = z | x z = 2 x
2zlidl.u U = LIdeal ring
Assertion 2zlidl E U

Proof

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