Metamath Proof Explorer


Theorem gausslemma2dlem0i

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

Ref Expression
Hypotheses gausslemma2dlem0.p φ P 2
gausslemma2dlem0.m M = P 4
gausslemma2dlem0.h H = P 1 2
gausslemma2dlem0.n N = H M
Assertion gausslemma2dlem0i φ 2 / L P mod P = 1 N mod P 2 / L P = 1 N

Proof

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