lgseisenlem4 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lgseisenlem4		GIF version

Theorem lgseisenlem4 15805

Description: Lemma for lgseisen 15806. (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 variables 𝑘 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zringbas 14613	. . . . 5 ⊢ ℤ = (Base‘ℤ_ring)
2		zring0 14617	. . . . 5 ⊢ 0 = (0_g‘ℤ_ring)
3		zringabl 14611	. . . . . 6 ⊢ ℤ_ring ∈ Abel
4		ablcmn 13880	. . . . . 6 ⊢ (ℤ_ring ∈ Abel → ℤ_ring ∈ CMnd)
5	3, 4	mp1i 10	. . . . 5 ⊢ (𝜑 → ℤ_ring ∈ CMnd)
6		lgseisen.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
7	6	eldifad 3211	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℙ)
8		prmnn 12684	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	8	nnnn0d 9455	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ₀)
10	7, 9	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
11		lgseisen.7	. . . . . . . . 9 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
12	11	zncrng 14662	. . . . . . . 8 ⊢ (𝑃 ∈ ℕ₀ → 𝑌 ∈ CRing)
13	10, 12	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ CRing)
14		lgseisen.8	. . . . . . . 8 ⊢ 𝐺 = (mulGrp‘𝑌)
15	14	crngmgp 14020	. . . . . . 7 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
16	13, 15	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ CMnd)
17	16	cmnmndd 13897	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Mnd)
18		1zzd 9506	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
19		oddprm 12834	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
20	6, 19	syl 14	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
21	20	nnzd 9601	. . . . 5 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℤ)
22	13	crngringd 14025	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ Ring)
23		lgseisen.9	. . . . . . . . . 10 ⊢ 𝐿 = (ℤRHom‘𝑌)
24	23	zrhrhm 14640	. . . . . . . . 9 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
25	22, 24	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
26		eqid 2231	. . . . . . . . 9 ⊢ (Base‘𝑌) = (Base‘𝑌)
27	1, 26	rhmf 14180	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
28	25, 27	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
29		m1expcl 10825	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → (-1↑𝑘) ∈ ℤ)
30	29	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℤ)
31	28, 30	cofmpt 5816	. . . . . 6 ⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) = (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))))
32		zringmpg 14623	. . . . . . . . 9 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = (mulGrp‘ℤ_ring)
33	32, 14	rhmmhm 14176	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
34	25, 33	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
35		neg1cn 9248	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
36		neg1ap0 9252	. . . . . . . . . . 11 ⊢ -1 # 0
37		eqid 2231	. . . . . . . . . . . 12 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
38		eqid 2231	. . . . . . . . . . . 12 ⊢ ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0}) = ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0})
39	37, 38	expghmap 14624	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ -1 # 0) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring GrpHom ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0})))
40	35, 36, 39	mp2an 426	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring GrpHom ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0}))
41		ghmmhm 13842	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring GrpHom ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0})) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0})))
42	40, 41	ax-mp 5	. . . . . . . . 9 ⊢ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0}))
43		cnring 14587	. . . . . . . . . 10 ⊢ ℂ_fld ∈ Ring
44		cnfldui 14606	. . . . . . . . . . 11 ⊢ {𝑧 ∈ ℂ ∣ 𝑧 # 0} = (Unit‘ℂ_fld)
45	44, 37	unitsubm 14136	. . . . . . . . . 10 ⊢ (ℂ_fld ∈ Ring → {𝑧 ∈ ℂ ∣ 𝑧 # 0} ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
46	43, 45	ax-mp 5	. . . . . . . . 9 ⊢ {𝑧 ∈ ℂ ∣ 𝑧 # 0} ∈ (SubMnd‘(mulGrp‘ℂ_fld))
47	38	resmhm2 13573	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0})) ∧ {𝑧 ∈ ℂ ∣ 𝑧 # 0} ∈ (SubMnd‘(mulGrp‘ℂ_fld))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld)))
48	42, 46, 47	mp2an 426	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld))
49		zsubrg 14598	. . . . . . . . . 10 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
50	37	subrgsubm 14251	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
51	49, 50	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld))
52	30	fmpttd 5802	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)):ℤ⟶ℤ)
53	52	frnd 5492	. . . . . . . . 9 ⊢ (𝜑 → ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ)
54		eqid 2231	. . . . . . . . . 10 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = ((mulGrp‘ℂ_fld) ↾_s ℤ)
55	54	resmhm2b 13574	. . . . . . . . 9 ⊢ ((ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ) → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ))))
56	51, 53, 55	sylancr 414	. . . . . . . 8 ⊢ (𝜑 → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom (mulGrp‘ℂ_fld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ))))
57	48, 56	mpbii 148	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ)))
58		mhmco 13575	. . . . . . 7 ⊢ ((𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺) ∧ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈ (ℤ_ring MndHom ((mulGrp‘ℂ_fld) ↾_s ℤ))) → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
59	34, 57, 58	syl2anc 411	. . . . . 6 ⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
60	31, 59	eqeltrrd 2309	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
61		lgseisen.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
62	61	gausslemma2dlem0a 15781	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℕ)
63	62	nnzd 9601	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℤ)
64	63	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
65	6	gausslemma2dlem0a 15781	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℕ)
66	65	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
67		znq 9858	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑄 / 𝑃) ∈ ℚ)
68	64, 66, 67	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℚ)
69		2nn 9305	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
70		elfznn 10289	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
71	70	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
72		nnmulcl 9164	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
73	69, 71, 72	sylancr 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
74	73	nnzd 9601	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
75		zq 9860	. . . . . . . 8 ⊢ ((2 · 𝑥) ∈ ℤ → (2 · 𝑥) ∈ ℚ)
76	74, 75	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℚ)
77		qmulcl 9871	. . . . . . 7 ⊢ (((𝑄 / 𝑃) ∈ ℚ ∧ (2 · 𝑥) ∈ ℚ) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℚ)
78	68, 76, 77	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℚ)
79	78	flqcld 10538	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
80		oveq2 6026	. . . . . 6 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (-1↑𝑘) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
81	80	fveq2d 5643	. . . . 5 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
82		oveq2 6026	. . . . . 6 ⊢ (𝑘 = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (-1↑𝑘) = (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
83	82	fveq2d 5643	. . . . 5 ⊢ (𝑘 = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
84	1, 2, 5, 17, 18, 21, 60, 79, 81, 83	gsumfzmhm2 13933	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
85		eqid 2231	. . . . . . . 8 ⊢ (Base‘𝐺) = (Base‘𝐺)
86		eqid 2231	. . . . . . . 8 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
87	28	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
88		m1expcl 10825	. . . . . . . . . . 11 ⊢ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
89	79, 88	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
90	87, 89	ffvelcdmd 5783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝑌))
91	14, 26	mgpbasg 13942	. . . . . . . . . . 11 ⊢ (𝑌 ∈ CRing → (Base‘𝑌) = (Base‘𝐺))
92	13, 91	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑌) = (Base‘𝐺))
93	92	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (Base‘𝑌) = (Base‘𝐺))
94	90, 93	eleqtrd 2310	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝐺))
95		neg1z 9511	. . . . . . . . . . . 12 ⊢ -1 ∈ ℤ
96		lgseisen.4	. . . . . . . . . . . . 13 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
97	61	eldifad 3211	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℙ)
98	97	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
99		prmz 12685	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
100	98, 99	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
101	100, 74	zmulcld 9608	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
102	7	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
103	102, 8	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
104	101, 103	zmodcld 10608	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
105	96, 104	eqeltrid 2318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
106		zexpcl 10817	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℤ ∧ 𝑅 ∈ ℕ₀) → (-1↑𝑅) ∈ ℤ)
107	95, 105, 106	sylancr 414	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
108	107, 100	zmulcld 9608	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
109	87, 108	ffvelcdmd 5783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
110	109, 93	eleqtrd 2310	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝐺))
111		eqid 2231	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
112		eqid 2231	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
113	85, 86, 16, 18, 21, 94, 110, 111, 112	gsumfzmptfidmadd2 13929	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(+_g‘𝐺)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))))
114		eqid 2231	. . . . . . . . . . . 12 ⊢ (._r‘𝑌) = (._r‘𝑌)
115	14, 114	mgpplusgg 13940	. . . . . . . . . . 11 ⊢ (𝑌 ∈ CRing → (._r‘𝑌) = (+_g‘𝐺))
116	13, 115	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝑌) = (+_g‘𝐺))
117	116	ofeqd 6237	. . . . . . . . 9 ⊢ (𝜑 → ∘_𝑓 (._r‘𝑌) = ∘_𝑓 (+_g‘𝐺))
118	117	oveqd 6035	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))
119	118	oveq2d 6034	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))))
120	116	oveqd 6035	. . . . . . 7 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(+_g‘𝐺)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))))
121	113, 119, 120	3eqtr4d 2274	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))))
122	18, 21	fzfigd 10694	. . . . . . . . 9 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
123		eqidd 2232	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
124		eqidd 2232	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
125	122, 90, 109, 123, 124	offval2 6251	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))))
126	25	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
127		zringmulr 14616	. . . . . . . . . . . 12 ⊢ · = (._r‘ℤ_ring)
128	1, 127, 114	rhmmul 14181	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
129	126, 89, 108, 128	syl3anc 1273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
130	62	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℕ)
131	130, 73	nnmulcld 9192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℕ)
132		nnq 9867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 · (2 · 𝑥)) ∈ ℕ → (𝑄 · (2 · 𝑥)) ∈ ℚ)
133	131, 132	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℚ)
134		nnq 9867	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
135	65, 134	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ ℚ)
136	135	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℚ)
137	66	nngt0d 9187	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 𝑃)
138		modqval 10587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
139	133, 136, 137, 138	syl3anc 1273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
140	96, 139	eqtrid 2276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
141	100	zcnd 9603	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
142	73	nncnd 9157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
143	103	nncnd 9157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
144	103	nnap0d 9189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 # 0)
145	141, 142, 143, 144	div23apd 9008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑥)))
146	145	fveq2d 5643	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
147	146	oveq2d 6034	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))) = (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
148	147	oveq2d 6034	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
149	140, 148	eqtrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
150	149	oveq2d 6034	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
151		prmz 12685	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
152	102, 151	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
153	152, 79	zmulcld 9608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
154	153	zcnd 9603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
155	101	zcnd 9603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℂ)
156	154, 155	pncan3d 8493	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑄 · (2 · 𝑥)))
157		2cnd 9216	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
158	71	nncnd 9157	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℂ)
159	141, 157, 158	mul12d 8331	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) = (2 · (𝑄 · 𝑥)))
160	150, 156, 159	3eqtrd 2268	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = (2 · (𝑄 · 𝑥)))
161	160	oveq2d 6034	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = (-1↑(2 · (𝑄 · 𝑥))))
162	35	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈ ℂ)
163	36	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 # 0)
164	105	nn0zd 9600	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
165		expaddzap 10846	. . . . . . . . . . . . . . . 16 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ 𝑅 ∈ ℤ)) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
166	162, 163, 153, 164, 165	syl22anc 1274	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
167		expmulzap 10848	. . . . . . . . . . . . . . . . . 18 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ (𝑃 ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
168	162, 163, 152, 79, 167	syl22anc 1274	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
169		1cnd 8195	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℂ)
170		eldifsni 3802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
171	6, 170	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ≠ 2)
172	171	necomd 2488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 2 ≠ 𝑃)
173	172	neneqd 2423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 2 = 𝑃)
174	173	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 = 𝑃)
175		2z 9507	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℤ
176		uzid 9770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
177	175, 176	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (ℤ_≥‘2)
178		dvdsprm 12711	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
179	177, 102, 178	sylancr 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
180	174, 179	mtbird 679	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 ∥ 𝑃)
181		oexpneg 12440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (-1↑𝑃) = -(1↑𝑃))
182	169, 103, 180, 181	syl3anc 1273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -(1↑𝑃))
183		1exp 10831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → (1↑𝑃) = 1)
184	152, 183	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑𝑃) = 1)
185	184	negeqd 8374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -(1↑𝑃) = -1)
186	182, 185	eqtrd 2264	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -1)
187	186	oveq1d 6033	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
188	168, 187	eqtrd 2264	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
189	188	oveq1d 6033	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
190	166, 189	eqtrd 2264	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
191		nnmulcl 9164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (𝑄 · 𝑥) ∈ ℕ)
192	62, 70, 191	syl2an 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ)
193	192	nnnn0d 9455	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ₀)
194		2nn0 9419	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
195	194	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ₀)
196	162, 193, 195	expmuld 10939	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = ((-1↑2)↑(𝑄 · 𝑥)))
197		neg1sqe1 10897	. . . . . . . . . . . . . . . . 17 ⊢ (-1↑2) = 1
198	197	oveq1i 6028	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑2)↑(𝑄 · 𝑥)) = (1↑(𝑄 · 𝑥))
199	192	nnzd 9601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℤ)
200		1exp 10831	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 · 𝑥) ∈ ℤ → (1↑(𝑄 · 𝑥)) = 1)
201	199, 200	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑(𝑄 · 𝑥)) = 1)
202	198, 201	eqtrid 2276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑2)↑(𝑄 · 𝑥)) = 1)
203	196, 202	eqtrd 2264	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = 1)
204	161, 190, 203	3eqtr3d 2272	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) = 1)
205	204	oveq1d 6033	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = (1 · 𝑄))
206	89	zcnd 9603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
207	107	zcnd 9603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
208	206, 207, 141	mulassd 8203	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)))
209	141	mullidd 8197	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑄) = 𝑄)
210	205, 208, 209	3eqtr3d 2272	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)) = 𝑄)
211	210	fveq2d 5643	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
212	129, 211	eqtr3d 2266	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
213	212	mpteq2dva 4179	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
214	125, 213	eqtrd 2264	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
215	214	oveq2d 6034	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))))
216		lgseisen.3	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
217		lgseisen.5	. . . . . . . 8 ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
218		lgseisen.6	. . . . . . . 8 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
219	6, 61, 216, 96, 217, 218, 11, 14, 23	lgseisenlem3 15804	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))
220	219	oveq2d 6034	. . . . . 6 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)))
221	121, 215, 220	3eqtr3rd 2273	. . . . 5 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))))
222		eqid 2231	. . . . . . . 8 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
223	90	fmpttd 5802	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
224	92	feq3d 5471	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌) ↔ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝐺)))
225	223, 224	mpbid 147	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝐺))
226	85, 222, 17, 18, 21, 225	gsumfzcl 13584	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝐺))
227	226, 92	eleqtrrd 2311	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌))
228		eqid 2231	. . . . . . 7 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
229	26, 114, 228	ringridm 14040	. . . . . 6 ⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌)) → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
230	22, 227, 229	syl2anc 411	. . . . 5 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
231		nnuz 9792	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
232	20, 231	eleqtrdi 2324	. . . . . . 7 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ (ℤ_≥‘1))
233	97, 99	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℤ)
234	28, 233	ffvelcdmd 5783	. . . . . . . 8 ⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝑌))
235	234, 92	eleqtrd 2310	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝐺))
236		eqid 2231	. . . . . . . 8 ⊢ (._g‘𝐺) = (._g‘𝐺)
237	85, 236	gsumfzconst 13930	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ ((𝑃 − 1) / 2) ∈ (ℤ_≥‘1) ∧ (𝐿‘𝑄) ∈ (Base‘𝐺)) → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)))
238	17, 232, 235, 237	syl3anc 1273	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)))
239	20	nncnd 9157	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℂ)
240		1cnd 8195	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
241	239, 240	npcand 8494	. . . . . . 7 ⊢ (𝜑 → ((((𝑃 − 1) / 2) − 1) + 1) = ((𝑃 − 1) / 2))
242	241	oveq1d 6033	. . . . . 6 ⊢ (𝜑 → (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
243	20	nnnn0d 9455	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
244		zringring 14610	. . . . . . . . . 10 ⊢ ℤ_ring ∈ Ring
245	32, 1	mgpbasg 13942	. . . . . . . . . 10 ⊢ (ℤ_ring ∈ Ring → ℤ = (Base‘((mulGrp‘ℂ_fld) ↾_s ℤ)))
246	244, 245	ax-mp 5	. . . . . . . . 9 ⊢ ℤ = (Base‘((mulGrp‘ℂ_fld) ↾_s ℤ))
247		eqid 2231	. . . . . . . . 9 ⊢ (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ)) = (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))
248	246, 247, 236	mhmmulg 13752	. . . . . . . 8 ⊢ ((𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
249	34, 243, 233, 248	syl3anc 1273	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
250	51	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
251		eqid 2231	. . . . . . . . . . 11 ⊢ (._g‘(mulGrp‘ℂ_fld)) = (._g‘(mulGrp‘ℂ_fld))
252	251, 54, 247	submmulg 13755	. . . . . . . . . 10 ⊢ ((ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
253	250, 243, 233, 252	syl3anc 1273	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
254	233	zcnd 9603	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℂ)
255		cnfldexp 14594	. . . . . . . . . 10 ⊢ ((𝑄 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
256	254, 243, 255	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
257	253, 256	eqtr3d 2266	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
258	257	fveq2d 5643	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
259	249, 258	eqtr3d 2266	. . . . . 6 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
260	238, 242, 259	3eqtrd 2268	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
261	221, 230, 260	3eqtr3d 2272	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
262		subrgsubg 14244	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubGrp‘ℂ_fld))
263	49, 262	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubGrp‘ℂ_fld)
264		subgsubm 13785	. . . . . . . . 9 ⊢ (ℤ ∈ (SubGrp‘ℂ_fld) → ℤ ∈ (SubMnd‘ℂ_fld))
265	263, 264	mp1i 10	. . . . . . . 8 ⊢ (𝜑 → ℤ ∈ (SubMnd‘ℂ_fld))
266	79	fmpttd 5802	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))):(1...((𝑃 − 1) / 2))⟶ℤ)
267		df-zring 14608	. . . . . . . 8 ⊢ ℤ_ring = (ℂ_fld ↾_s ℤ)
268	122, 265, 266, 267	gsumsubm 13579	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
269	79	zcnd 9603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℂ)
270	18, 21, 269	gsumfzfsum 14605	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
271	268, 270	eqtr3d 2266	. . . . . 6 ⊢ (𝜑 → (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
272	271	oveq2d 6034	. . . . 5 ⊢ (𝜑 → (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
273	272	fveq2d 5643	. . . 4 ⊢ (𝜑 → (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
274	84, 261, 273	3eqtr3d 2272	. . 3 ⊢ (𝜑 → (𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
275	65	nnnn0d 9455	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
276		zexpcl 10817	. . . . 5 ⊢ ((𝑄 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
277	233, 243, 276	syl2anc 411	. . . 4 ⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
278	122, 79	fsumzcl 11965	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
279		m1expcl 10825	. . . . 5 ⊢ (Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
280	278, 279	syl 14	. . . 4 ⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
281	11, 23	zndvds 14666	. . . 4 ⊢ ((𝑃 ∈ ℕ₀ ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
282	275, 277, 280, 281	syl3anc 1273	. . 3 ⊢ (𝜑 → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
283	274, 282	mpbid 147	. 2 ⊢ (𝜑 → 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
284		moddvds 12362	. . 3 ⊢ ((𝑃 ∈ ℕ ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
285	65, 277, 280, 284	syl3anc 1273	. 2 ⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) − (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
286	283, 285	mpbird 167	1 ⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1397 ∈ wcel 2202 ≠ wne 2402 {crab 2514 ∖ cdif 3197 ⊆ wss 3200 {csn 3669 class class class wbr 4088 ↦ cmpt 4150 ran crn 4726 ∘ ccom 4729 ⟶wf 5322 ‘cfv 5326 (class class class)co 6018 ∘_𝑓 cof 6233 Fincfn 6909 ℂcc 8030 0cc0 8032 1c1 8033 + caddc 8035 · cmul 8037 < clt 8214 − cmin 8350 -cneg 8351 # cap 8761 / cdiv 8852 ℕcn 9143 2c2 9194 ℕ₀cn0 9402 ℤcz 9479 ℤ_≥cuz 9755 ℚcq 9853 ...cfz 10243 ⌊cfl 10529 mod cmo 10585 ↑cexp 10801 Σcsu 11915 ∥ cdvds 12350 ℙcprime 12681 Basecbs 13084 ↾_s cress 13085 +_gcplusg 13162 ._rcmulr 13163 0_gc0g 13341 Σ_g cgsu 13342 Mndcmnd 13501 MndHom cmhm 13542 SubMndcsubmnd 13543 ._gcmg 13708 SubGrpcsubg 13756 GrpHom cghm 13829 CMndccmn 13873 Abelcabl 13874 mulGrpcmgp 13936 1_rcur 13975 Ringcrg 14012 CRingccrg 14013 RingHom crh 14167 SubRingcsubrg 14234 ℂ_fldccnfld 14573 ℤ_ringczring 14607 ℤRHomczrh 14628 ℤ/nℤczn 14630

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8123 ax-resscn 8124 ax-1cn 8125 ax-1re 8126 ax-icn 8127 ax-addcl 8128 ax-addrcl 8129 ax-mulcl 8130 ax-mulrcl 8131 ax-addcom 8132 ax-mulcom 8133 ax-addass 8134 ax-mulass 8135 ax-distr 8136 ax-i2m1 8137 ax-0lt1 8138 ax-1rid 8139 ax-0id 8140 ax-rnegex 8141 ax-precex 8142 ax-cnre 8143 ax-pre-ltirr 8144 ax-pre-ltwlin 8145 ax-pre-lttrn 8146 ax-pre-apti 8147 ax-pre-ltadd 8148 ax-pre-mulgt0 8149 ax-pre-mulext 8150 ax-arch 8151 ax-caucvg 8152 ax-addf 8154 ax-mulf 8155

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-xor 1420 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-tp 3677 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5971 df-ov 6021 df-oprab 6022 df-mpo 6023 df-of 6235 df-1st 6303 df-2nd 6304 df-tpos 6411 df-recs 6471 df-irdg 6536 df-frec 6557 df-1o 6582 df-2o 6583 df-oadd 6586 df-er 6702 df-ec 6704 df-qs 6708 df-map 6819 df-en 6910 df-dom 6911 df-fin 6912 df-sup 7183 df-pnf 8216 df-mnf 8217 df-xr 8218 df-ltxr 8219 df-le 8220 df-sub 8352 df-neg 8353 df-reap 8755 df-ap 8762 df-div 8853 df-inn 9144 df-2 9202 df-3 9203 df-4 9204 df-5 9205 df-6 9206 df-7 9207 df-8 9208 df-9 9209 df-n0 9403 df-z 9480 df-dec 9612 df-uz 9756 df-q 9854 df-rp 9889 df-fz 10244 df-fzo 10378 df-fl 10531 df-mod 10586 df-seqfrec 10711 df-exp 10802 df-ihash 11039 df-cj 11404 df-re 11405 df-im 11406 df-rsqrt 11560 df-abs 11561 df-clim 11841 df-sumdc 11916 df-dvds 12351 df-gcd 12527 df-prm 12682 df-struct 13086 df-ndx 13087 df-slot 13088 df-base 13090 df-sets 13091 df-iress 13092 df-plusg 13175 df-mulr 13176 df-starv 13177 df-sca 13178 df-vsca 13179 df-ip 13180 df-tset 13181 df-ple 13182 df-ds 13184 df-unif 13185 df-0g 13343 df-igsum 13344 df-topgen 13345 df-iimas 13387 df-qus 13388 df-mgm 13441 df-sgrp 13487 df-mnd 13502 df-mhm 13544 df-submnd 13545 df-grp 13588 df-minusg 13589 df-sbg 13590 df-mulg 13709 df-subg 13759 df-nsg 13760 df-eqg 13761 df-ghm 13830 df-cmn 13875 df-abl 13876 df-mgp 13937 df-rng 13949 df-ur 13976 df-srg 13980 df-ring 14014 df-cring 14015 df-oppr 14084 df-dvdsr 14105 df-unit 14106 df-invr 14138 df-dvr 14149 df-rhm 14169 df-nzr 14197 df-subrg 14236 df-domn 14276 df-idom 14277 df-lmod 14306 df-lssm 14370 df-lsp 14404 df-sra 14452 df-rgmod 14453 df-lidl 14486 df-rsp 14487 df-2idl 14517 df-bl 14563 df-mopn 14564 df-fg 14566 df-metu 14567 df-cnfld 14574 df-zring 14608 df-zrh 14631 df-zn 14633

This theorem is referenced by: lgseisen 15806

W3C validator