lgseisenlem4 - Intuitionistic Logic Explorer

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

Theorem lgseisenlem4 15995

Description: Lemma for lgseisen 15996. (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 14793	. . . . 5 ⊢ ℤ = (Base‘ℤ_ring)
2		zring0 14797	. . . . 5 ⊢ 0 = (0_g‘ℤ_ring)
3		zringabl 14791	. . . . . 6 ⊢ ℤ_ring ∈ Abel
4		ablcmn 14029	. . . . . 6 ⊢ (ℤ_ring ∈ Abel → ℤ_ring ∈ CMnd)
5	3, 4	mp1i 10	. . . . 5 ⊢ (𝜑 → ℤ_ring ∈ CMnd)
6		lgseisen.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
7	6	eldifad 3224	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℙ)
8		prmnn 12815	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	8	nnnn0d 9558	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ₀)
10	7, 9	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
11		lgseisen.7	. . . . . . . . 9 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
12	11	zncrng 14842	. . . . . . . 8 ⊢ (𝑃 ∈ ℕ₀ → 𝑌 ∈ CRing)
13	10, 12	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ CRing)
14		lgseisen.8	. . . . . . . 8 ⊢ 𝐺 = (mulGrp‘𝑌)
15	14	crngmgp 14169	. . . . . . 7 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
16	13, 15	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ CMnd)
17	16	cmnmndd 14046	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Mnd)
18		1zzd 9609	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
19		oddprm 12965	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
20	6, 19	syl 14	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
21	20	nnzd 9705	. . . . 5 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℤ)
22	13	crngringd 14174	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ Ring)
23		lgseisen.9	. . . . . . . . . 10 ⊢ 𝐿 = (ℤRHom‘𝑌)
24	23	zrhrhm 14820	. . . . . . . . 9 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
25	22, 24	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
26		eqid 2234	. . . . . . . . 9 ⊢ (Base‘𝑌) = (Base‘𝑌)
27	1, 26	rhmf 14330	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
28	25, 27	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
29		m1expcl 10931	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → (-1↑𝑘) ∈ ℤ)
30	29	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℤ)
31	28, 30	cofmpt 5848	. . . . . 6 ⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) = (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))))
32		zringmpg 14803	. . . . . . . . 9 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = (mulGrp‘ℤ_ring)
33	32, 14	rhmmhm 14326	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
34	25, 33	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
35		neg1cn 9347	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
36		neg1ap0 9351	. . . . . . . . . . 11 ⊢ -1 # 0
37		eqid 2234	. . . . . . . . . . . 12 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
38		eqid 2234	. . . . . . . . . . . 12 ⊢ ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0}) = ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0})
39	37, 38	expghmap 14804	. . . . . . . . . . 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 13991	. . . . . . . . . 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 14767	. . . . . . . . . 10 ⊢ ℂ_fld ∈ Ring
44		cnfldui 14786	. . . . . . . . . . 11 ⊢ {𝑧 ∈ ℂ ∣ 𝑧 # 0} = (Unit‘ℂ_fld)
45	44, 37	unitsubm 14286	. . . . . . . . . 10 ⊢ (ℂ_fld ∈ Ring → {𝑧 ∈ ℂ ∣ 𝑧 # 0} ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
46	43, 45	ax-mp 5	. . . . . . . . 9 ⊢ {𝑧 ∈ ℂ ∣ 𝑧 # 0} ∈ (SubMnd‘(mulGrp‘ℂ_fld))
47	38	resmhm2 13722	. . . . . . . . 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 14778	. . . . . . . . . 10 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
50	37	subrgsubm 14402	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
51	49, 50	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld))
52	30	fmpttd 5834	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)):ℤ⟶ℤ)
53	52	frnd 5520	. . . . . . . . 9 ⊢ (𝜑 → ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ)
54		eqid 2234	. . . . . . . . . 10 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = ((mulGrp‘ℂ_fld) ↾_s ℤ)
55	54	resmhm2b 13723	. . . . . . . . 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 13724	. . . . . . 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 2312	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
61		lgseisen.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
62	61	gausslemma2dlem0a 15971	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℕ)
63	62	nnzd 9705	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℤ)
64	63	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
65	6	gausslemma2dlem0a 15971	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℕ)
66	65	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
67		znq 9962	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑄 / 𝑃) ∈ ℚ)
68	64, 66, 67	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℚ)
69		2nn 9404	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
70		elfznn 10394	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
71	70	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
72		nnmulcl 9263	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
73	69, 71, 72	sylancr 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
74	73	nnzd 9705	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
75		zq 9964	. . . . . . . 8 ⊢ ((2 · 𝑥) ∈ ℤ → (2 · 𝑥) ∈ ℚ)
76	74, 75	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℚ)
77		qmulcl 9975	. . . . . . 7 ⊢ (((𝑄 / 𝑃) ∈ ℚ ∧ (2 · 𝑥) ∈ ℚ) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℚ)
78	68, 76, 77	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℚ)
79	78	flqcld 10644	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
80		oveq2 6060	. . . . . 6 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (-1↑𝑘) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
81	80	fveq2d 5676	. . . . 5 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
82		oveq2 6060	. . . . . 6 ⊢ (𝑘 = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (-1↑𝑘) = (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
83	82	fveq2d 5676	. . . . 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 14082	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
85		eqid 2234	. . . . . . . 8 ⊢ (Base‘𝐺) = (Base‘𝐺)
86		eqid 2234	. . . . . . . 8 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
87	28	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
88		m1expcl 10931	. . . . . . . . . . 11 ⊢ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
89	79, 88	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
90	87, 89	ffvelcdmd 5815	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝑌))
91	14, 26	mgpbasg 14091	. . . . . . . . . . 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 2313	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝐺))
95		neg1z 9614	. . . . . . . . . . . 12 ⊢ -1 ∈ ℤ
96		lgseisen.4	. . . . . . . . . . . . 13 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
97	61	eldifad 3224	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℙ)
98	97	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
99		prmz 12816	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
100	98, 99	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
101	100, 74	zmulcld 9712	. . . . . . . . . . . . . 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 10714	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
105	96, 104	eqeltrid 2321	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
106		zexpcl 10923	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℤ ∧ 𝑅 ∈ ℕ₀) → (-1↑𝑅) ∈ ℤ)
107	95, 105, 106	sylancr 414	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
108	107, 100	zmulcld 9712	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
109	87, 108	ffvelcdmd 5815	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
110	109, 93	eleqtrd 2313	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝐺))
111		eqid 2234	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
112		eqid 2234	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
113	85, 86, 16, 18, 21, 94, 110, 111, 112	gsumfzmptfidmadd2 14078	. . . . . . 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 2234	. . . . . . . . . . . 12 ⊢ (._r‘𝑌) = (._r‘𝑌)
115	14, 114	mgpplusgg 14089	. . . . . . . . . . 11 ⊢ (𝑌 ∈ CRing → (._r‘𝑌) = (+_g‘𝐺))
116	13, 115	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝑌) = (+_g‘𝐺))
117	116	ofeqd 6270	. . . . . . . . 9 ⊢ (𝜑 → ∘_𝑓 (._r‘𝑌) = ∘_𝑓 (+_g‘𝐺))
118	117	oveqd 6069	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))
119	118	oveq2d 6068	. . . . . . 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 6069	. . . . . . 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 2277	. . . . . 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 10800	. . . . . . . . 9 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
123		eqidd 2235	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
124		eqidd 2235	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
125	122, 90, 109, 123, 124	offval2 6284	. . . . . . . 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 14796	. . . . . . . . . . . 12 ⊢ · = (._r‘ℤ_ring)
128	1, 127, 114	rhmmul 14331	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
129	126, 89, 108, 128	syl3anc 1274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
130	62	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℕ)
131	130, 73	nnmulcld 9291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℕ)
132		nnq 9971	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 · (2 · 𝑥)) ∈ ℕ → (𝑄 · (2 · 𝑥)) ∈ ℚ)
133	131, 132	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℚ)
134		nnq 9971	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
135	65, 134	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ ℚ)
136	135	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℚ)
137	66	nngt0d 9286	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 𝑃)
138		modqval 10693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
139	133, 136, 137, 138	syl3anc 1274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
140	96, 139	eqtrid 2279	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
141	100	zcnd 9707	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
142	73	nncnd 9256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
143	103	nncnd 9256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
144	103	nnap0d 9288	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 # 0)
145	141, 142, 143, 144	div23apd 9107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑥)))
146	145	fveq2d 5676	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
147	146	oveq2d 6068	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))) = (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
148	147	oveq2d 6068	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
149	140, 148	eqtrd 2267	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
150	149	oveq2d 6068	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
151		prmz 12816	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
152	102, 151	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
153	152, 79	zmulcld 9712	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
154	153	zcnd 9707	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
155	101	zcnd 9707	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℂ)
156	154, 155	pncan3d 8592	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑄 · (2 · 𝑥)))
157		2cnd 9315	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
158	71	nncnd 9256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℂ)
159	141, 157, 158	mul12d 8430	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) = (2 · (𝑄 · 𝑥)))
160	150, 156, 159	3eqtrd 2271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = (2 · (𝑄 · 𝑥)))
161	160	oveq2d 6068	. . . . . . . . . . . . . 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 9704	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
165		expaddzap 10952	. . . . . . . . . . . . . . . 16 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ 𝑅 ∈ ℤ)) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
166	162, 163, 153, 164, 165	syl22anc 1275	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
167		expmulzap 10954	. . . . . . . . . . . . . . . . . 18 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ (𝑃 ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
168	162, 163, 152, 79, 167	syl22anc 1275	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
169		1cnd 8295	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℂ)
170		eldifsni 3824	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
171	6, 170	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ≠ 2)
172	171	necomd 2500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 2 ≠ 𝑃)
173	172	neneqd 2435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 2 = 𝑃)
174	173	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 = 𝑃)
175		2z 9610	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℤ
176		uzid 9874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
177	175, 176	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (ℤ_≥‘2)
178		dvdsprm 12842	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
179	177, 102, 178	sylancr 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
180	174, 179	mtbird 680	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 ∥ 𝑃)
181		oexpneg 12571	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (-1↑𝑃) = -(1↑𝑃))
182	169, 103, 180, 181	syl3anc 1274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -(1↑𝑃))
183		1exp 10937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → (1↑𝑃) = 1)
184	152, 183	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑𝑃) = 1)
185	184	negeqd 8473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -(1↑𝑃) = -1)
186	182, 185	eqtrd 2267	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -1)
187	186	oveq1d 6067	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
188	168, 187	eqtrd 2267	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
189	188	oveq1d 6067	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
190	166, 189	eqtrd 2267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
191		nnmulcl 9263	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (𝑄 · 𝑥) ∈ ℕ)
192	62, 70, 191	syl2an 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ)
193	192	nnnn0d 9558	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ₀)
194		2nn0 9518	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
195	194	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ₀)
196	162, 193, 195	expmuld 11046	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = ((-1↑2)↑(𝑄 · 𝑥)))
197		neg1sqe1 11003	. . . . . . . . . . . . . . . . 17 ⊢ (-1↑2) = 1
198	197	oveq1i 6062	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑2)↑(𝑄 · 𝑥)) = (1↑(𝑄 · 𝑥))
199	192	nnzd 9705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℤ)
200		1exp 10937	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 · 𝑥) ∈ ℤ → (1↑(𝑄 · 𝑥)) = 1)
201	199, 200	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑(𝑄 · 𝑥)) = 1)
202	198, 201	eqtrid 2279	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑2)↑(𝑄 · 𝑥)) = 1)
203	196, 202	eqtrd 2267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = 1)
204	161, 190, 203	3eqtr3d 2275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) = 1)
205	204	oveq1d 6067	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = (1 · 𝑄))
206	89	zcnd 9707	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
207	107	zcnd 9707	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
208	206, 207, 141	mulassd 8302	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)))
209	141	mullidd 8297	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑄) = 𝑄)
210	205, 208, 209	3eqtr3d 2275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)) = 𝑄)
211	210	fveq2d 5676	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
212	129, 211	eqtr3d 2269	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
213	212	mpteq2dva 4202	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
214	125, 213	eqtrd 2267	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
215	214	oveq2d 6068	. . . . . 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 15994	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))
220	219	oveq2d 6068	. . . . . 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 2276	. . . . 5 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))))
222		eqid 2234	. . . . . . . 8 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
223	90	fmpttd 5834	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
224	92	feq3d 5499	. . . . . . . . 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 13733	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝐺))
227	226, 92	eleqtrrd 2314	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌))
228		eqid 2234	. . . . . . 7 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
229	26, 114, 228	ringridm 14189	. . . . . 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 9896	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
232	20, 231	eleqtrdi 2327	. . . . . . 7 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ (ℤ_≥‘1))
233	97, 99	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℤ)
234	28, 233	ffvelcdmd 5815	. . . . . . . 8 ⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝑌))
235	234, 92	eleqtrd 2313	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝐺))
236		eqid 2234	. . . . . . . 8 ⊢ (._g‘𝐺) = (._g‘𝐺)
237	85, 236	gsumfzconst 14079	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ ((𝑃 − 1) / 2) ∈ (ℤ_≥‘1) ∧ (𝐿‘𝑄) ∈ (Base‘𝐺)) → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)))
238	17, 232, 235, 237	syl3anc 1274	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)))
239	20	nncnd 9256	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℂ)
240		1cnd 8295	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
241	239, 240	npcand 8593	. . . . . . 7 ⊢ (𝜑 → ((((𝑃 − 1) / 2) − 1) + 1) = ((𝑃 − 1) / 2))
242	241	oveq1d 6067	. . . . . 6 ⊢ (𝜑 → (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
243	20	nnnn0d 9558	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
244		zringring 14790	. . . . . . . . . 10 ⊢ ℤ_ring ∈ Ring
245	32, 1	mgpbasg 14091	. . . . . . . . . 10 ⊢ (ℤ_ring ∈ Ring → ℤ = (Base‘((mulGrp‘ℂ_fld) ↾_s ℤ)))
246	244, 245	ax-mp 5	. . . . . . . . 9 ⊢ ℤ = (Base‘((mulGrp‘ℂ_fld) ↾_s ℤ))
247		eqid 2234	. . . . . . . . 9 ⊢ (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ)) = (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))
248	246, 247, 236	mhmmulg 13901	. . . . . . . 8 ⊢ ((𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
249	34, 243, 233, 248	syl3anc 1274	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
250	51	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
251		eqid 2234	. . . . . . . . . . 11 ⊢ (._g‘(mulGrp‘ℂ_fld)) = (._g‘(mulGrp‘ℂ_fld))
252	251, 54, 247	submmulg 13904	. . . . . . . . . 10 ⊢ ((ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
253	250, 243, 233, 252	syl3anc 1274	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
254	233	zcnd 9707	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℂ)
255		cnfldexp 14774	. . . . . . . . . 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 2269	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
258	257	fveq2d 5676	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
259	249, 258	eqtr3d 2269	. . . . . 6 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
260	238, 242, 259	3eqtrd 2271	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
261	221, 230, 260	3eqtr3d 2275	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
262		subrgsubg 14395	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubGrp‘ℂ_fld))
263	49, 262	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubGrp‘ℂ_fld)
264		subgsubm 13934	. . . . . . . . 9 ⊢ (ℤ ∈ (SubGrp‘ℂ_fld) → ℤ ∈ (SubMnd‘ℂ_fld))
265	263, 264	mp1i 10	. . . . . . . 8 ⊢ (𝜑 → ℤ ∈ (SubMnd‘ℂ_fld))
266	79	fmpttd 5834	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))):(1...((𝑃 − 1) / 2))⟶ℤ)
267		df-zring 14788	. . . . . . . 8 ⊢ ℤ_ring = (ℂ_fld ↾_s ℤ)
268	122, 265, 266, 267	gsumsubm 13728	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
269	79	zcnd 9707	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℂ)
270	18, 21, 269	gsumfzfsum 14785	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
271	268, 270	eqtr3d 2269	. . . . . 6 ⊢ (𝜑 → (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
272	271	oveq2d 6068	. . . . 5 ⊢ (𝜑 → (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
273	272	fveq2d 5676	. . . 4 ⊢ (𝜑 → (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
274	84, 261, 273	3eqtr3d 2275	. . 3 ⊢ (𝜑 → (𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
275	65	nnnn0d 9558	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
276		zexpcl 10923	. . . . 5 ⊢ ((𝑄 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
277	233, 243, 276	syl2anc 411	. . . 4 ⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
278	122, 79	fsumzcl 12096	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
279		m1expcl 10931	. . . . 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 14846	. . . 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 1274	. . 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 12493	. . 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 1274	. 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 1398 ∈ wcel 2205 ≠ wne 2414 {crab 2526 ∖ cdif 3210 ⊆ wss 3213 {csn 3691 class class class wbr 4111 ↦ cmpt 4173 ran crn 4752 ∘ ccom 4755 ⟶wf 5350 ‘cfv 5354 (class class class)co 6052 ∘_𝑓 cof 6266 Fincfn 6977 ℂcc 8130 0cc0 8132 1c1 8133 + caddc 8135 · cmul 8137 < clt 8313 − cmin 8449 -cneg 8450 # cap 8860 / cdiv 8951 ℕcn 9242 2c2 9293 ℕ₀cn0 9501 ℤcz 9582 ℤ_≥cuz 9859 ℚcq 9957 ...cfz 10348 ⌊cfl 10635 mod cmo 10691 ↑cexp 10907 Σcsu 12046 ∥ cdvds 12481 ℙcprime 12812 Basecbs 13233 ↾_s cress 13234 +_gcplusg 13311 ._rcmulr 13312 0_gc0g 13490 Σ_g cgsu 13491 Mndcmnd 13650 MndHom cmhm 13691 SubMndcsubmnd 13692 ._gcmg 13857 SubGrpcsubg 13905 GrpHom cghm 13978 CMndccmn 14022 Abelcabl 14023 mulGrpcmgp 14085 1_rcur 14124 Ringcrg 14161 CRingccrg 14162 RingHom crh 14317 SubRingcsubrg 14385 ℂ_fldccnfld 14753 ℤ_ringczring 14787 ℤRHomczrh 14808 ℤ/nℤczn 14810

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 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4227 ax-sep 4230 ax-nul 4238 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-iinf 4712 ax-cnex 8223 ax-resscn 8224 ax-1cn 8225 ax-1re 8226 ax-icn 8227 ax-addcl 8228 ax-addrcl 8229 ax-mulcl 8230 ax-mulrcl 8231 ax-addcom 8232 ax-mulcom 8233 ax-addass 8234 ax-mulass 8235 ax-distr 8236 ax-i2m1 8237 ax-0lt1 8238 ax-1rid 8239 ax-0id 8240 ax-rnegex 8241 ax-precex 8242 ax-cnre 8243 ax-pre-ltirr 8244 ax-pre-ltwlin 8245 ax-pre-lttrn 8246 ax-pre-apti 8247 ax-pre-ltadd 8248 ax-pre-mulgt0 8249 ax-pre-mulext 8250 ax-arch 8251 ax-caucvg 8252 ax-addf 8254 ax-mulf 8255

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-xor 1421 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3045 df-csb 3141 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-nul 3511 df-if 3623 df-pw 3673 df-sn 3697 df-pr 3698 df-tp 3699 df-op 3700 df-uni 3917 df-int 3952 df-iun 3995 df-br 4112 df-opab 4174 df-mpt 4175 df-tr 4211 df-id 4416 df-po 4419 df-iso 4420 df-iord 4489 df-on 4491 df-ilim 4492 df-suc 4494 df-iom 4715 df-xp 4757 df-rel 4758 df-cnv 4759 df-co 4760 df-dm 4761 df-rn 4762 df-res 4763 df-ima 4764 df-iota 5314 df-fun 5356 df-fn 5357 df-f 5358 df-f1 5359 df-fo 5360 df-f1o 5361 df-fv 5362 df-isom 5363 df-riota 6005 df-ov 6055 df-oprab 6056 df-mpo 6057 df-of 6268 df-1st 6336 df-2nd 6337 df-tpos 6478 df-recs 6538 df-irdg 6603 df-frec 6624 df-1o 6649 df-2o 6650 df-oadd 6653 df-er 6769 df-ec 6771 df-qs 6775 df-map 6886 df-en 6978 df-dom 6979 df-fin 6980 df-sup 7277 df-pnf 8315 df-mnf 8316 df-xr 8317 df-ltxr 8318 df-le 8319 df-sub 8451 df-neg 8452 df-reap 8854 df-ap 8861 df-div 8952 df-inn 9243 df-2 9301 df-3 9302 df-4 9303 df-5 9304 df-6 9305 df-7 9306 df-8 9307 df-9 9308 df-n0 9502 df-z 9583 df-dec 9716 df-uz 9860 df-q 9958 df-rp 9993 df-fz 10349 df-fzo 10484 df-fl 10637 df-mod 10692 df-seqfrec 10817 df-exp 10908 df-ihash 11147 df-cj 11535 df-re 11536 df-im 11537 df-rsqrt 11691 df-abs 11692 df-clim 11972 df-sumdc 12047 df-dvds 12482 df-gcd 12658 df-prm 12813 df-struct 13235 df-ndx 13236 df-slot 13237 df-base 13239 df-sets 13240 df-iress 13241 df-plusg 13324 df-mulr 13325 df-starv 13326 df-sca 13327 df-vsca 13328 df-ip 13329 df-tset 13330 df-ple 13331 df-ds 13333 df-unif 13334 df-0g 13492 df-igsum 13493 df-topgen 13494 df-iimas 13536 df-qus 13537 df-mgm 13590 df-sgrp 13636 df-mnd 13651 df-mhm 13693 df-submnd 13694 df-grp 13737 df-minusg 13738 df-sbg 13739 df-mulg 13858 df-subg 13908 df-nsg 13909 df-eqg 13910 df-ghm 13979 df-cmn 14024 df-abl 14025 df-mgp 14086 df-rng 14098 df-ur 14125 df-srg 14129 df-ring 14163 df-cring 14164 df-oppr 14233 df-dvdsr 14255 df-unit 14256 df-invr 14288 df-dvr 14299 df-rhm 14319 df-nzr 14347 df-subrg 14387 df-domn 14427 df-idom 14428 df-lmod 14486 df-lssm 14550 df-lsp 14584 df-sra 14632 df-rgmod 14633 df-lidl 14666 df-rsp 14667 df-2idl 14697 df-bl 14743 df-mopn 14744 df-fg 14746 df-metu 14747 df-cnfld 14754 df-zring 14788 df-zrh 14811 df-zn 14813

This theorem is referenced by: lgseisen 15996

W3C validator