Step |
Hyp |
Ref |
Expression |
1 |
|
2zrng.e |
⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } |
2 |
|
2z |
⊢ 2 ∈ ℤ |
3 |
|
2cn |
⊢ 2 ∈ ℂ |
4 |
|
1zzd |
⊢ ( 2 ∈ ℂ → 1 ∈ ℤ ) |
5 |
|
oveq2 |
⊢ ( 𝑥 = 1 → ( 2 · 𝑥 ) = ( 2 · 1 ) ) |
6 |
5
|
eqeq2d |
⊢ ( 𝑥 = 1 → ( 2 = ( 2 · 𝑥 ) ↔ 2 = ( 2 · 1 ) ) ) |
7 |
6
|
adantl |
⊢ ( ( 2 ∈ ℂ ∧ 𝑥 = 1 ) → ( 2 = ( 2 · 𝑥 ) ↔ 2 = ( 2 · 1 ) ) ) |
8 |
|
mulid1 |
⊢ ( 2 ∈ ℂ → ( 2 · 1 ) = 2 ) |
9 |
8
|
eqcomd |
⊢ ( 2 ∈ ℂ → 2 = ( 2 · 1 ) ) |
10 |
4 7 9
|
rspcedvd |
⊢ ( 2 ∈ ℂ → ∃ 𝑥 ∈ ℤ 2 = ( 2 · 𝑥 ) ) |
11 |
3 10
|
ax-mp |
⊢ ∃ 𝑥 ∈ ℤ 2 = ( 2 · 𝑥 ) |
12 |
|
eqeq1 |
⊢ ( 𝑧 = 2 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 2 = ( 2 · 𝑥 ) ) ) |
13 |
12
|
rexbidv |
⊢ ( 𝑧 = 2 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 2 = ( 2 · 𝑥 ) ) ) |
14 |
13
|
elrab |
⊢ ( 2 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ↔ ( 2 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 2 = ( 2 · 𝑥 ) ) ) |
15 |
2 11 14
|
mpbir2an |
⊢ 2 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } |
16 |
15 1
|
eleqtrri |
⊢ 2 ∈ 𝐸 |