Metamath Proof Explorer

Theorem gausslemma2dlem0i

Description: Auxiliary lemma 9 for gausslemma2d . (Contributed by AV, 14-Jul-2021)

Ref Expression
Hypotheses gausslemma2dlem0.p 
|- ( ph -> P e. ( Prime \ { 2 } ) )
gausslemma2dlem0.m 
|- M = ( |_ ` ( P / 4 ) )
gausslemma2dlem0.h 
|- H = ( ( P - 1 ) / 2 )
gausslemma2dlem0.n 
|- N = ( H - M )
Assertion gausslemma2dlem0i 
|- ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0.p 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 gausslemma2dlem0.m 
 |-  M = ( |_ ` ( P / 4 ) )
3 gausslemma2dlem0.h 
 |-  H = ( ( P - 1 ) / 2 )
4 gausslemma2dlem0.n 
 |-  N = ( H - M )
5 2z 
 |-  2 e. ZZ
6 id 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( Prime \ { 2 } ) )
7 6 gausslemma2dlem0a 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. NN )
8 7 nnzd 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ZZ )
9 1 8 syl 
 |-  ( ph -> P e. ZZ )
10 lgscl1 
 |-  ( ( 2 e. ZZ /\ P e. ZZ ) -> ( 2 /L P ) e. { -u 1 , 0 , 1 } )
11 5 9 10 sylancr 
 |-  ( ph -> ( 2 /L P ) e. { -u 1 , 0 , 1 } )
12 ovex 
 |-  ( 2 /L P ) e. _V
13 12 eltp 
 |-  ( ( 2 /L P ) e. { -u 1 , 0 , 1 } <-> ( ( 2 /L P ) = -u 1 \/ ( 2 /L P ) = 0 \/ ( 2 /L P ) = 1 ) )
14 1 2 3 4 gausslemma2dlem0h 
 |-  ( ph -> N e. NN0 )
15 14 nn0zd 
 |-  ( ph -> N e. ZZ )
16 m1expcl2 
 |-  ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } )
17 15 16 syl 
 |-  ( ph -> ( -u 1 ^ N ) e. { -u 1 , 1 } )
18 ovex 
 |-  ( -u 1 ^ N ) e. _V
19 18 elpr 
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } <-> ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) )
20 eqcom 
 |-  ( ( -u 1 ^ N ) = -u 1 <-> -u 1 = ( -u 1 ^ N ) )
21 20 biimpi 
 |-  ( ( -u 1 ^ N ) = -u 1 -> -u 1 = ( -u 1 ^ N ) )
22 21 2a1d 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) ) )
23 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
24 prmnn 
 |-  ( P e. Prime -> P e. NN )
25 24 nnred 
 |-  ( P e. Prime -> P e. RR )
26 prmgt1 
 |-  ( P e. Prime -> 1 < P )
27 25 26 jca 
 |-  ( P e. Prime -> ( P e. RR /\ 1 < P ) )
28 23 27 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. RR /\ 1 < P ) )
29 1mod 
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
30 1 28 29 3syl 
 |-  ( ph -> ( 1 mod P ) = 1 )
31 30 eqeq2d 
 |-  ( ph -> ( ( -u 1 mod P ) = ( 1 mod P ) <-> ( -u 1 mod P ) = 1 ) )
32 oddprmge3 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) )
33 m1modge3gt1 
 |-  ( P e. ( ZZ>= ` 3 ) -> 1 < ( -u 1 mod P ) )
34 breq2 
 |-  ( ( -u 1 mod P ) = 1 -> ( 1 < ( -u 1 mod P ) <-> 1 < 1 ) )
35 1re 
 |-  1 e. RR
36 35 ltnri 
 |-  -. 1 < 1
37 36 pm2.21i 
 |-  ( 1 < 1 -> -u 1 = 1 )
38 34 37 syl6bi 
 |-  ( ( -u 1 mod P ) = 1 -> ( 1 < ( -u 1 mod P ) -> -u 1 = 1 ) )
39 33 38 syl5com 
 |-  ( P e. ( ZZ>= ` 3 ) -> ( ( -u 1 mod P ) = 1 -> -u 1 = 1 ) )
40 1 32 39 3syl 
 |-  ( ph -> ( ( -u 1 mod P ) = 1 -> -u 1 = 1 ) )
41 31 40 sylbid 
 |-  ( ph -> ( ( -u 1 mod P ) = ( 1 mod P ) -> -u 1 = 1 ) )
42 oveq1 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 ^ N ) mod P ) = ( 1 mod P ) )
43 42 eqeq2d 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( -u 1 mod P ) = ( 1 mod P ) ) )
44 eqeq2 
 |-  ( ( -u 1 ^ N ) = 1 -> ( -u 1 = ( -u 1 ^ N ) <-> -u 1 = 1 ) )
45 43 44 imbi12d 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) <-> ( ( -u 1 mod P ) = ( 1 mod P ) -> -u 1 = 1 ) ) )
46 41 45 syl5ibr 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) ) )
47 22 46 jaoi 
 |-  ( ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) -> ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) ) )
48 19 47 sylbi 
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) ) )
49 17 48 mpcom 
 |-  ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) )
50 oveq1 
 |-  ( ( 2 /L P ) = -u 1 -> ( ( 2 /L P ) mod P ) = ( -u 1 mod P ) )
51 50 eqeq1d 
 |-  ( ( 2 /L P ) = -u 1 -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) ) )
52 eqeq1 
 |-  ( ( 2 /L P ) = -u 1 -> ( ( 2 /L P ) = ( -u 1 ^ N ) <-> -u 1 = ( -u 1 ^ N ) ) )
53 51 52 imbi12d 
 |-  ( ( 2 /L P ) = -u 1 -> ( ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) <-> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) ) )
54 49 53 syl5ibr 
 |-  ( ( 2 /L P ) = -u 1 -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
55 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
56 55 nnrpd 
 |-  ( ph -> P e. RR+ )
57 0mod 
 |-  ( P e. RR+ -> ( 0 mod P ) = 0 )
58 56 57 syl 
 |-  ( ph -> ( 0 mod P ) = 0 )
59 58 eqeq1d 
 |-  ( ph -> ( ( 0 mod P ) = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( ( -u 1 ^ N ) mod P ) ) )
60 oveq1 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ( -u 1 ^ N ) mod P ) = ( -u 1 mod P ) )
61 60 eqeq2d 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( -u 1 mod P ) ) )
62 61 adantr 
 |-  ( ( ( -u 1 ^ N ) = -u 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( -u 1 mod P ) ) )
63 negmod0 
 |-  ( ( 1 e. RR /\ P e. RR+ ) -> ( ( 1 mod P ) = 0 <-> ( -u 1 mod P ) = 0 ) )
64 eqcom 
 |-  ( ( -u 1 mod P ) = 0 <-> 0 = ( -u 1 mod P ) )
65 63 64 bitrdi 
 |-  ( ( 1 e. RR /\ P e. RR+ ) -> ( ( 1 mod P ) = 0 <-> 0 = ( -u 1 mod P ) ) )
66 35 56 65 sylancr 
 |-  ( ph -> ( ( 1 mod P ) = 0 <-> 0 = ( -u 1 mod P ) ) )
67 30 eqeq1d 
 |-  ( ph -> ( ( 1 mod P ) = 0 <-> 1 = 0 ) )
68 ax-1ne0 
 |-  1 =/= 0
69 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> 0 = ( -u 1 ^ N ) ) )
70 68 69 mpi 
 |-  ( 1 = 0 -> 0 = ( -u 1 ^ N ) )
71 67 70 syl6bi 
 |-  ( ph -> ( ( 1 mod P ) = 0 -> 0 = ( -u 1 ^ N ) ) )
72 66 71 sylbird 
 |-  ( ph -> ( 0 = ( -u 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
73 72 adantl 
 |-  ( ( ( -u 1 ^ N ) = -u 1 /\ ph ) -> ( 0 = ( -u 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
74 62 73 sylbid 
 |-  ( ( ( -u 1 ^ N ) = -u 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
75 74 ex 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
76 42 eqeq2d 
 |-  ( ( -u 1 ^ N ) = 1 -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( 1 mod P ) ) )
77 76 adantr 
 |-  ( ( ( -u 1 ^ N ) = 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( 1 mod P ) ) )
78 eqcom 
 |-  ( 0 = ( 1 mod P ) <-> ( 1 mod P ) = 0 )
79 78 67 syl5bb 
 |-  ( ph -> ( 0 = ( 1 mod P ) <-> 1 = 0 ) )
80 79 70 syl6bi 
 |-  ( ph -> ( 0 = ( 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
81 80 adantl 
 |-  ( ( ( -u 1 ^ N ) = 1 /\ ph ) -> ( 0 = ( 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
82 77 81 sylbid 
 |-  ( ( ( -u 1 ^ N ) = 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
83 82 ex 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
84 75 83 jaoi 
 |-  ( ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
85 19 84 sylbi 
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
86 17 85 mpcom 
 |-  ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
87 59 86 sylbid 
 |-  ( ph -> ( ( 0 mod P ) = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
88 oveq1 
 |-  ( ( 2 /L P ) = 0 -> ( ( 2 /L P ) mod P ) = ( 0 mod P ) )
89 88 eqeq1d 
 |-  ( ( 2 /L P ) = 0 -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( 0 mod P ) = ( ( -u 1 ^ N ) mod P ) ) )
90 eqeq1 
 |-  ( ( 2 /L P ) = 0 -> ( ( 2 /L P ) = ( -u 1 ^ N ) <-> 0 = ( -u 1 ^ N ) ) )
91 89 90 imbi12d 
 |-  ( ( 2 /L P ) = 0 -> ( ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) <-> ( ( 0 mod P ) = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
92 87 91 syl5ibr 
 |-  ( ( 2 /L P ) = 0 -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
93 30 eqeq1d 
 |-  ( ph -> ( ( 1 mod P ) = ( ( -u 1 ^ N ) mod P ) <-> 1 = ( ( -u 1 ^ N ) mod P ) ) )
94 eqcom 
 |-  ( 1 = ( -u 1 mod P ) <-> ( -u 1 mod P ) = 1 )
95 eqcom 
 |-  ( 1 = -u 1 <-> -u 1 = 1 )
96 40 94 95 3imtr4g 
 |-  ( ph -> ( 1 = ( -u 1 mod P ) -> 1 = -u 1 ) )
97 60 eqeq2d 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( 1 = ( ( -u 1 ^ N ) mod P ) <-> 1 = ( -u 1 mod P ) ) )
98 eqeq2 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( 1 = ( -u 1 ^ N ) <-> 1 = -u 1 ) )
99 97 98 imbi12d 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) <-> ( 1 = ( -u 1 mod P ) -> 1 = -u 1 ) ) )
100 96 99 syl5ibr 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
101 eqcom 
 |-  ( ( -u 1 ^ N ) = 1 <-> 1 = ( -u 1 ^ N ) )
102 101 biimpi 
 |-  ( ( -u 1 ^ N ) = 1 -> 1 = ( -u 1 ^ N ) )
103 102 2a1d 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
104 100 103 jaoi 
 |-  ( ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
105 19 104 sylbi 
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
106 17 105 mpcom 
 |-  ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) )
107 93 106 sylbid 
 |-  ( ph -> ( ( 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) )
108 oveq1 
 |-  ( ( 2 /L P ) = 1 -> ( ( 2 /L P ) mod P ) = ( 1 mod P ) )
109 108 eqeq1d 
 |-  ( ( 2 /L P ) = 1 -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( 1 mod P ) = ( ( -u 1 ^ N ) mod P ) ) )
110 eqeq1 
 |-  ( ( 2 /L P ) = 1 -> ( ( 2 /L P ) = ( -u 1 ^ N ) <-> 1 = ( -u 1 ^ N ) ) )
111 109 110 imbi12d 
 |-  ( ( 2 /L P ) = 1 -> ( ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) <-> ( ( 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
112 107 111 syl5ibr 
 |-  ( ( 2 /L P ) = 1 -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
113 54 92 112 3jaoi 
 |-  ( ( ( 2 /L P ) = -u 1 \/ ( 2 /L P ) = 0 \/ ( 2 /L P ) = 1 ) -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
114 13 113 sylbi 
 |-  ( ( 2 /L P ) e. { -u 1 , 0 , 1 } -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
115 11 114 mpcom 
 |-  ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )