lgseisenlem3

Description: Lemma for lgseisen . (Contributed by Mario Carneiro, 17-Jun-2015) (Proof shortened by AV, 28-Jul-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	lgseisenlem3	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{R} Q) = 1_{Y}$

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		oveq2	$⊢ k = x \to 2 k = 2 x$
11	10	fveq2d	$⊢ k = x \to L (2 k) = L (2 x)$
12	11	cbvmptv	$⊢ (k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x))$
13	12	oveq2i	$⊢ {\sum_{G}}_{k = 1}^{\frac{P - 1}{2}} L (2 k) = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 x)$
14		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
15	8 14	mgpbas	$⊢ {Base}_{Y} = {Base}_{G}$
16		eqid	$⊢ 0_{G} = 0_{G}$
17	1	eldifad	$⊢ φ \to P \in ℙ$
18	7	znfld	$⊢ P \in ℙ \to Y \in Field$
19	17 18	syl	$⊢ φ \to Y \in Field$
20		isfld	$⊢ Y \in Field \leftrightarrow (Y \in DivRing \land Y \in CRing)$
21	20	simprbi	$⊢ Y \in Field \to Y \in CRing$
22	19 21	syl	$⊢ φ \to Y \in CRing$
23	8	crngmgp	$⊢ Y \in CRing \to G \in CMnd$
24	22 23	syl	$⊢ φ \to G \in CMnd$
25		fzfid	$⊢ φ \to (1 \dots \frac{P - 1}{2}) \in Fin$
26		crngring	$⊢ Y \in CRing \to Y \in Ring$
27	22 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		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
31	30 14	rhmf	$⊢ L \in (ℤ_{ring} RingHom Y) \to L : ℤ ⟶ {Base}_{Y}$
32	29 31	syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Y}$
33		2z	$⊢ 2 \in ℤ$
34		elfzelz	$⊢ k \in (1 \dots \frac{P - 1}{2}) \to k \in ℤ$
35		zmulcl	$⊢ (2 \in ℤ \land k \in ℤ) \to 2 k \in ℤ$
36	33 34 35	sylancr	$⊢ k \in (1 \dots \frac{P - 1}{2}) \to 2 k \in ℤ$
37		ffvelcdm	$⊢ (L : ℤ ⟶ {Base}_{Y} \land 2 k \in ℤ) \to L (2 k) \in {Base}_{Y}$
38	32 36 37	syl2an	$⊢ (φ \land k \in (1 \dots \frac{P - 1}{2})) \to L (2 k) \in {Base}_{Y}$
39	38	fmpttd	$⊢ φ \to (k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) : (1 \dots \frac{P - 1}{2}) ⟶ {Base}_{Y}$
40		eqid	$⊢ (k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) = (k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k))$
41		fvexd	$⊢ (φ \land k \in (1 \dots \frac{P - 1}{2})) \to L (2 k) \in V$
42		fvexd	$⊢ φ \to 0_{G} \in V$
43	40 25 41 42	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} ((k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)))$
44	1 2 3 4 5 6	lgseisenlem2	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) \underset{1-1 onto}{⟶} (1 \dots \frac{P - 1}{2})$
45	15 16 24 25 39 43 44	gsumf1o	$⊢ φ \to {\sum_{G}}_{k = 1}^{\frac{P - 1}{2}} L (2 k) = \sum_{G} ((k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) \circ M)$
46	13 45	eqtr3id	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 x) = \sum_{G} ((k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) \circ M)$
47	1 2 3 4 5	lgseisenlem1	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) ⟶ (1 \dots \frac{P - 1}{2})$
48	5	fmpt	$⊢ \forall x \in (1 \dots \frac{P - 1}{2}) \frac{{(- 1)}^{R} R \mod P}{2} \in (1 \dots \frac{P - 1}{2}) \leftrightarrow M : (1 \dots \frac{P - 1}{2}) ⟶ (1 \dots \frac{P - 1}{2})$
49	47 48	sylibr	$⊢ φ \to \forall x \in (1 \dots \frac{P - 1}{2}) \frac{{(- 1)}^{R} R \mod P}{2} \in (1 \dots \frac{P - 1}{2})$
50	5	a1i	$⊢ φ \to M = (x \in (1 \dots \frac{P - 1}{2}) ⟼ \frac{{(- 1)}^{R} R \mod P}{2})$
51		eqidd	$⊢ φ \to (k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) = (k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k))$
52		oveq2	$⊢ k = \frac{{(- 1)}^{R} R \mod P}{2} \to 2 k = 2 (\frac{{(- 1)}^{R} R \mod P}{2})$
53	52	fveq2d	$⊢ k = \frac{{(- 1)}^{R} R \mod P}{2} \to L (2 k) = L (2 (\frac{{(- 1)}^{R} R \mod P}{2}))$
54	49 50 51 53	fmptcof	$⊢ φ \to (k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) \circ M = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 (\frac{{(- 1)}^{R} R \mod P}{2})))$
55	54	oveq2d	$⊢ φ \to \sum_{G} ((k \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 k)) \circ M) = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 (\frac{{(- 1)}^{R} R \mod P}{2}))$
56	2	eldifad	$⊢ φ \to Q \in ℙ$
57	56	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℙ$
58		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
59	57 58	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℤ$
60		2nn	$⊢ 2 \in ℕ$
61		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
62	61	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℕ$
63		nnmulcl	$⊢ (2 \in ℕ \land x \in ℕ) \to 2 x \in ℕ$
64	60 62 63	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℕ$
65	64	nnzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℤ$
66	59 65	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℤ$
67	17	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℙ$
68		prmnn	$⊢ P \in ℙ \to P \in ℕ$
69	67 68	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℕ$
70	66 69	zmodcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \mod P \in ℕ_{0}$
71	4 70	eqeltrid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℕ_{0}$
72	71	nn0zd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℤ$
73		m1expcl	$⊢ R \in ℤ \to {(- 1)}^{R} \in ℤ$
74	72 73	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \in ℤ$
75	74 72	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \in ℤ$
76	75 69	zmodcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \in ℕ_{0}$
77	76	nn0cnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \in ℂ$
78		2cnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 \in ℂ$
79		2ne0	$⊢ 2 \neq 0$
80	79	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 \neq 0$
81	77 78 80	divcan2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 (\frac{{(- 1)}^{R} R \mod P}{2}) = {(- 1)}^{R} R \mod P$
82	81	fveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L (2 (\frac{{(- 1)}^{R} R \mod P}{2})) = L ({(- 1)}^{R} R \mod P)$
83	69	nnrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ^{+}$
84		eqidd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \mod P = {(- 1)}^{R} \mod P$
85	4	oveq1i	$⊢ R \mod P = (Q 2 x \mod P) \mod P$
86	66	zred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℝ$
87		modabs2	$⊢ (Q 2 x \in ℝ \land P \in ℝ^{+}) \to (Q 2 x \mod P) \mod P = Q 2 x \mod P$
88	86 83 87	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (Q 2 x \mod P) \mod P = Q 2 x \mod P$
89	85 88	eqtrid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \mod P = Q 2 x \mod P$
90	74 74 72 66 83 84 89	modmul12d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P = {(- 1)}^{R} Q 2 x \mod P$
91	75	zred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \in ℝ$
92		modabs2	$⊢ ({(- 1)}^{R} R \in ℝ \land P \in ℝ^{+}) \to ({(- 1)}^{R} R \mod P) \mod P = {(- 1)}^{R} R \mod P$
93	91 83 92	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ({(- 1)}^{R} R \mod P) \mod P = {(- 1)}^{R} R \mod P$
94	74	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \in ℂ$
95	59	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℂ$
96	65	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℂ$
97	94 95 96	mulassd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} Q 2 x = {(- 1)}^{R} Q 2 x$
98	97	oveq1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} Q 2 x \mod P = {(- 1)}^{R} Q 2 x \mod P$
99	90 93 98	3eqtr4d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ({(- 1)}^{R} R \mod P) \mod P = {(- 1)}^{R} Q 2 x \mod P$
100	17 68	syl	$⊢ φ \to P \in ℕ$
101	100	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℕ$
102	76	nn0zd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \in ℤ$
103	74 59	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} Q \in ℤ$
104	103 65	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} Q 2 x \in ℤ$
105		moddvds	$⊢ (P \in ℕ \land {(- 1)}^{R} R \mod P \in ℤ \land {(- 1)}^{R} Q 2 x \in ℤ) \to (({(- 1)}^{R} R \mod P) \mod P = {(- 1)}^{R} Q 2 x \mod P \leftrightarrow P ∥ (({(- 1)}^{R} R \mod P) - {(- 1)}^{R} Q 2 x))$
106	101 102 104 105	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (({(- 1)}^{R} R \mod P) \mod P = {(- 1)}^{R} Q 2 x \mod P \leftrightarrow P ∥ (({(- 1)}^{R} R \mod P) - {(- 1)}^{R} Q 2 x))$
107	99 106	mpbid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P ∥ (({(- 1)}^{R} R \mod P) - {(- 1)}^{R} Q 2 x)$
108	69	nnnn0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℕ_{0}$
109	7 9	zndvds	$⊢ (P \in ℕ_{0} \land {(- 1)}^{R} R \mod P \in ℤ \land {(- 1)}^{R} Q 2 x \in ℤ) \to (L ({(- 1)}^{R} R \mod P) = L ({(- 1)}^{R} Q 2 x) \leftrightarrow P ∥ (({(- 1)}^{R} R \mod P) - {(- 1)}^{R} Q 2 x))$
110	108 102 104 109	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (L ({(- 1)}^{R} R \mod P) = L ({(- 1)}^{R} Q 2 x) \leftrightarrow P ∥ (({(- 1)}^{R} R \mod P) - {(- 1)}^{R} Q 2 x))$
111	107 110	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{R} R \mod P) = L ({(- 1)}^{R} Q 2 x)$
112	29	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L \in (ℤ_{ring} RingHom Y)$
113		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
114		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
115	30 113 114	rhmmul	$⊢ (L \in (ℤ_{ring} RingHom Y) \land {(- 1)}^{R} Q \in ℤ \land 2 x \in ℤ) \to L ({(- 1)}^{R} Q 2 x) = L ({(- 1)}^{R} Q) \cdot_{Y} L (2 x)$
116	112 103 65 115	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{R} Q 2 x) = L ({(- 1)}^{R} Q) \cdot_{Y} L (2 x)$
117	82 111 116	3eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L (2 (\frac{{(- 1)}^{R} R \mod P}{2})) = L ({(- 1)}^{R} Q) \cdot_{Y} L (2 x)$
118	117	mpteq2dva	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 (\frac{{(- 1)}^{R} R \mod P}{2}))) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q) \cdot_{Y} L (2 x))$
119	32	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L : ℤ ⟶ {Base}_{Y}$
120	119 103	ffvelcdmd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{R} Q) \in {Base}_{Y}$
121	119 65	ffvelcdmd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L (2 x) \in {Base}_{Y}$
122		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))$
123		eqidd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x))$
124	25 120 121 122 123	offval2	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q) \cdot_{Y} L (2 x))$
125	118 124	eqtr4d	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 (\frac{{(- 1)}^{R} R \mod P}{2}))) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x))$
126	125	oveq2d	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 (\frac{{(- 1)}^{R} R \mod P}{2})) = \sum_{G} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x)))$
127	46 55 126	3eqtrd	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 x) = \sum_{G} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x)))$
128	8 114	mgpplusg	$⊢ \cdot_{Y} = +_{G}$
129		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))$
130		eqid	$⊢ (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x)) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x))$
131	15 128 24 25 120 121 129 130	gsummptfidmadd2	$⊢ φ \to \sum_{G} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) {\cdot_{Y}}_{f} (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x))) = ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{R} Q)) \cdot_{Y} ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x))$
132	127 131	eqtrd	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 x) = ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{R} Q)) \cdot_{Y} ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x))$
133	132	oveq1d	$⊢ φ \to ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) /_{r} (Y) ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) = (({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{R} Q)) \cdot_{Y} ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x))) /_{r} (Y) ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x))$
134		eqid	$⊢ Unit (Y) = Unit (Y)$
135	134 8	unitsubm	$⊢ Y \in Ring \to Unit (Y) \in SubMnd (G)$
136	27 135	syl	$⊢ φ \to Unit (Y) \in SubMnd (G)$
137		elfzle2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \leq \frac{P - 1}{2}$
138	137	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \leq \frac{P - 1}{2}$
139	62	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℝ$
140		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
141		uz2m1nn	$⊢ P \in ℤ_{\geq 2} \to P - 1 \in ℕ$
142	67 140 141	3syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℕ$
143	142	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℝ$
144		2re	$⊢ 2 \in ℝ$
145	144	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 \in ℝ$
146		2pos	$⊢ 0 < 2$
147	146	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 < 2$
148		lemuldiv2	$⊢ (x \in ℝ \land P - 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 x \leq P - 1 \leftrightarrow x \leq \frac{P - 1}{2})$
149	139 143 145 147 148	syl112anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 x \leq P - 1 \leftrightarrow x \leq \frac{P - 1}{2})$
150	138 149	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \leq P - 1$
151		prmz	$⊢ P \in ℙ \to P \in ℤ$
152	67 151	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℤ$
153		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
154	152 153	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℤ$
155		fznn	$⊢ P - 1 \in ℤ \to (2 x \in (1 \dots P - 1) \leftrightarrow (2 x \in ℕ \land 2 x \leq P - 1))$
156	154 155	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 x \in (1 \dots P - 1) \leftrightarrow (2 x \in ℕ \land 2 x \leq P - 1))$
157	64 150 156	mpbir2and	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in (1 \dots P - 1)$
158		fzm1ndvds	$⊢ (P \in ℕ \land 2 x \in (1 \dots P - 1)) \to \neg P ∥ 2 x$
159	69 157 158	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ 2 x$
160		eqid	$⊢ 0_{Y} = 0_{Y}$
161	7 9 160	zndvds0	$⊢ (P \in ℕ_{0} \land 2 x \in ℤ) \to (L (2 x) = 0_{Y} \leftrightarrow P ∥ 2 x)$
162	108 65 161	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (L (2 x) = 0_{Y} \leftrightarrow P ∥ 2 x)$
163	162	necon3abid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (L (2 x) \neq 0_{Y} \leftrightarrow \neg P ∥ 2 x)$
164	159 163	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L (2 x) \neq 0_{Y}$
165	20	simplbi	$⊢ Y \in Field \to Y \in DivRing$
166	19 165	syl	$⊢ φ \to Y \in DivRing$
167	166	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Y \in DivRing$
168	14 134 160	drngunit	$⊢ Y \in DivRing \to (L (2 x) \in Unit (Y) \leftrightarrow (L (2 x) \in {Base}_{Y} \land L (2 x) \neq 0_{Y}))$
169	167 168	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (L (2 x) \in Unit (Y) \leftrightarrow (L (2 x) \in {Base}_{Y} \land L (2 x) \neq 0_{Y}))$
170	121 164 169	mpbir2and	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L (2 x) \in Unit (Y)$
171	170	fmpttd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x)) : (1 \dots \frac{P - 1}{2}) ⟶ Unit (Y)$
172		fvexd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L (2 x) \in V$
173	130 25 172 42	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L (2 x)))$
174	16 24 25 136 171 173	gsumsubmcl	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 x) \in Unit (Y)$
175		eqid	$⊢ /_{r} (Y) = /_{r} (Y)$
176		eqid	$⊢ 1_{Y} = 1_{Y}$
177	134 175 176	dvrid	$⊢ (Y \in Ring \land {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 x) \in Unit (Y)) \to ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) /_{r} (Y) ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) = 1_{Y}$
178	27 174 177	syl2anc	$⊢ φ \to ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) /_{r} (Y) ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) = 1_{Y}$
179	120	fmpttd	$⊢ φ \to (x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)) : (1 \dots \frac{P - 1}{2}) ⟶ {Base}_{Y}$
180		fvexd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to L ({(- 1)}^{R} Q) \in V$
181	129 25 180 42	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} ((x \in (1 \dots \frac{P - 1}{2}) ⟼ L ({(- 1)}^{R} Q)))$
182	15 16 24 25 179 181	gsumcl	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{R} Q) \in {Base}_{Y}$
183	14 134 175 114	dvrcan3	$⊢ (Y \in Ring \land {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{R} Q) \in {Base}_{Y} \land {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L (2 x) \in Unit (Y)) \to (({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{R} Q)) \cdot_{Y} ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x))) /_{r} (Y) ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{R} Q)$
184	27 182 174 183	syl3anc	$⊢ φ \to (({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L ({(- 1)}^{R} Q)) \cdot_{Y} ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x))) /_{r} (Y) ({\sum_{G}}_{x = 1}^{\frac{P - 1}{2}}, L (2 x)) = {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{R} Q)$
185	133 178 184	3eqtr3rd	$⊢ φ \to {\sum_{G}}_{x = 1}^{\frac{P - 1}{2}} L ({(- 1)}^{R} Q) = 1_{Y}$

Metamath Proof Explorer

Theorem lgseisenlem3

Proof