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 e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2zlidl.u 
|- U = ( LIdeal ` ZZring )
Assertion 2zlidl 
|- E e. U

Proof

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