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 N¬2NN218

Proof

Step Hyp Ref Expression
1 odd2np1 N¬2Nk2k+1=N
2 1 biimpa N¬2Nk2k+1=N
3 eqcom 2k+1=NN=2k+1
4 sqoddm1div8 kN=2k+1N218=kk+12
5 4 adantll N¬2NkN=2k+1N218=kk+12
6 mulsucdiv2z kkk+12
7 6 ad2antlr N¬2NkN=2k+1kk+12
8 5 7 eqeltrd N¬2NkN=2k+1N218
9 8 ex N¬2NkN=2k+1N218
10 3 9 syl5bi N¬2Nk2k+1=NN218
11 10 rexlimdva N¬2Nk2k+1=NN218
12 2 11 mpd N¬2NN218