This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑘 ) + 1 ) = 𝑁 → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ ) )
11 10 rexlimdva ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = 𝑁 → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ ) )
12 2 11 mpd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ( 𝑁 ↑ 2 ) − 1 ) / 8 ) ∈ ℤ )