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	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	lgseisen.2	$⊢ φ \to Q \in (ℙ ∖ \{2\})$
	lgseisen.3	$⊢ φ \to P \neq Q$
Assertion	lgseisen	$⊢ φ \to Q /_{L} P = {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}$

Proof

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

Metamath Proof Explorer

Theorem lgseisen

Proof