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 e. ZZ /\ -. 2 || N ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) e. ZZ )

Proof

Step Hyp Ref Expression
1 odd2np1 
 |-  ( N e. ZZ -> ( -. 2 || N <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = N ) )
2 1 biimpa 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> E. k e. ZZ ( ( 2 x. k ) + 1 ) = N )
3 eqcom 
 |-  ( ( ( 2 x. k ) + 1 ) = N <-> N = ( ( 2 x. k ) + 1 ) )
4 sqoddm1div8 
 |-  ( ( k e. ZZ /\ N = ( ( 2 x. k ) + 1 ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( k x. ( k + 1 ) ) / 2 ) )
5 4 adantll 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N ) /\ k e. ZZ ) /\ N = ( ( 2 x. k ) + 1 ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) = ( ( k x. ( k + 1 ) ) / 2 ) )
6 mulsucdiv2z 
 |-  ( k e. ZZ -> ( ( k x. ( k + 1 ) ) / 2 ) e. ZZ )
7 6 ad2antlr 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N ) /\ k e. ZZ ) /\ N = ( ( 2 x. k ) + 1 ) ) -> ( ( k x. ( k + 1 ) ) / 2 ) e. ZZ )
8 5 7 eqeltrd 
 |-  ( ( ( ( N e. ZZ /\ -. 2 || N ) /\ k e. ZZ ) /\ N = ( ( 2 x. k ) + 1 ) ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) e. ZZ )
9 8 ex 
 |-  ( ( ( N e. ZZ /\ -. 2 || N ) /\ k e. ZZ ) -> ( N = ( ( 2 x. k ) + 1 ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) e. ZZ ) )
10 3 9 syl5bi 
 |-  ( ( ( N e. ZZ /\ -. 2 || N ) /\ k e. ZZ ) -> ( ( ( 2 x. k ) + 1 ) = N -> ( ( ( N ^ 2 ) - 1 ) / 8 ) e. ZZ ) )
11 10 rexlimdva 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( E. k e. ZZ ( ( 2 x. k ) + 1 ) = N -> ( ( ( N ^ 2 ) - 1 ) / 8 ) e. ZZ ) )
12 2 11 mpd 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) e. ZZ )