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