Metamath Proof Explorer


Theorem gausslemma2dlem0i

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

Ref Expression
Hypotheses gausslemma2dlem0.p φP2
gausslemma2dlem0.m M=P4
gausslemma2dlem0.h H=P12
gausslemma2dlem0.n N=HM
Assertion gausslemma2dlem0i φ2/LPmodP=1NmodP2/LP=1N

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0.p φP2
2 gausslemma2dlem0.m M=P4
3 gausslemma2dlem0.h H=P12
4 gausslemma2dlem0.n N=HM
5 2z 2
6 id P2P2
7 6 gausslemma2dlem0a P2P
8 7 nnzd P2P
9 1 8 syl φP
10 lgscl1 2P2/LP101
11 5 9 10 sylancr φ2/LP101
12 ovex 2/LPV
13 12 eltp 2/LP1012/LP=12/LP=02/LP=1
14 1 2 3 4 gausslemma2dlem0h φN0
15 14 nn0zd φN
16 m1expcl2 N1N11
17 15 16 syl φ1N11
18 ovex 1NV
19 18 elpr 1N111N=11N=1
20 eqcom 1N=11=1N
21 20 biimpi 1N=11=1N
22 21 2a1d 1N=1φ-1modP=1NmodP1=1N
23 eldifi P2P
24 prmnn PP
25 24 nnred PP
26 prmgt1 P1<P
27 25 26 jca PP1<P
28 23 27 syl P2P1<P
29 1mod P1<P1modP=1
30 1 28 29 3syl φ1modP=1
31 30 eqeq2d φ-1modP=1modP-1modP=1
32 oddprmge3 P2P3
33 m1modge3gt1 P31<-1modP
34 breq2 -1modP=11<-1modP1<1
35 1re 1
36 35 ltnri ¬1<1
37 36 pm2.21i 1<11=1
38 34 37 syl6bi -1modP=11<-1modP1=1
39 33 38 syl5com P3-1modP=11=1
40 1 32 39 3syl φ-1modP=11=1
41 31 40 sylbid φ-1modP=1modP1=1
42 oveq1 1N=11NmodP=1modP
43 42 eqeq2d 1N=1-1modP=1NmodP-1modP=1modP
44 eqeq2 1N=11=1N1=1
45 43 44 imbi12d 1N=1-1modP=1NmodP1=1N-1modP=1modP1=1
46 41 45 syl5ibr 1N=1φ-1modP=1NmodP1=1N
47 22 46 jaoi 1N=11N=1φ-1modP=1NmodP1=1N
48 19 47 sylbi 1N11φ-1modP=1NmodP1=1N
49 17 48 mpcom φ-1modP=1NmodP1=1N
50 oveq1 2/LP=12/LPmodP=-1modP
51 50 eqeq1d 2/LP=12/LPmodP=1NmodP-1modP=1NmodP
52 eqeq1 2/LP=12/LP=1N1=1N
53 51 52 imbi12d 2/LP=12/LPmodP=1NmodP2/LP=1N-1modP=1NmodP1=1N
54 49 53 syl5ibr 2/LP=1φ2/LPmodP=1NmodP2/LP=1N
55 1 gausslemma2dlem0a φP
56 55 nnrpd φP+
57 0mod P+0modP=0
58 56 57 syl φ0modP=0
59 58 eqeq1d φ0modP=1NmodP0=1NmodP
60 oveq1 1N=11NmodP=-1modP
61 60 eqeq2d 1N=10=1NmodP0=-1modP
62 61 adantr 1N=1φ0=1NmodP0=-1modP
63 negmod0 1P+1modP=0-1modP=0
64 eqcom -1modP=00=-1modP
65 63 64 bitrdi 1P+1modP=00=-1modP
66 35 56 65 sylancr φ1modP=00=-1modP
67 30 eqeq1d φ1modP=01=0
68 ax-1ne0 10
69 eqneqall 1=0100=1N
70 68 69 mpi 1=00=1N
71 67 70 syl6bi φ1modP=00=1N
72 66 71 sylbird φ0=-1modP0=1N
73 72 adantl 1N=1φ0=-1modP0=1N
74 62 73 sylbid 1N=1φ0=1NmodP0=1N
75 74 ex 1N=1φ0=1NmodP0=1N
76 42 eqeq2d 1N=10=1NmodP0=1modP
77 76 adantr 1N=1φ0=1NmodP0=1modP
78 eqcom 0=1modP1modP=0
79 78 67 syl5bb φ0=1modP1=0
80 79 70 syl6bi φ0=1modP0=1N
81 80 adantl 1N=1φ0=1modP0=1N
82 77 81 sylbid 1N=1φ0=1NmodP0=1N
83 82 ex 1N=1φ0=1NmodP0=1N
84 75 83 jaoi 1N=11N=1φ0=1NmodP0=1N
85 19 84 sylbi 1N11φ0=1NmodP0=1N
86 17 85 mpcom φ0=1NmodP0=1N
87 59 86 sylbid φ0modP=1NmodP0=1N
88 oveq1 2/LP=02/LPmodP=0modP
89 88 eqeq1d 2/LP=02/LPmodP=1NmodP0modP=1NmodP
90 eqeq1 2/LP=02/LP=1N0=1N
91 89 90 imbi12d 2/LP=02/LPmodP=1NmodP2/LP=1N0modP=1NmodP0=1N
92 87 91 syl5ibr 2/LP=0φ2/LPmodP=1NmodP2/LP=1N
93 30 eqeq1d φ1modP=1NmodP1=1NmodP
94 eqcom 1=-1modP-1modP=1
95 eqcom 1=11=1
96 40 94 95 3imtr4g φ1=-1modP1=1
97 60 eqeq2d 1N=11=1NmodP1=-1modP
98 eqeq2 1N=11=1N1=1
99 97 98 imbi12d 1N=11=1NmodP1=1N1=-1modP1=1
100 96 99 syl5ibr 1N=1φ1=1NmodP1=1N
101 eqcom 1N=11=1N
102 101 biimpi 1N=11=1N
103 102 2a1d 1N=1φ1=1NmodP1=1N
104 100 103 jaoi 1N=11N=1φ1=1NmodP1=1N
105 19 104 sylbi 1N11φ1=1NmodP1=1N
106 17 105 mpcom φ1=1NmodP1=1N
107 93 106 sylbid φ1modP=1NmodP1=1N
108 oveq1 2/LP=12/LPmodP=1modP
109 108 eqeq1d 2/LP=12/LPmodP=1NmodP1modP=1NmodP
110 eqeq1 2/LP=12/LP=1N1=1N
111 109 110 imbi12d 2/LP=12/LPmodP=1NmodP2/LP=1N1modP=1NmodP1=1N
112 107 111 syl5ibr 2/LP=1φ2/LPmodP=1NmodP2/LP=1N
113 54 92 112 3jaoi 2/LP=12/LP=02/LP=1φ2/LPmodP=1NmodP2/LP=1N
114 13 113 sylbi 2/LP101φ2/LPmodP=1NmodP2/LP=1N
115 11 114 mpcom φ2/LPmodP=1NmodP2/LP=1N