# 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 ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.2 ${⊢}{\phi }\to {Q}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.3 ${⊢}{\phi }\to {P}\ne {Q}$
Assertion lgseisen ${⊢}{\phi }\to {Q}{/}_{L}{P}={\left(-1\right)}^{\sum _{{x}=1}^{\frac{{P}-1}{2}}⌊\left(\frac{{Q}}{{P}}\right)2{x}⌋}$

### Proof

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