Metamath Proof Explorer

Theorem 2lgsoddprmlem3

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

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

Proof

Step Hyp Ref Expression
1 lgsdir2lem3 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( N mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
2 eleq1 
 |-  ( ( N mod 8 ) = R -> ( ( N mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) <-> R e. ( { 1 , 7 } u. { 3 , 5 } ) ) )
3 2 eqcoms 
 |-  ( R = ( N mod 8 ) -> ( ( N mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) <-> R e. ( { 1 , 7 } u. { 3 , 5 } ) ) )
4 elun 
 |-  ( R e. ( { 1 , 7 } u. { 3 , 5 } ) <-> ( R e. { 1 , 7 } \/ R e. { 3 , 5 } ) )
5 elpri 
 |-  ( R e. { 3 , 5 } -> ( R = 3 \/ R = 5 ) )
6 oveq1 
 |-  ( R = 3 -> ( R ^ 2 ) = ( 3 ^ 2 ) )
7 6 oveq1d 
 |-  ( R = 3 -> ( ( R ^ 2 ) - 1 ) = ( ( 3 ^ 2 ) - 1 ) )
8 7 oveq1d 
 |-  ( R = 3 -> ( ( ( R ^ 2 ) - 1 ) / 8 ) = ( ( ( 3 ^ 2 ) - 1 ) / 8 ) )
9 2lgsoddprmlem3b 
 |-  ( ( ( 3 ^ 2 ) - 1 ) / 8 ) = 1
10 8 9 eqtrdi 
 |-  ( R = 3 -> ( ( ( R ^ 2 ) - 1 ) / 8 ) = 1 )
11 10 breq2d 
 |-  ( R = 3 -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> 2 || 1 ) )
12 n2dvds1 
 |-  -. 2 || 1
13 12 pm2.21i 
 |-  ( 2 || 1 -> R e. { 1 , 7 } )
14 11 13 biimtrdi 
 |-  ( R = 3 -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) -> R e. { 1 , 7 } ) )
15 oveq1 
 |-  ( R = 5 -> ( R ^ 2 ) = ( 5 ^ 2 ) )
16 15 oveq1d 
 |-  ( R = 5 -> ( ( R ^ 2 ) - 1 ) = ( ( 5 ^ 2 ) - 1 ) )
17 16 oveq1d 
 |-  ( R = 5 -> ( ( ( R ^ 2 ) - 1 ) / 8 ) = ( ( ( 5 ^ 2 ) - 1 ) / 8 ) )
18 17 breq2d 
 |-  ( R = 5 -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> 2 || ( ( ( 5 ^ 2 ) - 1 ) / 8 ) ) )
19 2lgsoddprmlem3c 
 |-  ( ( ( 5 ^ 2 ) - 1 ) / 8 ) = 3
20 19 breq2i 
 |-  ( 2 || ( ( ( 5 ^ 2 ) - 1 ) / 8 ) <-> 2 || 3 )
21 18 20 bitrdi 
 |-  ( R = 5 -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> 2 || 3 ) )
22 n2dvds3 
 |-  -. 2 || 3
23 22 pm2.21i 
 |-  ( 2 || 3 -> R e. { 1 , 7 } )
24 21 23 biimtrdi 
 |-  ( R = 5 -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) -> R e. { 1 , 7 } ) )
25 14 24 jaoi 
 |-  ( ( R = 3 \/ R = 5 ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) -> R e. { 1 , 7 } ) )
26 5 25 syl 
 |-  ( R e. { 3 , 5 } -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) -> R e. { 1 , 7 } ) )
27 26 jao1i 
 |-  ( ( R e. { 1 , 7 } \/ R e. { 3 , 5 } ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) -> R e. { 1 , 7 } ) )
28 4 27 sylbi 
 |-  ( R e. ( { 1 , 7 } u. { 3 , 5 } ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) -> R e. { 1 , 7 } ) )
29 elpri 
 |-  ( R e. { 1 , 7 } -> ( R = 1 \/ R = 7 ) )
30 z0even 
 |-  2 || 0
31 oveq1 
 |-  ( R = 1 -> ( R ^ 2 ) = ( 1 ^ 2 ) )
32 31 oveq1d 
 |-  ( R = 1 -> ( ( R ^ 2 ) - 1 ) = ( ( 1 ^ 2 ) - 1 ) )
33 32 oveq1d 
 |-  ( R = 1 -> ( ( ( R ^ 2 ) - 1 ) / 8 ) = ( ( ( 1 ^ 2 ) - 1 ) / 8 ) )
34 2lgsoddprmlem3a 
 |-  ( ( ( 1 ^ 2 ) - 1 ) / 8 ) = 0
35 33 34 eqtrdi 
 |-  ( R = 1 -> ( ( ( R ^ 2 ) - 1 ) / 8 ) = 0 )
36 30 35 breqtrrid 
 |-  ( R = 1 -> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) )
37 2z 
 |-  2 e. ZZ
38 3z 
 |-  3 e. ZZ
39 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ ) -> 2 || ( 2 x. 3 ) )
40 37 38 39 mp2an 
 |-  2 || ( 2 x. 3 )
41 oveq1 
 |-  ( R = 7 -> ( R ^ 2 ) = ( 7 ^ 2 ) )
42 41 oveq1d 
 |-  ( R = 7 -> ( ( R ^ 2 ) - 1 ) = ( ( 7 ^ 2 ) - 1 ) )
43 42 oveq1d 
 |-  ( R = 7 -> ( ( ( R ^ 2 ) - 1 ) / 8 ) = ( ( ( 7 ^ 2 ) - 1 ) / 8 ) )
44 2lgsoddprmlem3d 
 |-  ( ( ( 7 ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 )
45 43 44 eqtrdi 
 |-  ( R = 7 -> ( ( ( R ^ 2 ) - 1 ) / 8 ) = ( 2 x. 3 ) )
46 40 45 breqtrrid 
 |-  ( R = 7 -> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) )
47 36 46 jaoi 
 |-  ( ( R = 1 \/ R = 7 ) -> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) )
48 29 47 syl 
 |-  ( R e. { 1 , 7 } -> 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) )
49 28 48 impbid1 
 |-  ( R e. ( { 1 , 7 } u. { 3 , 5 } ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> R e. { 1 , 7 } ) )
50 3 49 biimtrdi 
 |-  ( R = ( N mod 8 ) -> ( ( N mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> R e. { 1 , 7 } ) ) )
51 1 50 syl5com 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( R = ( N mod 8 ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> R e. { 1 , 7 } ) ) )
52 51 3impia 
 |-  ( ( N e. ZZ /\ -. 2 || N /\ R = ( N mod 8 ) ) -> ( 2 || ( ( ( R ^ 2 ) - 1 ) / 8 ) <-> R e. { 1 , 7 } ) )