lgseisenlem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgseisenlem4		Structured version Visualization version GIF version

Theorem lgseisenlem4 27347

Description: Lemma for lgseisen 27348. (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.)

**Hypotheses**
Ref	Expression
lgseisen.1	⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
lgseisen.2	⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
lgseisen.3	⊢ (𝜑 → 𝑃 ≠ 𝑄)
lgseisen.4	⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
lgseisen.5	⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
lgseisen.6	⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
lgseisen.7	⊢ 𝑌 = (ℤ/nℤ‘𝑃)
lgseisen.8	⊢ 𝐺 = (mulGrp‘𝑌)
lgseisen.9	⊢ 𝐿 = (ℤRHom‘𝑌)

**Assertion**
Ref	Expression
lgseisenlem4	⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃))

Distinct variable groups: 𝑥,𝐺 𝑥,𝐿 𝑥,𝑦,𝑃 𝜑,𝑥,𝑦 𝑦,𝑀 𝑥,𝑄,𝑦 𝑥,𝑌 𝑥,𝑆 Allowed substitution hints: 𝑅(𝑥,𝑦) 𝑆(𝑦) 𝐺(𝑦) 𝐿(𝑦) 𝑀(𝑥) 𝑌(𝑦)

Proof of Theorem lgseisenlem4 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zringbas 21410	. . . . 5 ⊢ ℤ = (Base‘ℤ_ring)
2		zring0 21415	. . . . 5 ⊢ 0 = (0_g‘ℤ_ring)
3		zringabl 21408	. . . . . 6 ⊢ ℤ_ring ∈ Abel
4		ablcmn 19718	. . . . . 6 ⊢ (ℤ_ring ∈ Abel → ℤ_ring ∈ CMnd)
5	3, 4	mp1i 13	. . . . 5 ⊢ (𝜑 → ℤ_ring ∈ CMnd)
6		lgseisen.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
7	6	eldifad 3912	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℙ)
8		lgseisen.7	. . . . . . . . . 10 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
9	8	znfld 21517	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field)
10	7, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ Field)
11		isfld 20675	. . . . . . . . 9 ⊢ (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing))
12	11	simprbi 496	. . . . . . . 8 ⊢ (𝑌 ∈ Field → 𝑌 ∈ CRing)
13	10, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ CRing)
14		lgseisen.8	. . . . . . . 8 ⊢ 𝐺 = (mulGrp‘𝑌)
15	14	crngmgp 20178	. . . . . . 7 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
16	13, 15	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ CMnd)
17		cmnmnd 19728	. . . . . 6 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
18	16, 17	syl 17	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Mnd)
19		fzfid 13898	. . . . 5 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
20		crngring 20182	. . . . . . . . . 10 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
21	13, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ Ring)
22		lgseisen.9	. . . . . . . . . 10 ⊢ 𝐿 = (ℤRHom‘𝑌)
23	22	zrhrhm 21468	. . . . . . . . 9 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
24	21, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
25		eqid 2735	. . . . . . . . 9 ⊢ (Base‘𝑌) = (Base‘𝑌)
26	1, 25	rhmf 20422	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
27	24, 26	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
28		m1expcl 14011	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → (-1↑𝑘) ∈ ℤ)
29	28	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℤ)
30	27, 29	cofmpt 7077	. . . . . 6 ⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) = (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))))
31		zringmpg 21428	. . . . . . . . 9 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = (mulGrp‘ℤ_ring)
32	31, 14	rhmmhm 20417	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
33	24, 32	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
34		neg1cn 12132	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
35		neg1ne0 12134	. . . . . . . . . . 11 ⊢ -1 ≠ 0
36		eqid 2735	. . . . . . . . . . . 12 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
37		eqid 2735	. . . . . . . . . . . 12 ⊢ ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0})) = ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))
38	36, 37	expghm 21432	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ -1 ≠ 0) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring GrpHom ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))))
39	34, 35, 38	mp2an 693	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring GrpHom ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0})))
40		ghmmhm 19157	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring GrpHom ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))))
41	39, 40	ax-mp 5	. . . . . . . . 9 ⊢ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0})))
42		cnring 21347	. . . . . . . . . 10 ⊢ ℂ_fld ∈ Ring
43		cnfldbas 21315	. . . . . . . . . . . 12 ⊢ ℂ = (Base‘ℂ_fld)
44		cnfld0 21349	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘ℂ_fld)
45		cndrng 21355	. . . . . . . . . . . 12 ⊢ ℂ_fld ∈ DivRing
46	43, 44, 45	drngui 20670	. . . . . . . . . . 11 ⊢ (ℂ ∖ {0}) = (Unit‘ℂ_fld)
47	46, 36	unitsubm 20324	. . . . . . . . . 10 ⊢ (ℂ_fld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
48	42, 47	ax-mp 5	. . . . . . . . 9 ⊢ (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld))
49	37	resmhm2 18748	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))) ∧ (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld)))
50	41, 48, 49	mp2an 693	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld))
51		zsubrg 21377	. . . . . . . . . 10 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
52	36	subrgsubm 20520	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
53	51, 52	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld))
54	29	fmpttd 7060	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)):ℤ⟶ℤ)
55	54	frnd 6669	. . . . . . . . 9 ⊢ (𝜑 → ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ)
56		eqid 2735	. . . . . . . . . 10 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = ((mulGrp‘ℂ_fld) ↾_s ℤ)
57	56	resmhm2b 18749	. . . . . . . . 9 ⊢ ((ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ) → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ))))
58	53, 55, 57	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ))))
59	50, 58	mpbii 233	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ)))
60		mhmco 18750	. . . . . . 7 ⊢ ((𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺) ∧ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ))) → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
61	33, 59, 60	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
62	30, 61	eqeltrrd 2836	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
63		lgseisen.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
64	63	gausslemma2dlem0a 27325	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℕ)
65	64	nnred 12162	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℝ)
66	6	gausslemma2dlem0a 27325	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℕ)
67	65, 66	nndivred 12201	. . . . . . . 8 ⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
68	67	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℝ)
69		2nn 12220	. . . . . . . . 9 ⊢ 2 ∈ ℕ
70		elfznn 13471	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
71	70	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
72		nnmulcl 12171	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
73	69, 71, 72	sylancr 588	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
74	73	nnred 12162	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℝ)
75	68, 74	remulcld 11164	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℝ)
76	75	flcld 13720	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
77		eqid 2735	. . . . . 6 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
78		fvexd 6848	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ V)
79		c0ex 11128	. . . . . . 7 ⊢ 0 ∈ V
80	79	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ V)
81	77, 19, 78, 80	fsuppmptdm 9281	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) finSupp 0)
82		oveq2 7366	. . . . . 6 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (-1↑𝑘) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
83	82	fveq2d 6837	. . . . 5 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
84		oveq2 7366	. . . . . 6 ⊢ (𝑘 = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (-1↑𝑘) = (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
85	84	fveq2d 6837	. . . . 5 ⊢ (𝑘 = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
86	1, 2, 5, 18, 19, 62, 76, 81, 83, 85	gsummhm2 19870	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
87	14, 25	mgpbas 20082	. . . . . . 7 ⊢ (Base‘𝑌) = (Base‘𝐺)
88		eqid 2735	. . . . . . . 8 ⊢ (._r‘𝑌) = (._r‘𝑌)
89	14, 88	mgpplusg 20081	. . . . . . 7 ⊢ (._r‘𝑌) = (+_g‘𝐺)
90	27	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
91		m1expcl 14011	. . . . . . . . 9 ⊢ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
92	76, 91	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
93	90, 92	ffvelcdmd 7030	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝑌))
94		neg1z 12529	. . . . . . . . . 10 ⊢ -1 ∈ ℤ
95		lgseisen.4	. . . . . . . . . . 11 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
96	63	eldifad 3912	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ ℙ)
97	96	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
98		prmz 16604	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
99	97, 98	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
100	73	nnzd 12516	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
101	99, 100	zmulcld 12604	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
102	7	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
103		prmnn 16603	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
104	102, 103	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
105	101, 104	zmodcld 13814	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
106	95, 105	eqeltrid 2839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
107		zexpcl 14001	. . . . . . . . . 10 ⊢ ((-1 ∈ ℤ ∧ 𝑅 ∈ ℕ₀) → (-1↑𝑅) ∈ ℤ)
108	94, 106, 107	sylancr 588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
109	108, 99	zmulcld 12604	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
110	90, 109	ffvelcdmd 7030	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
111		eqid 2735	. . . . . . 7 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
112		eqid 2735	. . . . . . 7 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
113	87, 89, 16, 19, 93, 110, 111, 112	gsummptfidmadd2 19857	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))))
114		eqidd 2736	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
115		eqidd 2736	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
116	19, 93, 110, 114, 115	offval2 7642	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))))
117	24	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
118		zringmulr 21414	. . . . . . . . . . . 12 ⊢ · = (._r‘ℤ_ring)
119	1, 118, 88	rhmmul 20423	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
120	117, 92, 109, 119	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
121	101	zred 12598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
122	104	nnrpd 12949	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ⁺)
123		modval 13793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
124	121, 122, 123	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
125	95, 124	eqtrid 2782	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
126	99	zcnd 12599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
127	73	nncnd 12163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
128	104	nncnd 12163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
129	104	nnne0d 12197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ≠ 0)
130	126, 127, 128, 129	div23d 11956	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑥)))
131	130	fveq2d 6837	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
132	131	oveq2d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))) = (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
133	132	oveq2d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
134	125, 133	eqtrd 2770	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
135	134	oveq2d 7374	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
136		prmz 16604	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
137	102, 136	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
138	137, 76	zmulcld 12604	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
139	138	zcnd 12599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
140	101	zcnd 12599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℂ)
141	139, 140	pncan3d 11497	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑄 · (2 · 𝑥)))
142		2cnd 12225	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
143	71	nncnd 12163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℂ)
144	126, 142, 143	mul12d 11344	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) = (2 · (𝑄 · 𝑥)))
145	135, 141, 144	3eqtrd 2774	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = (2 · (𝑄 · 𝑥)))
146	145	oveq2d 7374	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = (-1↑(2 · (𝑄 · 𝑥))))
147	34	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈ ℂ)
148	35	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ≠ 0)
149	106	nn0zd 12515	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
150		expaddz 14031	. . . . . . . . . . . . . . . 16 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ 𝑅 ∈ ℤ)) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
151	147, 148, 138, 149, 150	syl22anc 839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
152		expmulz 14033	. . . . . . . . . . . . . . . . . 18 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑃 ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
153	147, 148, 137, 76, 152	syl22anc 839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
154		1cnd 11129	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℂ)
155		eldifsni 4745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
156	6, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ≠ 2)
157	156	necomd 2986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 2 ≠ 𝑃)
158	157	neneqd 2936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 2 = 𝑃)
159	158	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 = 𝑃)
160		2z 12525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℤ
161		uzid 12768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
162	160, 161	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (ℤ_≥‘2)
163		dvdsprm 16632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
164	162, 102, 163	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
165	159, 164	mtbird 325	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 ∥ 𝑃)
166		oexpneg 16274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (-1↑𝑃) = -(1↑𝑃))
167	154, 104, 165, 166	syl3anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -(1↑𝑃))
168		1exp 14016	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → (1↑𝑃) = 1)
169	137, 168	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑𝑃) = 1)
170	169	negeqd 11376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -(1↑𝑃) = -1)
171	167, 170	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -1)
172	171	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
173	153, 172	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
174	173	oveq1d 7373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
175	151, 174	eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
176		nnmulcl 12171	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (𝑄 · 𝑥) ∈ ℕ)
177	64, 70, 176	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ)
178	177	nnnn0d 12464	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ₀)
179		2nn0 12420	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
180	179	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ₀)
181	147, 178, 180	expmuld 14074	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = ((-1↑2)↑(𝑄 · 𝑥)))
182		neg1sqe1 14121	. . . . . . . . . . . . . . . . 17 ⊢ (-1↑2) = 1
183	182	oveq1i 7368	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑2)↑(𝑄 · 𝑥)) = (1↑(𝑄 · 𝑥))
184	177	nnzd 12516	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℤ)
185		1exp 14016	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 · 𝑥) ∈ ℤ → (1↑(𝑄 · 𝑥)) = 1)
186	184, 185	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑(𝑄 · 𝑥)) = 1)
187	183, 186	eqtrid 2782	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑2)↑(𝑄 · 𝑥)) = 1)
188	181, 187	eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = 1)
189	146, 175, 188	3eqtr3d 2778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) = 1)
190	189	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = (1 · 𝑄))
191	92	zcnd 12599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
192	108	zcnd 12599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
193	191, 192, 126	mulassd 11157	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)))
194	126	mullidd 11152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑄) = 𝑄)
195	190, 193, 194	3eqtr3d 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)) = 𝑄)
196	195	fveq2d 6837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
197	120, 196	eqtr3d 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
198	197	mpteq2dva 5190	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
199	116, 198	eqtrd 2770	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
200	199	oveq2d 7374	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_f (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))))
201		lgseisen.3	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
202		lgseisen.5	. . . . . . . 8 ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
203		lgseisen.6	. . . . . . . 8 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
204	6, 63, 201, 95, 202, 203, 8, 14, 22	lgseisenlem3 27346	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))
205	204	oveq2d 7374	. . . . . 6 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)))
206	113, 200, 205	3eqtr3rd 2779	. . . . 5 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))))
207		eqid 2735	. . . . . . 7 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
208	93	fmpttd 7060	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
209		fvexd 6848	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ V)
210		fvexd 6848	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝐺) ∈ V)
211	111, 19, 209, 210	fsuppmptdm 9281	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) finSupp (0_g‘𝐺))
212	87, 207, 16, 19, 208, 211	gsumcl 19846	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌))
213		eqid 2735	. . . . . . 7 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
214	25, 88, 213	ringridm 20207	. . . . . 6 ⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌)) → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
215	21, 212, 214	syl2anc 585	. . . . 5 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
216	96, 98	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℤ)
217	27, 216	ffvelcdmd 7030	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝑌))
218		eqid 2735	. . . . . . . 8 ⊢ (._g‘𝐺) = (._g‘𝐺)
219	87, 218	gsumconst 19865	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ (1...((𝑃 − 1) / 2)) ∈ Fin ∧ (𝐿‘𝑄) ∈ (Base‘𝑌)) → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = ((♯‘(1...((𝑃 − 1) / 2)))(._g‘𝐺)(𝐿‘𝑄)))
220	18, 19, 217, 219	syl3anc 1374	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = ((♯‘(1...((𝑃 − 1) / 2)))(._g‘𝐺)(𝐿‘𝑄)))
221		oddprm 16740	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
222	6, 221	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
223	222	nnnn0d 12464	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
224		hashfz1 14271	. . . . . . . 8 ⊢ (((𝑃 − 1) / 2) ∈ ℕ₀ → (♯‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) / 2))
225	223, 224	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) / 2))
226	225	oveq1d 7373	. . . . . 6 ⊢ (𝜑 → ((♯‘(1...((𝑃 − 1) / 2)))(._g‘𝐺)(𝐿‘𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
227	31, 1	mgpbas 20082	. . . . . . . . 9 ⊢ ℤ = (Base‘((mulGrp‘ℂ_fld) ↾_s ℤ))
228		eqid 2735	. . . . . . . . 9 ⊢ (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ)) = (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))
229	227, 228, 218	mhmmulg 19047	. . . . . . . 8 ⊢ ((𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
230	33, 223, 216, 229	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
231	53	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
232		eqid 2735	. . . . . . . . . . 11 ⊢ (._g‘(mulGrp‘ℂ_fld)) = (._g‘(mulGrp‘ℂ_fld))
233	232, 56, 228	submmulg 19050	. . . . . . . . . 10 ⊢ ((ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
234	231, 223, 216, 233	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
235	216	zcnd 12599	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℂ)
236		cnfldexp 21361	. . . . . . . . . 10 ⊢ ((𝑄 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
237	235, 223, 236	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
238	234, 237	eqtr3d 2772	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
239	238	fveq2d 6837	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
240	230, 239	eqtr3d 2772	. . . . . 6 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
241	220, 226, 240	3eqtrd 2774	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
242	206, 215, 241	3eqtr3d 2778	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
243		subrgsubg 20512	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubGrp‘ℂ_fld))
244	51, 243	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubGrp‘ℂ_fld)
245		subgsubm 19080	. . . . . . . . 9 ⊢ (ℤ ∈ (SubGrp‘ℂ_fld) → ℤ ∈ (SubMnd‘ℂ_fld))
246	244, 245	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ℤ ∈ (SubMnd‘ℂ_fld))
247	76	fmpttd 7060	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))):(1...((𝑃 − 1) / 2))⟶ℤ)
248		df-zring 21404	. . . . . . . 8 ⊢ ℤ_ring = (ℂ_fld ↾_s ℤ)
249	19, 246, 247, 248	gsumsubm 18762	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
250	76	zcnd 12599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℂ)
251	19, 250	gsumfsum 21391	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
252	249, 251	eqtr3d 2772	. . . . . 6 ⊢ (𝜑 → (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
253	252	oveq2d 7374	. . . . 5 ⊢ (𝜑 → (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
254	253	fveq2d 6837	. . . 4 ⊢ (𝜑 → (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
255	86, 242, 254	3eqtr3d 2778	. . 3 ⊢ (𝜑 → (𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
256	66	nnnn0d 12464	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
257		zexpcl 14001	. . . . 5 ⊢ ((𝑄 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
258	216, 223, 257	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
259	19, 76	fsumzcl 15660	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
260		m1expcl 14011	. . . . 5 ⊢ (Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
261	259, 260	syl 17	. . . 4 ⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
262	8, 22	zndvds 21506	. . . 4 ⊢ ((𝑃 ∈ ℕ₀ ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
263	256, 258, 261, 262	syl3anc 1374	. . 3 ⊢ (𝜑 → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
264	255, 263	mpbid 232	. 2 ⊢ (𝜑 → 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
265		moddvds 16192	. . 3 ⊢ ((𝑃 ∈ ℕ ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
266	66, 258, 261, 265	syl3anc 1374	. 2 ⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
267	264, 266	mpbird 257	1 ⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2931 Vcvv 3439 ∖ cdif 3897 ⊆ wss 3900 {csn 4579 class class class wbr 5097 ↦ cmpt 5178 ran crn 5624 ∘ ccom 5627 ⟶wf 6487 ‘cfv 6491 (class class class)co 7358 ∘_f cof 7620 Fincfn 8885 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 − cmin 11366 -cneg 11367 / cdiv 11796 ℕcn 12147 2c2 12202 ℕ₀cn0 12403 ℤcz 12490 ℤ_≥cuz 12753 ℝ⁺crp 12907 ...cfz 13425 ⌊cfl 13712 mod cmo 13791 ↑cexp 13986 ♯chash 14255 Σcsu 15611 ∥ cdvds 16181 ℙcprime 16600 Basecbs 17138 ↾_s cress 17159 ._rcmulr 17180 0_gc0g 17361 Σ_g cgsu 17362 Mndcmnd 18661 MndHom cmhm 18708 SubMndcsubmnd 18709 ._gcmg 18999 SubGrpcsubg 19052 GrpHom cghm 19143 CMndccmn 19711 Abelcabl 19712 mulGrpcmgp 20077 1_rcur 20118 Ringcrg 20170 CRingccrg 20171 RingHom crh 20407 SubRingcsubrg 20504 DivRingcdr 20664 Fieldcfield 20665 ℂ_fldccnfld 21311 ℤ_ringczring 21403 ℤRHomczrh 21456 ℤ/nℤczn 21459

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2183 ax-ext 2707 ax-rep 5223 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680 ax-inf2 9552 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107 ax-mulf 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3349 df-reu 3350 df-rab 3399 df-v 3441 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4902 df-iun 4947 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6258 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-isom 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-tpos 8168 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-oadd 8401 df-er 8635 df-ec 8637 df-qs 8641 df-map 8767 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-fsupp 9267 df-sup 9347 df-inf 9348 df-oi 9417 df-dju 9815 df-card 9853 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-7 12215 df-8 12216 df-9 12217 df-n0 12404 df-xnn0 12477 df-z 12491 df-dec 12610 df-uz 12754 df-rp 12908 df-fz 13426 df-fzo 13573 df-fl 13714 df-mod 13792 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-clim 15413 df-sum 15612 df-dvds 16182 df-gcd 16424 df-prm 16601 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-0g 17363 df-gsum 17364 df-imas 17431 df-qus 17432 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mhm 18710 df-submnd 18711 df-grp 18868 df-minusg 18869 df-sbg 18870 df-mulg 19000 df-subg 19055 df-nsg 19056 df-eqg 19057 df-ghm 19144 df-cntz 19248 df-cmn 19713 df-abl 19714 df-mgp 20078 df-rng 20090 df-ur 20119 df-ring 20172 df-cring 20173 df-oppr 20275 df-dvdsr 20295 df-unit 20296 df-invr 20326 df-dvr 20339 df-rhm 20410 df-nzr 20448 df-subrng 20481 df-subrg 20505 df-rlreg 20629 df-domn 20630 df-idom 20631 df-drng 20666 df-field 20667 df-lmod 20815 df-lss 20885 df-lsp 20925 df-sra 21127 df-rgmod 21128 df-lidl 21165 df-rsp 21166 df-2idl 21207 df-cnfld 21312 df-zring 21404 df-zrh 21460 df-zn 21463

This theorem is referenced by: lgseisen 27348

W3C validator