Step |
Hyp |
Ref |
Expression |
1 |
|
isodd |
⊢ ( 𝑍 ∈ Odd ↔ ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) |
2 |
|
zeo2 |
⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) |
3 |
2
|
biimpd |
⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 / 2 ) ∈ ℤ → ¬ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) |
4 |
3
|
con2d |
⊢ ( 𝑍 ∈ ℤ → ( ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ → ¬ ( 𝑍 / 2 ) ∈ ℤ ) ) |
5 |
4
|
imp |
⊢ ( ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) → ¬ ( 𝑍 / 2 ) ∈ ℤ ) |
6 |
1 5
|
sylbi |
⊢ ( 𝑍 ∈ Odd → ¬ ( 𝑍 / 2 ) ∈ ℤ ) |
7 |
6
|
olcd |
⊢ ( 𝑍 ∈ Odd → ( ¬ 𝑍 ∈ ℤ ∨ ¬ ( 𝑍 / 2 ) ∈ ℤ ) ) |
8 |
|
ianor |
⊢ ( ¬ ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) ↔ ( ¬ 𝑍 ∈ ℤ ∨ ¬ ( 𝑍 / 2 ) ∈ ℤ ) ) |
9 |
|
iseven |
⊢ ( 𝑍 ∈ Even ↔ ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) ) |
10 |
8 9
|
xchnxbir |
⊢ ( ¬ 𝑍 ∈ Even ↔ ( ¬ 𝑍 ∈ ℤ ∨ ¬ ( 𝑍 / 2 ) ∈ ℤ ) ) |
11 |
7 10
|
sylibr |
⊢ ( 𝑍 ∈ Odd → ¬ 𝑍 ∈ Even ) |