Step |
Hyp |
Ref |
Expression |
1 |
|
oddm1even |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) ) |
2 |
|
2z |
⊢ 2 ∈ ℤ |
3 |
|
peano2zm |
⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ ) |
4 |
|
dvdsadd |
⊢ ( ( 2 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ 2 ∥ ( 2 + ( 𝑁 − 1 ) ) ) ) |
5 |
2 3 4
|
sylancr |
⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 𝑁 − 1 ) ↔ 2 ∥ ( 2 + ( 𝑁 − 1 ) ) ) ) |
6 |
|
2cnd |
⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ ) |
7 |
|
zcn |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ ) |
8 |
|
1cnd |
⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℂ ) |
9 |
6 7 8
|
addsub12d |
⊢ ( 𝑁 ∈ ℤ → ( 2 + ( 𝑁 − 1 ) ) = ( 𝑁 + ( 2 − 1 ) ) ) |
10 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
11 |
10
|
oveq2i |
⊢ ( 𝑁 + ( 2 − 1 ) ) = ( 𝑁 + 1 ) |
12 |
9 11
|
eqtrdi |
⊢ ( 𝑁 ∈ ℤ → ( 2 + ( 𝑁 − 1 ) ) = ( 𝑁 + 1 ) ) |
13 |
12
|
breq2d |
⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 2 + ( 𝑁 − 1 ) ) ↔ 2 ∥ ( 𝑁 + 1 ) ) ) |
14 |
1 5 13
|
3bitrd |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) ) |