lgseisenlem4

Description: Lemma for lgseisen . The function M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015) (Proof shortened by AV, 15-Jun-2019)

	Ref	Expression
Hypotheses	lgseisen.1	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	lgseisen.2	$⊢ φ \to Q \in (ℙ ∖ \{2\})$
	lgseisen.3	$⊢ φ \to P \neq Q$
	lgseisen.4	$⊢ R = Q 2 x \mod P$
	lgseisen.5	$⊢ M = (x \in (1 \dots \frac{P - 1}{2}) ⟼ \frac{{(- 1)}^{R} R \mod P}{2})$
	lgseisen.6	$⊢ S = Q 2 y \mod P$
	lgseisen.7	$⊢ Y = ℤ / P ℤ$
	lgseisen.8	$⊢ G = {mulGrp}_{Y}$
	lgseisen.9	$⊢ L = ℤRHom (Y)$
Assertion	lgseisenlem4	$⊢ φ \to Q^{\frac{P - 1}{2}} \mod P = {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} \mod P$

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		lgseisen.4	$⊢ R = Q 2 x \mod P$
5		lgseisen.5	$⊢ M = (x \in (1 \dots \frac{P - 1}{2}) ⟼ \frac{{(- 1)}^{R} R \mod P}{2})$
6		lgseisen.6	$⊢ S = Q 2 y \mod P$
7		lgseisen.7	$⊢ Y = ℤ / P ℤ$
8		lgseisen.8	$⊢ G = {mulGrp}_{Y}$
9		lgseisen.9	$⊢ L = ℤRHom (Y)$
10		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
11		zring0	$⊢ 0 = 0_{ℤ_{ring}}$
12		zringabl	$⊢ ℤ_{ring} \in Abel$
13		ablcmn	$⊢ ℤ_{ring} \in Abel \to ℤ_{ring} \in CMnd$
14	12 13	mp1i	$⊢ φ \to ℤ_{ring} \in CMnd$
15	1	eldifad	$⊢ φ \to P \in ℙ$
16	7	znfld	$⊢ P \in ℙ \to Y \in Field$
17	15 16	syl	$⊢ φ \to Y \in Field$
18		isfld	$⊢ Y \in Field \leftrightarrow (Y \in DivRing \land Y \in CRing)$
19	18	simprbi	$⊢ Y \in Field \to Y \in CRing$
20	17 19	syl	$⊢ φ \to Y \in CRing$
21	8	crngmgp	$⊢ Y \in CRing \to G \in CMnd$
22	20 21	syl	$⊢ φ \to G \in CMnd$
23		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
24	22 23	syl	$⊢ φ \to G \in Mnd$
25		fzfid	$⊢ φ \to (1 \dots \frac{P - 1}{2}) \in Fin$
26		crngring	$⊢ Y \in CRing \to Y \in Ring$
27	20 26	syl	$⊢ φ \to Y \in Ring$
28	9	zrhrhm	$⊢ Y \in Ring \to L \in (ℤ_{ring} RingHom Y)$
29	27 28	syl	$⊢ φ \to L \in (ℤ_{ring} RingHom Y)$
30		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
31	10 30	rhmf	$⊢ L \in (ℤ_{ring} RingHom Y) \to L : ℤ ⟶ {Base}_{Y}$
32	29 31	syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Y}$
33		m1expcl	$⊢ k \in ℤ \to {(- 1)}^{k} \in ℤ$
34	33	adantl	$⊢ (φ \land k \in ℤ) \to {(- 1)}^{k} \in ℤ$
35	32 34	cofmpt	$⊢ φ \to L \circ (k \in ℤ ⟼ {(- 1)}^{k}) = (k \in ℤ ⟼ L ({(- 1)}^{k}))$
36		zringmpg	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ = {mulGrp}_{ℤ_{ring}}$
37	36 8	rhmmhm	$⊢ L \in (ℤ_{ring} RingHom Y) \to L \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom G)$
38	29 37	syl	$⊢ φ \to L \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom G)$
39		neg1cn	$⊢ - 1 \in ℂ$
40		neg1ne0	$⊢ - 1 \neq 0$
41		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
42		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\}) = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
43	41 42	expghm	$⊢ (- 1 \in ℂ \land - 1 \neq 0) \to (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})))$
44	39 40 43	mp2an	$⊢ (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})))$
45		ghmmhm	$⊢ (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\}))) \to (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})))$
46	44 45	ax-mp	$⊢ (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})))$
47		cnring	$⊢ ℂ_{fld} \in Ring$
48		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
49		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
50		cndrng	$⊢ ℂ_{fld} \in DivRing$
51	48 49 50	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
52	51 41	unitsubm	$⊢ ℂ_{fld} \in Ring \to ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}})$
53	47 52	ax-mp	$⊢ ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}})$
54	42	resmhm2	$⊢ ((k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\}))) \land ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}})) \to (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom {mulGrp}_{ℂ_{fld}})$
55	46 53 54	mp2an	$⊢ (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom {mulGrp}_{ℂ_{fld}})$
56		zsubrg	$⊢ ℤ \in SubRing (ℂ_{fld})$
57	41	subrgsubm	$⊢ ℤ \in SubRing (ℂ_{fld}) \to ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}})$
58	56 57	ax-mp	$⊢ ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}})$
59	34	fmpttd	$⊢ φ \to (k \in ℤ ⟼ {(- 1)}^{k}) : ℤ ⟶ ℤ$
60	59	frnd	$⊢ φ \to ran (k \in ℤ ⟼ {(- 1)}^{k}) \subseteq ℤ$
61		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ$
62	61	resmhm2b	$⊢ (ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}}) \land ran (k \in ℤ ⟼ {(- 1)}^{k}) \subseteq ℤ) \to ((k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom {mulGrp}_{ℂ_{fld}}) \leftrightarrow (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)))$
63	58 60 62	sylancr	$⊢ φ \to ((k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom {mulGrp}_{ℂ_{fld}}) \leftrightarrow (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)))$
64	55 63	mpbii	$⊢ φ \to (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ))$
65		mhmco	$⊢ (L \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom G) \land (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ))) \to L \circ (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom G)$
66	38 64 65	syl2anc	$⊢ φ \to L \circ (k \in ℤ ⟼ {(- 1)}^{k}) \in (ℤ_{ring} MndHom G)$
67	35 66	eqeltrrd	$⊢ φ \to (k \in ℤ ⟼ L ({(- 1)}^{k})) \in (ℤ_{ring} MndHom G)$
68	2	gausslemma2dlem0a	$⊢ φ \to Q \in ℕ$
69	68	nnred	$⊢ φ \to Q \in ℝ$
70	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
71	69 70	nndivred	$⊢ φ \to \frac{Q}{P} \in ℝ$
72	71	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{Q}{P} \in ℝ$
73		2nn	$⊢ 2 \in ℕ$
74		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
75	74	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℕ$
76		nnmulcl	$⊢ (2 \in ℕ \land x \in ℕ) \to 2 x \in ℕ$
77	73 75 76	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℕ$
78	77	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℝ$
79	72 78	remulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (\frac{Q}{P}) 2 x \in ℝ$
80	79	flcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ⌊(\frac{Q}{P}) 2 x⌋ \in ℤ$
81		eqid	$⊢ (x \in (1 \dots \frac{P - 1}{2}) ⟼ ⌊(\frac{Q}{P}) 2 x⌋) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ ⌊(\frac{Q}{P}) 2 x⌋)$
82		fvexd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ⌊(\frac{Q}{P}) 2 x⌋ \in V$
83		c0ex	$⊢ 0 \in V$
84	83	a1i	$⊢ φ \to 0 \in V$
85	81 25 82 84	fsuppmptdm	$⊢ φ \to {finSupp}_{0} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ ⌊(\frac{Q}{P}) 2 x⌋))$
86		oveq2	$⊢ k = ⌊(\frac{Q}{P}) 2 x⌋ \to {(- 1)}^{k} = {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}$
87	86	fveq2d	$⊢ k = ⌊(\frac{Q}{P}) 2 x⌋ \to L ({(- 1)}^{k}) = L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})$
88		oveq2	$⊢ k = {\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋ \to {(- 1)}^{k} = {(- 1)}^{{\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}$
89	88	fveq2d	$⊢ k = {\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋ \to L ({(- 1)}^{k}) = L ({(- 1)}^{{\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋})$
90	10 11 14 24 25 67 80 85 87 89	gsummhm2	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) = L ({(- 1)}^{{\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋})$
91	8 30	mgpbas	$⊢ {Base}_{Y} = {Base}_{G}$
92		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
93	8 92	mgpplusg	$⊢ \cdot_{Y} = +_{G}$
94	32	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L : ℤ ⟶ {Base}_{Y}$
95		m1expcl	$⊢ ⌊(\frac{Q}{P}) 2 x⌋ \in ℤ \to {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} \in ℤ$
96	80 95	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} \in ℤ$
97	94 96	ffvelrnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \in {Base}_{Y}$
98		neg1z	$⊢ - 1 \in ℤ$
99	2	eldifad	$⊢ φ \to Q \in ℙ$
100	99	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℙ$
101		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
102	100 101	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℤ$
103	77	nnzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℤ$
104	102 103	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℤ$
105	15	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℙ$
106		prmnn	$⊢ P \in ℙ \to P \in ℕ$
107	105 106	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℕ$
108	104 107	zmodcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \mod P \in ℕ_{0}$
109	4 108	eqeltrid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℕ_{0}$
110		zexpcl	$⊢ (- 1 \in ℤ \land R \in ℕ_{0}) \to {(- 1)}^{R} \in ℤ$
111	98 109 110	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \in ℤ$
112	111 102	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} Q \in ℤ$
113	94 112	ffvelrnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{R} Q) \in {Base}_{Y}$
114		eqid	$⊢ (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}))$
115		eqid	$⊢ (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q))$
116	91 93 22 25 97 113 114 115	gsummptfidmadd2	$⊢ φ \to \sum_{G} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q))) = ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) \cdot_{Y} ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{R} Q))$
117		eqidd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}))$
118		eqidd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q))$
119	25 97 113 117 118	offval2	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \cdot_{Y} L ({(- 1)}^{R} Q))$
120	29	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L \in (ℤ_{ring} RingHom Y)$
121		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
122	10 121 92	rhmmul	$⊢ (L \in (ℤ_{ring} RingHom Y) \land {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} \in ℤ \land {(- 1)}^{R} Q \in ℤ) \to L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} Q) = L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \cdot_{Y} L ({(- 1)}^{R} Q)$
123	120 96 112 122	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} Q) = L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \cdot_{Y} L ({(- 1)}^{R} Q)$
124	104	zred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℝ$
125	107	nnrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ^{+}$
126		modval	$⊢ (Q 2 x \in ℝ \land P \in ℝ^{+}) \to Q 2 x \mod P = Q 2 x - P ⌊\frac{Q 2 x}{P}⌋$
127	124 125 126	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \mod P = Q 2 x - P ⌊\frac{Q 2 x}{P}⌋$
128	4 127	syl5eq	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R = Q 2 x - P ⌊\frac{Q 2 x}{P}⌋$
129	102	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℂ$
130	77	nncnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℂ$
131	107	nncnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℂ$
132	107	nnne0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \neq 0$
133	129 130 131 132	div23d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{Q 2 x}{P} = (\frac{Q}{P}) 2 x$
134	133	fveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ⌊\frac{Q 2 x}{P}⌋ = ⌊(\frac{Q}{P}) 2 x⌋$
135	134	oveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P ⌊\frac{Q 2 x}{P}⌋ = P ⌊(\frac{Q}{P}) 2 x⌋$
136	135	oveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x - P ⌊\frac{Q 2 x}{P}⌋ = Q 2 x - P ⌊(\frac{Q}{P}) 2 x⌋$
137	128 136	eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R = Q 2 x - P ⌊(\frac{Q}{P}) 2 x⌋$
138	137	oveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P ⌊(\frac{Q}{P}) 2 x⌋ + R = P ⌊(\frac{Q}{P}) 2 x⌋ + Q 2 x - P ⌊(\frac{Q}{P}) 2 x⌋$
139		prmz	$⊢ P \in ℙ \to P \in ℤ$
140	105 139	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℤ$
141	140 80	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P ⌊(\frac{Q}{P}) 2 x⌋ \in ℤ$
142	141	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P ⌊(\frac{Q}{P}) 2 x⌋ \in ℂ$
143	104	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℂ$
144	142 143	pncan3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P ⌊(\frac{Q}{P}) 2 x⌋ + Q 2 x - P ⌊(\frac{Q}{P}) 2 x⌋ = Q 2 x$
145		2cnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 \in ℂ$
146	75	nncnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℂ$
147	129 145 146	mul12d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x = 2 Q x$
148	138 144 147	3eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P ⌊(\frac{Q}{P}) 2 x⌋ + R = 2 Q x$
149	148	oveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋ + R} = {(- 1)}^{2 Q x}$
150	39	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - 1 \in ℂ$
151	40	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - 1 \neq 0$
152	109	nn0zd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℤ$
153		expaddz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (P ⌊(\frac{Q}{P}) 2 x⌋ \in ℤ \land R \in ℤ)) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋ + R} = {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R}$
154	150 151 141 152 153	syl22anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋ + R} = {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R}$
155		expmulz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (P \in ℤ \land ⌊(\frac{Q}{P}) 2 x⌋ \in ℤ)) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋} = {({-1}^{P})}^{⌊(\frac{Q}{P}) 2 x⌋}$
156	150 151 140 80 155	syl22anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋} = {({-1}^{P})}^{⌊(\frac{Q}{P}) 2 x⌋}$
157		1cnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 \in ℂ$
158		eldifsni	$⊢ P \in (ℙ ∖ \{2\}) \to P \neq 2$
159	1 158	syl	$⊢ φ \to P \neq 2$
160	159	necomd	$⊢ φ \to 2 \neq P$
161	160	neneqd	$⊢ φ \to \neg 2 = P$
162	161	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg 2 = P$
163		2z	$⊢ 2 \in ℤ$
164		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
165	163 164	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
166		dvdsprm	$⊢ (2 \in ℤ_{\geq 2} \land P \in ℙ) \to (2 ∥ P \leftrightarrow 2 = P)$
167	165 105 166	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 ∥ P \leftrightarrow 2 = P)$
168	162 167	mtbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg 2 ∥ P$
169		oexpneg	$⊢ (1 \in ℂ \land P \in ℕ \land \neg 2 ∥ P) \to {(- 1)}^{P} = - 1^{P}$
170	157 107 168 169	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P} = - 1^{P}$
171		1exp	$⊢ P \in ℤ \to 1^{P} = 1$
172	140 171	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1^{P} = 1$
173	172	negeqd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - 1^{P} = - 1$
174	170 173	eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P} = - 1$
175	174	oveq1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {({-1}^{P})}^{⌊(\frac{Q}{P}) 2 x⌋} = {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}$
176	156 175	eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋} = {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}$
177	176	oveq1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} = {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R}$
178	154 177	eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{P ⌊(\frac{Q}{P}) 2 x⌋ + R} = {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R}$
179		nnmulcl	$⊢ (Q \in ℕ \land x \in ℕ) \to Q x \in ℕ$
180	68 74 179	syl2an	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q x \in ℕ$
181	180	nnnn0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q x \in ℕ_{0}$
182		2nn0	$⊢ 2 \in ℕ_{0}$
183	182	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 \in ℕ_{0}$
184	150 181 183	expmuld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{2 Q x} = {({-1}^{2})}^{Q x}$
185		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
186	185	oveq1i	$⊢ {({-1}^{2})}^{Q x} = 1^{Q x}$
187	180	nnzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q x \in ℤ$
188		1exp	$⊢ Q x \in ℤ \to 1^{Q x} = 1$
189	187 188	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1^{Q x} = 1$
190	186 189	syl5eq	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {({-1}^{2})}^{Q x} = 1$
191	184 190	eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{2 Q x} = 1$
192	149 178 191	3eqtr3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} = 1$
193	192	oveq1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} Q = 1 Q$
194	96	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} \in ℂ$
195	111	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \in ℂ$
196	194 195 129	mulassd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} Q = {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} Q$
197	129	mulid2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 Q = Q$
198	193 196 197	3eqtr3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} Q = Q$
199	198	fveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋} {(- 1)}^{R} Q) = L (Q)$
200	123 199	eqtr3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \cdot_{Y} L ({(- 1)}^{R} Q) = L (Q)$
201	200	mpteq2dva	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \cdot_{Y} L ({(- 1)}^{R} Q)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (Q))$
202	119 201	eqtrd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (Q))$
203	202	oveq2d	$⊢ φ \to \sum_{G} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q))) = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (Q)$
204	1 2 3 4 5 6 7 8 9	lgseisenlem3	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{R} Q) = 1_{Y}$
205	204	oveq2d	$⊢ φ \to ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) \cdot_{Y} ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{R} Q)) = ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) \cdot_{Y} 1_{Y}$
206	116 203 205	3eqtr3rd	$⊢ φ \to ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) \cdot_{Y} 1_{Y} = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (Q)$
207		eqid	$⊢ 0_{G} = 0_{G}$
208	97	fmpttd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) : (1 \dots \frac{P - 1}{2}) ⟶ {Base}_{Y}$
209		fvexd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \in V$
210		fvexd	$⊢ φ \to 0_{G} \in V$
211	114 25 209 210	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})))$
212	91 207 22 25 208 211	gsumcl	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \in {Base}_{Y}$
213		eqid	$⊢ 1_{Y} = 1_{Y}$
214	30 92 213	ringridm	$⊢ (Y \in Ring \land {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) \in {Base}_{Y}) \to ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) \cdot_{Y} 1_{Y} = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})$
215	27 212 214	syl2anc	$⊢ φ \to ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})) \cdot_{Y} 1_{Y} = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋})$
216	99 101	syl	$⊢ φ \to Q \in ℤ$
217	32 216	ffvelrnd	$⊢ φ \to L (Q) \in {Base}_{Y}$
218		eqid	$⊢ \cdot_{G} = \cdot_{G}$
219	91 218	gsumconst	$⊢ (G \in Mnd \land (1 \dots \frac{P - 1}{2}) \in Fin \land L (Q) \in {Base}_{Y}) \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (Q) = \|(1 \dots \frac{P - 1}{2})\| \cdot_{G} L (Q)$
220	24 25 217 219	syl3anc	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (Q) = \|(1 \dots \frac{P - 1}{2})\| \cdot_{G} L (Q)$
221		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
222	1 221	syl	$⊢ φ \to \frac{P - 1}{2} \in ℕ$
223	222	nnnn0d	$⊢ φ \to \frac{P - 1}{2} \in ℕ_{0}$
224		hashfz1	$⊢ \frac{P - 1}{2} \in ℕ_{0} \to \|(1 \dots \frac{P - 1}{2})\| = \frac{P - 1}{2}$
225	223 224	syl	$⊢ φ \to \|(1 \dots \frac{P - 1}{2})\| = \frac{P - 1}{2}$
226	225	oveq1d	$⊢ φ \to \|(1 \dots \frac{P - 1}{2})\| \cdot_{G} L (Q) = (\frac{P - 1}{2}) \cdot_{G} L (Q)$
227	36 10	mgpbas	$⊢ ℤ = {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)}$
228		eqid	$⊢ \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} = \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)}$
229	227 228 218	mhmmulg	$⊢ (L \in (({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ) MndHom G) \land \frac{P - 1}{2} \in ℕ_{0} \land Q \in ℤ) \to L ((\frac{P - 1}{2}) \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} Q) = (\frac{P - 1}{2}) \cdot_{G} L (Q)$
230	38 223 216 229	syl3anc	$⊢ φ \to L ((\frac{P - 1}{2}) \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} Q) = (\frac{P - 1}{2}) \cdot_{G} L (Q)$
231	58	a1i	$⊢ φ \to ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}})$
232		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
233	232 61 228	submmulg	$⊢ (ℤ \in SubMnd ({mulGrp}_{ℂ_{fld}}) \land \frac{P - 1}{2} \in ℕ_{0} \land Q \in ℤ) \to (\frac{P - 1}{2}) \cdot_{{mulGrp}_{ℂ_{fld}}} Q = (\frac{P - 1}{2}) \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} Q$
234	231 223 216 233	syl3anc	$⊢ φ \to (\frac{P - 1}{2}) \cdot_{{mulGrp}_{ℂ_{fld}}} Q = (\frac{P - 1}{2}) \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} Q$
235	216	zcnd	$⊢ φ \to Q \in ℂ$
236		cnfldexp	$⊢ (Q \in ℂ \land \frac{P - 1}{2} \in ℕ_{0}) \to (\frac{P - 1}{2}) \cdot_{{mulGrp}_{ℂ_{fld}}} Q = Q^{\frac{P - 1}{2}}$
237	235 223 236	syl2anc	$⊢ φ \to (\frac{P - 1}{2}) \cdot_{{mulGrp}_{ℂ_{fld}}} Q = Q^{\frac{P - 1}{2}}$
238	234 237	eqtr3d	$⊢ φ \to (\frac{P - 1}{2}) \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} Q = Q^{\frac{P - 1}{2}}$
239	238	fveq2d	$⊢ φ \to L ((\frac{P - 1}{2}) \cdot_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℤ)} Q) = L (Q^{\frac{P - 1}{2}})$
240	230 239	eqtr3d	$⊢ φ \to (\frac{P - 1}{2}) \cdot_{G} L (Q) = L (Q^{\frac{P - 1}{2}})$
241	220 226 240	3eqtrd	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (Q) = L (Q^{\frac{P - 1}{2}})$
242	206 215 241	3eqtr3d	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{⌊(\frac{Q}{P}) 2 x⌋}) = L (Q^{\frac{P - 1}{2}})$
243		subrgsubg	$⊢ ℤ \in SubRing (ℂ_{fld}) \to ℤ \in SubGrp (ℂ_{fld})$
244	56 243	ax-mp	$⊢ ℤ \in SubGrp (ℂ_{fld})$
245		subgsubm	$⊢ ℤ \in SubGrp (ℂ_{fld}) \to ℤ \in SubMnd (ℂ_{fld})$
246	244 245	mp1i	$⊢ φ \to ℤ \in SubMnd (ℂ_{fld})$
247	80	fmpttd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ ⌊(\frac{Q}{P}) 2 x⌋) : (1 \dots \frac{P - 1}{2}) ⟶ ℤ$
248		df-zring	$⊢ ℤ_{ring} = ℂ_{fld} ↾_{𝑠} ℤ$
249	25 246 247 248	gsumsubm	$⊢ φ \to {\sum_{ℂ_{fld}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋ = {\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋$
250	80	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ⌊(\frac{Q}{P}) 2 x⌋ \in ℂ$
251	25 250	gsumfsum	$⊢ φ \to {\sum_{ℂ_{fld}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋ = \sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋$
252	249 251	eqtr3d	$⊢ φ \to {\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋ = \sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋$
253	252	oveq2d	$⊢ φ \to {(- 1)}^{{\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} = {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}$
254	253	fveq2d	$⊢ φ \to L ({(- 1)}^{{\sum_{ℤ_{ring}}}_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}) = L ({(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋})$
255	90 242 254	3eqtr3d	$⊢ φ \to L (Q^{\frac{P - 1}{2}}) = L ({(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋})$
256	70	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
257		zexpcl	$⊢ (Q \in ℤ \land \frac{P - 1}{2} \in ℕ_{0}) \to Q^{\frac{P - 1}{2}} \in ℤ$
258	216 223 257	syl2anc	$⊢ φ \to Q^{\frac{P - 1}{2}} \in ℤ$
259	25 80	fsumzcl	$⊢ φ \to \sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋ \in ℤ$
260		m1expcl	$⊢ \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⌋} \in ℤ$
261	259 260	syl	$⊢ φ \to {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} \in ℤ$
262	7 9	zndvds	$⊢ (P \in ℕ_{0} \land Q^{\frac{P - 1}{2}} \in ℤ \land {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} \in ℤ) \to (L (Q^{\frac{P - 1}{2}}) = L ({(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}) \leftrightarrow P ∥ (Q^{\frac{P - 1}{2}} - {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}))$
263	256 258 261 262	syl3anc	$⊢ φ \to (L (Q^{\frac{P - 1}{2}}) = L ({(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}) \leftrightarrow P ∥ (Q^{\frac{P - 1}{2}} - {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}))$
264	255 263	mpbid	$⊢ φ \to P ∥ (Q^{\frac{P - 1}{2}} - {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋})$
265		moddvds	$⊢ (P \in ℕ \land Q^{\frac{P - 1}{2}} \in ℤ \land {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} \in ℤ) \to (Q^{\frac{P - 1}{2}} \mod P = {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} \mod P \leftrightarrow P ∥ (Q^{\frac{P - 1}{2}} - {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}))$
266	70 258 261 265	syl3anc	$⊢ φ \to (Q^{\frac{P - 1}{2}} \mod P = {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} \mod P \leftrightarrow P ∥ (Q^{\frac{P - 1}{2}} - {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋}))$
267	264 266	mpbird	$⊢ φ \to Q^{\frac{P - 1}{2}} \mod P = {(- 1)}^{\sum_{x = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 x⌋} \mod P$

Metamath Proof Explorer

Theorem lgseisenlem4

Proof