Step |
Hyp |
Ref |
Expression |
1 |
|
odd2np1 |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = 𝑁 ) ) |
2 |
1
|
biimpa |
⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = 𝑁 ) |
3 |
|
eqcom |
⊢ ( ( ( 2 · 𝑘 ) + 1 ) = 𝑁 ↔ 𝑁 = ( ( 2 · 𝑘 ) + 1 ) ) |
4 |
|
sqoddm1div8 |
⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 = ( ( 2 · 𝑘 ) + 1 ) ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) = ( ( 𝑘 · ( 𝑘 + 1 ) ) / 2 ) ) |
5 |
4
|
adantll |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑁 = ( ( 2 · 𝑘 ) + 1 ) ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) = ( ( 𝑘 · ( 𝑘 + 1 ) ) / 2 ) ) |
6 |
|
mulsucdiv2z |
⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℤ ) |
7 |
6
|
ad2antlr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑁 = ( ( 2 · 𝑘 ) + 1 ) ) → ( ( 𝑘 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℤ ) |
8 |
5 7
|
eqeltrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑁 = ( ( 2 · 𝑘 ) + 1 ) ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ ) |
9 |
8
|
ex |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑁 = ( ( 2 · 𝑘 ) + 1 ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ ) ) |
10 |
3 9
|
syl5bi |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑘 ) + 1 ) = 𝑁 → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ ) ) |
11 |
10
|
rexlimdva |
⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = 𝑁 → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ ) ) |
12 |
2 11
|
mpd |
⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ ) |