Step |
Hyp |
Ref |
Expression |
1 |
|
df-even |
⊢ Even = { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ } |
2 |
|
simpr |
⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → ( 𝑧 / 2 ) ∈ ℤ ) |
3 |
|
oveq2 |
⊢ ( 𝑖 = ( 𝑧 / 2 ) → ( 2 · 𝑖 ) = ( 2 · ( 𝑧 / 2 ) ) ) |
4 |
3
|
eqeq2d |
⊢ ( 𝑖 = ( 𝑧 / 2 ) → ( 𝑧 = ( 2 · 𝑖 ) ↔ 𝑧 = ( 2 · ( 𝑧 / 2 ) ) ) ) |
5 |
4
|
adantl |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) ∧ 𝑖 = ( 𝑧 / 2 ) ) → ( 𝑧 = ( 2 · 𝑖 ) ↔ 𝑧 = ( 2 · ( 𝑧 / 2 ) ) ) ) |
6 |
|
zcn |
⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ ) |
7 |
6
|
adantr |
⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 𝑧 ∈ ℂ ) |
8 |
|
2cnd |
⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 2 ∈ ℂ ) |
9 |
|
2ne0 |
⊢ 2 ≠ 0 |
10 |
9
|
a1i |
⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 2 ≠ 0 ) |
11 |
7 8 10
|
divcan2d |
⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → ( 2 · ( 𝑧 / 2 ) ) = 𝑧 ) |
12 |
11
|
eqcomd |
⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → 𝑧 = ( 2 · ( 𝑧 / 2 ) ) ) |
13 |
2 5 12
|
rspcedvd |
⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑧 / 2 ) ∈ ℤ ) → ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ) |
14 |
13
|
ex |
⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 / 2 ) ∈ ℤ → ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ) ) |
15 |
|
oveq1 |
⊢ ( 𝑧 = ( 2 · 𝑖 ) → ( 𝑧 / 2 ) = ( ( 2 · 𝑖 ) / 2 ) ) |
16 |
|
zcn |
⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ ) |
17 |
16
|
adantl |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ ) |
18 |
|
2cnd |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ∈ ℂ ) |
19 |
9
|
a1i |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ≠ 0 ) |
20 |
17 18 19
|
divcan3d |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 2 · 𝑖 ) / 2 ) = 𝑖 ) |
21 |
15 20
|
sylan9eqr |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( 2 · 𝑖 ) ) → ( 𝑧 / 2 ) = 𝑖 ) |
22 |
|
simpr |
⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℤ ) |
23 |
22
|
adantr |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( 2 · 𝑖 ) ) → 𝑖 ∈ ℤ ) |
24 |
21 23
|
eqeltrd |
⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑧 = ( 2 · 𝑖 ) ) → ( 𝑧 / 2 ) ∈ ℤ ) |
25 |
24
|
rexlimdva2 |
⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) → ( 𝑧 / 2 ) ∈ ℤ ) ) |
26 |
14 25
|
impbid |
⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 / 2 ) ∈ ℤ ↔ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ) ) |
27 |
26
|
rabbiia |
⊢ { 𝑧 ∈ ℤ ∣ ( 𝑧 / 2 ) ∈ ℤ } = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) } |
28 |
1 27
|
eqtri |
⊢ Even = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) } |