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 1mod
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
29 1 23 27 28 4syl
 |-  ( ph -> ( 1 mod P ) = 1 )
30 29 eqeq2d
 |-  ( ph -> ( ( -u 1 mod P ) = ( 1 mod P ) <-> ( -u 1 mod P ) = 1 ) )
31 oddprmge3
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) )
32 m1modge3gt1
 |-  ( P e. ( ZZ>= ` 3 ) -> 1 < ( -u 1 mod P ) )
33 breq2
 |-  ( ( -u 1 mod P ) = 1 -> ( 1 < ( -u 1 mod P ) <-> 1 < 1 ) )
34 1re
 |-  1 e. RR
35 34 ltnri
 |-  -. 1 < 1
36 35 pm2.21i
 |-  ( 1 < 1 -> -u 1 = 1 )
37 33 36 biimtrdi
 |-  ( ( -u 1 mod P ) = 1 -> ( 1 < ( -u 1 mod P ) -> -u 1 = 1 ) )
38 32 37 syl5com
 |-  ( P e. ( ZZ>= ` 3 ) -> ( ( -u 1 mod P ) = 1 -> -u 1 = 1 ) )
39 1 31 38 3syl
 |-  ( ph -> ( ( -u 1 mod P ) = 1 -> -u 1 = 1 ) )
40 30 39 sylbid
 |-  ( ph -> ( ( -u 1 mod P ) = ( 1 mod P ) -> -u 1 = 1 ) )
41 oveq1
 |-  ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 ^ N ) mod P ) = ( 1 mod P ) )
42 41 eqeq2d
 |-  ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( -u 1 mod P ) = ( 1 mod P ) ) )
43 eqeq2
 |-  ( ( -u 1 ^ N ) = 1 -> ( -u 1 = ( -u 1 ^ N ) <-> -u 1 = 1 ) )
44 42 43 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 ) ) )
45 40 44 imbitrrid
 |-  ( ( -u 1 ^ N ) = 1 -> ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) ) )
46 22 45 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 ) ) ) )
47 19 46 sylbi
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) ) )
48 17 47 mpcom
 |-  ( ph -> ( ( -u 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> -u 1 = ( -u 1 ^ N ) ) )
49 oveq1
 |-  ( ( 2 /L P ) = -u 1 -> ( ( 2 /L P ) mod P ) = ( -u 1 mod P ) )
50 49 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 ) ) )
51 eqeq1
 |-  ( ( 2 /L P ) = -u 1 -> ( ( 2 /L P ) = ( -u 1 ^ N ) <-> -u 1 = ( -u 1 ^ N ) ) )
52 50 51 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 ) ) ) )
53 48 52 imbitrrid
 |-  ( ( 2 /L P ) = -u 1 -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
54 1 gausslemma2dlem0a
 |-  ( ph -> P e. NN )
55 54 nnrpd
 |-  ( ph -> P e. RR+ )
56 0mod
 |-  ( P e. RR+ -> ( 0 mod P ) = 0 )
57 55 56 syl
 |-  ( ph -> ( 0 mod P ) = 0 )
58 57 eqeq1d
 |-  ( ph -> ( ( 0 mod P ) = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( ( -u 1 ^ N ) mod P ) ) )
59 oveq1
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ( -u 1 ^ N ) mod P ) = ( -u 1 mod P ) )
60 59 eqeq2d
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( -u 1 mod P ) ) )
61 60 adantr
 |-  ( ( ( -u 1 ^ N ) = -u 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( -u 1 mod P ) ) )
62 negmod0
 |-  ( ( 1 e. RR /\ P e. RR+ ) -> ( ( 1 mod P ) = 0 <-> ( -u 1 mod P ) = 0 ) )
63 eqcom
 |-  ( ( -u 1 mod P ) = 0 <-> 0 = ( -u 1 mod P ) )
64 62 63 bitrdi
 |-  ( ( 1 e. RR /\ P e. RR+ ) -> ( ( 1 mod P ) = 0 <-> 0 = ( -u 1 mod P ) ) )
65 34 55 64 sylancr
 |-  ( ph -> ( ( 1 mod P ) = 0 <-> 0 = ( -u 1 mod P ) ) )
66 29 eqeq1d
 |-  ( ph -> ( ( 1 mod P ) = 0 <-> 1 = 0 ) )
67 ax-1ne0
 |-  1 =/= 0
68 eqneqall
 |-  ( 1 = 0 -> ( 1 =/= 0 -> 0 = ( -u 1 ^ N ) ) )
69 67 68 mpi
 |-  ( 1 = 0 -> 0 = ( -u 1 ^ N ) )
70 66 69 biimtrdi
 |-  ( ph -> ( ( 1 mod P ) = 0 -> 0 = ( -u 1 ^ N ) ) )
71 65 70 sylbird
 |-  ( ph -> ( 0 = ( -u 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
72 71 adantl
 |-  ( ( ( -u 1 ^ N ) = -u 1 /\ ph ) -> ( 0 = ( -u 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
73 61 72 sylbid
 |-  ( ( ( -u 1 ^ N ) = -u 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
74 73 ex
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
75 41 eqeq2d
 |-  ( ( -u 1 ^ N ) = 1 -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( 1 mod P ) ) )
76 75 adantr
 |-  ( ( ( -u 1 ^ N ) = 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) <-> 0 = ( 1 mod P ) ) )
77 eqcom
 |-  ( 0 = ( 1 mod P ) <-> ( 1 mod P ) = 0 )
78 77 66 bitrid
 |-  ( ph -> ( 0 = ( 1 mod P ) <-> 1 = 0 ) )
79 78 69 biimtrdi
 |-  ( ph -> ( 0 = ( 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
80 79 adantl
 |-  ( ( ( -u 1 ^ N ) = 1 /\ ph ) -> ( 0 = ( 1 mod P ) -> 0 = ( -u 1 ^ N ) ) )
81 76 80 sylbid
 |-  ( ( ( -u 1 ^ N ) = 1 /\ ph ) -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
82 81 ex
 |-  ( ( -u 1 ^ N ) = 1 -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
83 74 82 jaoi
 |-  ( ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
84 19 83 sylbi
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) ) )
85 17 84 mpcom
 |-  ( ph -> ( 0 = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
86 58 85 sylbid
 |-  ( ph -> ( ( 0 mod P ) = ( ( -u 1 ^ N ) mod P ) -> 0 = ( -u 1 ^ N ) ) )
87 oveq1
 |-  ( ( 2 /L P ) = 0 -> ( ( 2 /L P ) mod P ) = ( 0 mod P ) )
88 87 eqeq1d
 |-  ( ( 2 /L P ) = 0 -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( 0 mod P ) = ( ( -u 1 ^ N ) mod P ) ) )
89 eqeq1
 |-  ( ( 2 /L P ) = 0 -> ( ( 2 /L P ) = ( -u 1 ^ N ) <-> 0 = ( -u 1 ^ N ) ) )
90 88 89 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 ) ) ) )
91 86 90 imbitrrid
 |-  ( ( 2 /L P ) = 0 -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
92 29 eqeq1d
 |-  ( ph -> ( ( 1 mod P ) = ( ( -u 1 ^ N ) mod P ) <-> 1 = ( ( -u 1 ^ N ) mod P ) ) )
93 eqcom
 |-  ( 1 = ( -u 1 mod P ) <-> ( -u 1 mod P ) = 1 )
94 eqcom
 |-  ( 1 = -u 1 <-> -u 1 = 1 )
95 39 93 94 3imtr4g
 |-  ( ph -> ( 1 = ( -u 1 mod P ) -> 1 = -u 1 ) )
96 59 eqeq2d
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( 1 = ( ( -u 1 ^ N ) mod P ) <-> 1 = ( -u 1 mod P ) ) )
97 eqeq2
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( 1 = ( -u 1 ^ N ) <-> 1 = -u 1 ) )
98 96 97 imbi12d
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) <-> ( 1 = ( -u 1 mod P ) -> 1 = -u 1 ) ) )
99 95 98 imbitrrid
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
100 eqcom
 |-  ( ( -u 1 ^ N ) = 1 <-> 1 = ( -u 1 ^ N ) )
101 100 biimpi
 |-  ( ( -u 1 ^ N ) = 1 -> 1 = ( -u 1 ^ N ) )
102 101 2a1d
 |-  ( ( -u 1 ^ N ) = 1 -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
103 99 102 jaoi
 |-  ( ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
104 19 103 sylbi
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) ) )
105 17 104 mpcom
 |-  ( ph -> ( 1 = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) )
106 92 105 sylbid
 |-  ( ph -> ( ( 1 mod P ) = ( ( -u 1 ^ N ) mod P ) -> 1 = ( -u 1 ^ N ) ) )
107 oveq1
 |-  ( ( 2 /L P ) = 1 -> ( ( 2 /L P ) mod P ) = ( 1 mod P ) )
108 107 eqeq1d
 |-  ( ( 2 /L P ) = 1 -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( 1 mod P ) = ( ( -u 1 ^ N ) mod P ) ) )
109 eqeq1
 |-  ( ( 2 /L P ) = 1 -> ( ( 2 /L P ) = ( -u 1 ^ N ) <-> 1 = ( -u 1 ^ N ) ) )
110 108 109 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 ) ) ) )
111 106 110 imbitrrid
 |-  ( ( 2 /L P ) = 1 -> ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) ) )
112 53 91 111 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 ) ) ) )
113 13 112 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 ) ) ) )
114 11 113 mpcom
 |-  ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )