Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑁 ∈ ℤ ) |
2 |
1
|
zcnd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑁 ∈ ℂ ) |
3 |
|
1cnd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℂ ) |
4 |
|
2cnd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 2 ∈ ℂ ) |
5 |
|
simpr |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ ) |
6 |
5
|
zcnd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ ) |
7 |
4 6
|
mulcld |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) ∈ ℂ ) |
8 |
2 3 7
|
subadd2d |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑁 − 1 ) = ( 2 · 𝑛 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) |
9 |
|
eqcom |
⊢ ( ( 𝑁 − 1 ) = ( 2 · 𝑛 ) ↔ ( 2 · 𝑛 ) = ( 𝑁 − 1 ) ) |
10 |
4 6
|
mulcomd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) = ( 𝑛 · 2 ) ) |
11 |
10
|
eqeq1d |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 2 · 𝑛 ) = ( 𝑁 − 1 ) ↔ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) ) |
12 |
9 11
|
syl5bb |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑁 − 1 ) = ( 2 · 𝑛 ) ↔ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) ) |
13 |
8 12
|
bitr3d |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) ) |
14 |
13
|
rexbidva |
⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) ) |
15 |
|
odd2np1 |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) |
16 |
|
2z |
⊢ 2 ∈ ℤ |
17 |
|
peano2zm |
⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ ) |
18 |
|
divides |
⊢ ( ( 2 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) ) |
19 |
16 17 18
|
sylancr |
⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 𝑁 − 1 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = ( 𝑁 − 1 ) ) ) |
20 |
14 15 19
|
3bitr4d |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) ) |