Metamath Proof Explorer

Theorem 2lgslem3

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

Ref Expression
Hypothesis 2lgslem2.n 
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
Assertion 2lgslem3 
|- ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )

Proof

Step Hyp Ref Expression
1 2lgslem2.n 
 |-  N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
2 nnz 
 |-  ( P e. NN -> P e. ZZ )
3 lgsdir2lem3 
 |-  ( ( P e. ZZ /\ -. 2 || P ) -> ( P mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
4 2 3 sylan 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( P mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
5 elun 
 |-  ( ( P mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) <-> ( ( P mod 8 ) e. { 1 , 7 } \/ ( P mod 8 ) e. { 3 , 5 } ) )
6 ovex 
 |-  ( P mod 8 ) e. _V
7 6 elpr 
 |-  ( ( P mod 8 ) e. { 1 , 7 } <-> ( ( P mod 8 ) = 1 \/ ( P mod 8 ) = 7 ) )
8 1 2lgslem3a1 
 |-  ( ( P e. NN /\ ( P mod 8 ) = 1 ) -> ( N mod 2 ) = 0 )
9 8 a1d 
 |-  ( ( P e. NN /\ ( P mod 8 ) = 1 ) -> ( -. 2 || P -> ( N mod 2 ) = 0 ) )
10 9 expcom 
 |-  ( ( P mod 8 ) = 1 -> ( P e. NN -> ( -. 2 || P -> ( N mod 2 ) = 0 ) ) )
11 10 impd 
 |-  ( ( P mod 8 ) = 1 -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = 0 ) )
12 1 2lgslem3d1 
 |-  ( ( P e. NN /\ ( P mod 8 ) = 7 ) -> ( N mod 2 ) = 0 )
13 12 a1d 
 |-  ( ( P e. NN /\ ( P mod 8 ) = 7 ) -> ( -. 2 || P -> ( N mod 2 ) = 0 ) )
14 13 expcom 
 |-  ( ( P mod 8 ) = 7 -> ( P e. NN -> ( -. 2 || P -> ( N mod 2 ) = 0 ) ) )
15 14 impd 
 |-  ( ( P mod 8 ) = 7 -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = 0 ) )
16 11 15 jaoi 
 |-  ( ( ( P mod 8 ) = 1 \/ ( P mod 8 ) = 7 ) -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = 0 ) )
17 7 16 sylbi 
 |-  ( ( P mod 8 ) e. { 1 , 7 } -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = 0 ) )
18 17 imp 
 |-  ( ( ( P mod 8 ) e. { 1 , 7 } /\ ( P e. NN /\ -. 2 || P ) ) -> ( N mod 2 ) = 0 )
19 iftrue 
 |-  ( ( P mod 8 ) e. { 1 , 7 } -> if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 )
20 19 adantr 
 |-  ( ( ( P mod 8 ) e. { 1 , 7 } /\ ( P e. NN /\ -. 2 || P ) ) -> if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 )
21 18 20 eqtr4d 
 |-  ( ( ( P mod 8 ) e. { 1 , 7 } /\ ( P e. NN /\ -. 2 || P ) ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )
22 21 ex 
 |-  ( ( P mod 8 ) e. { 1 , 7 } -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) ) )
23 6 elpr 
 |-  ( ( P mod 8 ) e. { 3 , 5 } <-> ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) )
24 1 2lgslem3b1 
 |-  ( ( P e. NN /\ ( P mod 8 ) = 3 ) -> ( N mod 2 ) = 1 )
25 24 expcom 
 |-  ( ( P mod 8 ) = 3 -> ( P e. NN -> ( N mod 2 ) = 1 ) )
26 1 2lgslem3c1 
 |-  ( ( P e. NN /\ ( P mod 8 ) = 5 ) -> ( N mod 2 ) = 1 )
27 26 expcom 
 |-  ( ( P mod 8 ) = 5 -> ( P e. NN -> ( N mod 2 ) = 1 ) )
28 25 27 jaoi 
 |-  ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) -> ( P e. NN -> ( N mod 2 ) = 1 ) )
29 28 imp 
 |-  ( ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) /\ P e. NN ) -> ( N mod 2 ) = 1 )
30 1re 
 |-  1 e. RR
31 1lt3 
 |-  1 < 3
32 30 31 ltneii 
 |-  1 =/= 3
33 32 nesymi 
 |-  -. 3 = 1
34 3re 
 |-  3 e. RR
35 3lt7 
 |-  3 < 7
36 34 35 ltneii 
 |-  3 =/= 7
37 36 neii 
 |-  -. 3 = 7
38 33 37 pm3.2i 
 |-  ( -. 3 = 1 /\ -. 3 = 7 )
39 eqeq1 
 |-  ( ( P mod 8 ) = 3 -> ( ( P mod 8 ) = 1 <-> 3 = 1 ) )
40 39 notbid 
 |-  ( ( P mod 8 ) = 3 -> ( -. ( P mod 8 ) = 1 <-> -. 3 = 1 ) )
41 eqeq1 
 |-  ( ( P mod 8 ) = 3 -> ( ( P mod 8 ) = 7 <-> 3 = 7 ) )
42 41 notbid 
 |-  ( ( P mod 8 ) = 3 -> ( -. ( P mod 8 ) = 7 <-> -. 3 = 7 ) )
43 40 42 anbi12d 
 |-  ( ( P mod 8 ) = 3 -> ( ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) <-> ( -. 3 = 1 /\ -. 3 = 7 ) ) )
44 38 43 mpbiri 
 |-  ( ( P mod 8 ) = 3 -> ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) )
45 1lt5 
 |-  1 < 5
46 30 45 ltneii 
 |-  1 =/= 5
47 46 nesymi 
 |-  -. 5 = 1
48 5re 
 |-  5 e. RR
49 5lt7 
 |-  5 < 7
50 48 49 ltneii 
 |-  5 =/= 7
51 50 neii 
 |-  -. 5 = 7
52 47 51 pm3.2i 
 |-  ( -. 5 = 1 /\ -. 5 = 7 )
53 eqeq1 
 |-  ( ( P mod 8 ) = 5 -> ( ( P mod 8 ) = 1 <-> 5 = 1 ) )
54 53 notbid 
 |-  ( ( P mod 8 ) = 5 -> ( -. ( P mod 8 ) = 1 <-> -. 5 = 1 ) )
55 eqeq1 
 |-  ( ( P mod 8 ) = 5 -> ( ( P mod 8 ) = 7 <-> 5 = 7 ) )
56 55 notbid 
 |-  ( ( P mod 8 ) = 5 -> ( -. ( P mod 8 ) = 7 <-> -. 5 = 7 ) )
57 54 56 anbi12d 
 |-  ( ( P mod 8 ) = 5 -> ( ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) <-> ( -. 5 = 1 /\ -. 5 = 7 ) ) )
58 52 57 mpbiri 
 |-  ( ( P mod 8 ) = 5 -> ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) )
59 44 58 jaoi 
 |-  ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) -> ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) )
60 59 adantr 
 |-  ( ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) /\ P e. NN ) -> ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) )
61 ioran 
 |-  ( -. ( ( P mod 8 ) = 1 \/ ( P mod 8 ) = 7 ) <-> ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) )
62 61 7 xchnxbir 
 |-  ( -. ( P mod 8 ) e. { 1 , 7 } <-> ( -. ( P mod 8 ) = 1 /\ -. ( P mod 8 ) = 7 ) )
63 60 62 sylibr 
 |-  ( ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) /\ P e. NN ) -> -. ( P mod 8 ) e. { 1 , 7 } )
64 63 iffalsed 
 |-  ( ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) /\ P e. NN ) -> if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 1 )
65 29 64 eqtr4d 
 |-  ( ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) /\ P e. NN ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )
66 65 a1d 
 |-  ( ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) /\ P e. NN ) -> ( -. 2 || P -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) ) )
67 66 expimpd 
 |-  ( ( ( P mod 8 ) = 3 \/ ( P mod 8 ) = 5 ) -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) ) )
68 23 67 sylbi 
 |-  ( ( P mod 8 ) e. { 3 , 5 } -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) ) )
69 22 68 jaoi 
 |-  ( ( ( P mod 8 ) e. { 1 , 7 } \/ ( P mod 8 ) e. { 3 , 5 } ) -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) ) )
70 5 69 sylbi 
 |-  ( ( P mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) -> ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) ) )
71 4 70 mpcom 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( N mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )