Metamath Proof Explorer


Theorem sqoddm1div8z

Description: A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion sqoddm1div8z ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ )

Proof

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 ) ∈ ℤ )