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 |
⊢ 𝐸 ∈ 𝑈 |