Metamath Proof Explorer

Theorem lgseisen

Description: Eisenstein's lemma, an expression for ( P /L Q ) when P , Q are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 
|- ( ph -> P e. ( Prime \ { 2 } ) )
lgseisen.2 
|- ( ph -> Q e. ( Prime \ { 2 } ) )
lgseisen.3 
|- ( ph -> P =/= Q )
Assertion lgseisen 
|- ( ph -> ( Q /L P ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 lgseisen.2 
 |-  ( ph -> Q e. ( Prime \ { 2 } ) )
3 lgseisen.3 
 |-  ( ph -> P =/= Q )
4 2 eldifad 
 |-  ( ph -> Q e. Prime )
5 prmz 
 |-  ( Q e. Prime -> Q e. ZZ )
6 4 5 syl 
 |-  ( ph -> Q e. ZZ )
7 lgsval3 
 |-  ( ( Q e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( Q /L P ) = ( ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) )
8 6 1 7 syl2anc 
 |-  ( ph -> ( Q /L P ) = ( ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) )
9 2 gausslemma2dlem0a 
 |-  ( ph -> Q e. NN )
10 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
11 1 10 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN )
12 11 nnnn0d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
13 9 12 nnexpcld 
 |-  ( ph -> ( Q ^ ( ( P - 1 ) / 2 ) ) e. NN )
14 13 nnred 
 |-  ( ph -> ( Q ^ ( ( P - 1 ) / 2 ) ) e. RR )
15 neg1rr 
 |-  -u 1 e. RR
16 15 a1i 
 |-  ( ph -> -u 1 e. RR )
17 neg1ne0 
 |-  -u 1 =/= 0
18 17 a1i 
 |-  ( ph -> -u 1 =/= 0 )
19 fzfid 
 |-  ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin )
20 9 nnred 
 |-  ( ph -> Q e. RR )
21 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
22 20 21 nndivred 
 |-  ( ph -> ( Q / P ) e. RR )
23 22 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q / P ) e. RR )
24 2re 
 |-  2 e. RR
25 elfznn 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
26 25 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. NN )
27 26 nnred 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. RR )
28 remulcl 
 |-  ( ( 2 e. RR /\ x e. RR ) -> ( 2 x. x ) e. RR )
29 24 27 28 sylancr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. RR )
30 23 29 remulcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q / P ) x. ( 2 x. x ) ) e. RR )
31 30 flcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ )
32 19 31 fsumzcl 
 |-  ( ph -> sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ )
33 16 18 32 reexpclzd 
 |-  ( ph -> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. RR )
34 1re 
 |-  1 e. RR
35 34 a1i 
 |-  ( ph -> 1 e. RR )
36 21 nnrpd 
 |-  ( ph -> P e. RR+ )
37 eqid 
 |-  ( ( Q x. ( 2 x. x ) ) mod P ) = ( ( Q x. ( 2 x. x ) ) mod P )
38 eqid 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ ( ( Q x. ( 2 x. x ) ) mod P ) ) x. ( ( Q x. ( 2 x. x ) ) mod P ) ) mod P ) / 2 ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ ( ( Q x. ( 2 x. x ) ) mod P ) ) x. ( ( Q x. ( 2 x. x ) ) mod P ) ) mod P ) / 2 ) )
39 eqid 
 |-  ( ( Q x. ( 2 x. y ) ) mod P ) = ( ( Q x. ( 2 x. y ) ) mod P )
40 eqid 
 |-  ( Z/nZ ` P ) = ( Z/nZ ` P )
41 eqid 
 |-  ( mulGrp ` ( Z/nZ ` P ) ) = ( mulGrp ` ( Z/nZ ` P ) )
42 eqid 
 |-  ( ZRHom ` ( Z/nZ ` P ) ) = ( ZRHom ` ( Z/nZ ` P ) )
43 1 2 3 37 38 39 40 41 42 lgseisenlem4 
 |-  ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) )
44 modadd1 
 |-  ( ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) e. RR /\ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. RR ) /\ ( 1 e. RR /\ P e. RR+ ) /\ ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) ) -> ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) mod P ) )
45 14 33 35 36 43 44 syl221anc 
 |-  ( ph -> ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) mod P ) )
46 peano2re 
 |-  ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. RR -> ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) e. RR )
47 33 46 syl 
 |-  ( ph -> ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) e. RR )
48 df-neg 
 |-  -u 1 = ( 0 - 1 )
49 neg1cn 
 |-  -u 1 e. CC
50 absexpz 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ ) -> ( abs ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = ( ( abs ` -u 1 ) ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
51 49 17 32 50 mp3an12i 
 |-  ( ph -> ( abs ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = ( ( abs ` -u 1 ) ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
52 ax-1cn 
 |-  1 e. CC
53 52 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
54 abs1 
 |-  ( abs ` 1 ) = 1
55 53 54 eqtri 
 |-  ( abs ` -u 1 ) = 1
56 55 oveq1i 
 |-  ( ( abs ` -u 1 ) ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = ( 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) )
57 1exp 
 |-  ( sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ -> ( 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = 1 )
58 32 57 syl 
 |-  ( ph -> ( 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = 1 )
59 56 58 eqtrid 
 |-  ( ph -> ( ( abs ` -u 1 ) ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = 1 )
60 51 59 eqtrd 
 |-  ( ph -> ( abs ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = 1 )
61 1le1 
 |-  1 <_ 1
62 60 61 eqbrtrdi 
 |-  ( ph -> ( abs ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) <_ 1 )
63 absle 
 |-  ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) <_ 1 <-> ( -u 1 <_ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) /\ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) <_ 1 ) ) )
64 33 34 63 sylancl 
 |-  ( ph -> ( ( abs ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) <_ 1 <-> ( -u 1 <_ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) /\ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) <_ 1 ) ) )
65 62 64 mpbid 
 |-  ( ph -> ( -u 1 <_ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) /\ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) <_ 1 ) )
66 65 simpld 
 |-  ( ph -> -u 1 <_ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
67 48 66 eqbrtrrid 
 |-  ( ph -> ( 0 - 1 ) <_ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
68 0red 
 |-  ( ph -> 0 e. RR )
69 68 35 33 lesubaddd 
 |-  ( ph -> ( ( 0 - 1 ) <_ ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) <-> 0 <_ ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) ) )
70 67 69 mpbid 
 |-  ( ph -> 0 <_ ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) )
71 21 nnred 
 |-  ( ph -> P e. RR )
72 peano2rem 
 |-  ( P e. RR -> ( P - 1 ) e. RR )
73 71 72 syl 
 |-  ( ph -> ( P - 1 ) e. RR )
74 65 simprd 
 |-  ( ph -> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) <_ 1 )
75 df-2 
 |-  2 = ( 1 + 1 )
76 24 a1i 
 |-  ( ph -> 2 e. RR )
77 1 eldifad 
 |-  ( ph -> P e. Prime )
78 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
79 eluzle 
 |-  ( P e. ( ZZ>= ` 2 ) -> 2 <_ P )
80 77 78 79 3syl 
 |-  ( ph -> 2 <_ P )
81 eldifsni 
 |-  ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
82 1 81 syl 
 |-  ( ph -> P =/= 2 )
83 76 71 80 82 leneltd 
 |-  ( ph -> 2 < P )
84 75 83 eqbrtrrid 
 |-  ( ph -> ( 1 + 1 ) < P )
85 35 35 71 ltaddsubd 
 |-  ( ph -> ( ( 1 + 1 ) < P <-> 1 < ( P - 1 ) ) )
86 84 85 mpbid 
 |-  ( ph -> 1 < ( P - 1 ) )
87 33 35 73 74 86 lelttrd 
 |-  ( ph -> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) < ( P - 1 ) )
88 33 35 71 ltaddsubd 
 |-  ( ph -> ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) < P <-> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) < ( P - 1 ) ) )
89 87 88 mpbird 
 |-  ( ph -> ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) < P )
90 modid 
 |-  ( ( ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) e. RR /\ P e. RR+ ) /\ ( 0 <_ ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) /\ ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) < P ) ) -> ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) )
91 47 36 70 89 90 syl22anc 
 |-  ( ph -> ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) )
92 45 91 eqtrd 
 |-  ( ph -> ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) )
93 92 oveq1d 
 |-  ( ph -> ( ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) = ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) - 1 ) )
94 33 recnd 
 |-  ( ph -> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. CC )
95 pncan 
 |-  ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. CC /\ 1 e. CC ) -> ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) - 1 ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
96 94 52 95 sylancl 
 |-  ( ph -> ( ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + 1 ) - 1 ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
97 93 96 eqtrd 
 |-  ( ph -> ( ( ( ( Q ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )
98 8 97 eqtrd 
 |-  ( ph -> ( Q /L P ) = ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) )