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 ⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 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 ⊢ 𝐸 ∈ 𝑈