Metamath Proof Explorer

Theorem 2lgsoddprmlem4

Description: Lemma 4 for 2lgsoddprm . (Contributed by AV, 20-Jul-2021)

Ref Expression
Assertion 2lgsoddprmlem4 
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> ( N mod 8 ) e. { 1 , 7 } ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( N mod 8 ) = ( N mod 8 ) )
2 2lgsoddprmlem2 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ ( N mod 8 ) = ( N mod 8 ) ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( ( N mod 8 ) ^ 2 ) - 1 ) / 8 ) ) )
3 1 2 mpd3an3 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( ( N mod 8 ) ^ 2 ) - 1 ) / 8 ) ) )
4 2lgsoddprmlem3 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ ( N mod 8 ) = ( N mod 8 ) ) -> ( 2 || ( ( ( ( N mod 8 ) ^ 2 ) - 1 ) / 8 ) <-> ( N mod 8 ) e. { 1 , 7 } ) )
5 1 4 mpd3an3 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( 2 || ( ( ( ( N mod 8 ) ^ 2 ) - 1 ) / 8 ) <-> ( N mod 8 ) e. { 1 , 7 } ) )
6 3 5 bitrd 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( 2 || ( ( ( N ^ 2 ) - 1 ) / 8 ) <-> ( N mod 8 ) e. { 1 , 7 } ) )