lgseisenlem4 - Intuitionistic Logic Explorer

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

Theorem lgseisenlem4 15189

Description: Lemma for lgseisen 15190. (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 14084	. . . . 5 ⊢ ℤ = (Base‘ℤ_ring)
2		zring0 14088	. . . . 5 ⊢ 0 = (0_g‘ℤ_ring)
3		zringabl 14082	. . . . . 6 ⊢ ℤ_ring ∈ Abel
4		ablcmn 13361	. . . . . 6 ⊢ (ℤ_ring ∈ Abel → ℤ_ring ∈ CMnd)
5	3, 4	mp1i 10	. . . . 5 ⊢ (𝜑 → ℤ_ring ∈ CMnd)
6		lgseisen.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
7	6	eldifad 3164	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℙ)
8		prmnn 12248	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	8	nnnn0d 9293	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ₀)
10	7, 9	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
11		lgseisen.7	. . . . . . . . 9 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
12	11	zncrng 14133	. . . . . . . 8 ⊢ (𝑃 ∈ ℕ₀ → 𝑌 ∈ CRing)
13	10, 12	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ CRing)
14		lgseisen.8	. . . . . . . 8 ⊢ 𝐺 = (mulGrp‘𝑌)
15	14	crngmgp 13500	. . . . . . 7 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
16	13, 15	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ CMnd)
17	16	cmnmndd 13378	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Mnd)
18		1zzd 9344	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
19		oddprm 12397	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
20	6, 19	syl 14	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
21	20	nnzd 9438	. . . . 5 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℤ)
22	13	crngringd 13505	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ Ring)
23		lgseisen.9	. . . . . . . . . 10 ⊢ 𝐿 = (ℤRHom‘𝑌)
24	23	zrhrhm 14111	. . . . . . . . 9 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
25	22, 24	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
26		eqid 2193	. . . . . . . . 9 ⊢ (Base‘𝑌) = (Base‘𝑌)
27	1, 26	rhmf 13659	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
28	25, 27	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
29		m1expcl 10633	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → (-1↑𝑘) ∈ ℤ)
30	29	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℤ)
31	28, 30	cofmpt 5727	. . . . . 6 ⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) = (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))))
32		zringmpg 14094	. . . . . . . . 9 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = (mulGrp‘ℤ_ring)
33	32, 14	rhmmhm 13655	. . . . . . . 8 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
34	25, 33	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺))
35		neg1cn 9087	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
36		neg1ap0 9091	. . . . . . . . . . 11 ⊢ -1 # 0
37		eqid 2193	. . . . . . . . . . . 12 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
38		eqid 2193	. . . . . . . . . . . 12 ⊢ ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0}) = ((mulGrp‘ℂ_fld) ↾_s {𝑧 ∈ ℂ ∣ 𝑧 # 0})
39	37, 38	expghmap 14095	. . . . . . . . . . 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 13323	. . . . . . . . . 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 14058	. . . . . . . . . 10 ⊢ ℂ_fld ∈ Ring
44		cnfldui 14077	. . . . . . . . . . 11 ⊢ {𝑧 ∈ ℂ ∣ 𝑧 # 0} = (Unit‘ℂ_fld)
45	44, 37	unitsubm 13615	. . . . . . . . . 10 ⊢ (ℂ_fld ∈ Ring → {𝑧 ∈ ℂ ∣ 𝑧 # 0} ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
46	43, 45	ax-mp 5	. . . . . . . . 9 ⊢ {𝑧 ∈ ℂ ∣ 𝑧 # 0} ∈ (SubMnd‘(mulGrp‘ℂ_fld))
47	38	resmhm2 13060	. . . . . . . . 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 14069	. . . . . . . . . 10 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
50	37	subrgsubm 13730	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
51	49, 50	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld))
52	30	fmpttd 5713	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)):ℤ⟶ℤ)
53	52	frnd 5413	. . . . . . . . 9 ⊢ (𝜑 → ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆ ℤ)
54		eqid 2193	. . . . . . . . . 10 ⊢ ((mulGrp‘ℂ_fld) ↾_s ℤ) = ((mulGrp‘ℂ_fld) ↾_s ℤ)
55	54	resmhm2b 13061	. . . . . . . . 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 13062	. . . . . . 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 2271	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))) ∈ (ℤ_ring MndHom 𝐺))
61		lgseisen.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
62	61	gausslemma2dlem0a 15165	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℕ)
63	62	nnzd 9438	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℤ)
64	63	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
65	6	gausslemma2dlem0a 15165	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℕ)
66	65	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
67		znq 9689	. . . . . . . 8 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑄 / 𝑃) ∈ ℚ)
68	64, 66, 67	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℚ)
69		2nn 9143	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
70		elfznn 10120	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
71	70	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
72		nnmulcl 9003	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
73	69, 71, 72	sylancr 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
74	73	nnzd 9438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
75		zq 9691	. . . . . . . 8 ⊢ ((2 · 𝑥) ∈ ℤ → (2 · 𝑥) ∈ ℚ)
76	74, 75	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℚ)
77		qmulcl 9702	. . . . . . 7 ⊢ (((𝑄 / 𝑃) ∈ ℚ ∧ (2 · 𝑥) ∈ ℚ) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℚ)
78	68, 76, 77	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℚ)
79	78	flqcld 10346	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
80		oveq2 5926	. . . . . 6 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (-1↑𝑘) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
81	80	fveq2d 5558	. . . . 5 ⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
82		oveq2 5926	. . . . . 6 ⊢ (𝑘 = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (-1↑𝑘) = (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
83	82	fveq2d 5558	. . . . 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 13414	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))))
85		eqid 2193	. . . . . . . 8 ⊢ (Base‘𝐺) = (Base‘𝐺)
86		eqid 2193	. . . . . . . 8 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
87	28	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
88		m1expcl 10633	. . . . . . . . . . 11 ⊢ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
89	79, 88	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
90	87, 89	ffvelcdmd 5694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝑌))
91	14, 26	mgpbasg 13422	. . . . . . . . . . 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 2272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝐺))
95		neg1z 9349	. . . . . . . . . . . 12 ⊢ -1 ∈ ℤ
96		lgseisen.4	. . . . . . . . . . . . 13 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
97	61	eldifad 3164	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℙ)
98	97	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
99		prmz 12249	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
100	98, 99	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
101	100, 74	zmulcld 9445	. . . . . . . . . . . . . 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 10416	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
105	96, 104	eqeltrid 2280	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
106		zexpcl 10625	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℤ ∧ 𝑅 ∈ ℕ₀) → (-1↑𝑅) ∈ ℤ)
107	95, 105, 106	sylancr 414	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
108	107, 100	zmulcld 9445	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
109	87, 108	ffvelcdmd 5694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
110	109, 93	eleqtrd 2272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝐺))
111		eqid 2193	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
112		eqid 2193	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
113	85, 86, 16, 18, 21, 94, 110, 111, 112	gsumfzmptfidmadd2 13410	. . . . . . 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 2193	. . . . . . . . . . . 12 ⊢ (._r‘𝑌) = (._r‘𝑌)
115	14, 114	mgpplusgg 13420	. . . . . . . . . . 11 ⊢ (𝑌 ∈ CRing → (._r‘𝑌) = (+_g‘𝐺))
116	13, 115	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝑌) = (+_g‘𝐺))
117	116	ofeqd 6132	. . . . . . . . 9 ⊢ (𝜑 → ∘_𝑓 (._r‘𝑌) = ∘_𝑓 (+_g‘𝐺))
118	117	oveqd 5935	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))
119	118	oveq2d 5934	. . . . . . 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 5935	. . . . . . 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 2236	. . . . . 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 10502	. . . . . . . . 9 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
123		eqidd 2194	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
124		eqidd 2194	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
125	122, 90, 109, 123, 124	offval2 6146	. . . . . . . 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 14087	. . . . . . . . . . . 12 ⊢ · = (._r‘ℤ_ring)
128	1, 127, 114	rhmmul 13660	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
129	126, 89, 108, 128	syl3anc 1249	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))
130	62	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℕ)
131	130, 73	nnmulcld 9031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℕ)
132		nnq 9698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 · (2 · 𝑥)) ∈ ℕ → (𝑄 · (2 · 𝑥)) ∈ ℚ)
133	131, 132	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℚ)
134		nnq 9698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
135	65, 134	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ ℚ)
136	135	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℚ)
137	66	nngt0d 9026	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 𝑃)
138		modqval 10395	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
139	133, 136, 137, 138	syl3anc 1249	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
140	96, 139	eqtrid 2238	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))))
141	100	zcnd 9440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
142	73	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
143	103	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ)
144	103	nnap0d 9028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 # 0)
145	141, 142, 143, 144	div23apd 8847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑥)))
146	145	fveq2d 5558	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
147	146	oveq2d 5934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))) = (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
148	147	oveq2d 5934	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
149	140, 148	eqtrd 2226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
150	149	oveq2d 5934	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))
151		prmz 12249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
152	102, 151	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
153	152, 79	zmulcld 9445	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ)
154	153	zcnd 9440	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
155	101	zcnd 9440	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℂ)
156	154, 155	pncan3d 8333	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑄 · (2 · 𝑥)))
157		2cnd 9055	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
158	71	nncnd 8996	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℂ)
159	141, 157, 158	mul12d 8171	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) = (2 · (𝑄 · 𝑥)))
160	150, 156, 159	3eqtrd 2230	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = (2 · (𝑄 · 𝑥)))
161	160	oveq2d 5934	. . . . . . . . . . . . . 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 9437	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
165		expaddzap 10654	. . . . . . . . . . . . . . . 16 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ 𝑅 ∈ ℤ)) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
166	162, 163, 153, 164, 165	syl22anc 1250	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)))
167		expmulzap 10656	. . . . . . . . . . . . . . . . . 18 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ (𝑃 ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
168	162, 163, 152, 79, 167	syl22anc 1250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
169		1cnd 8035	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈ ℂ)
170		eldifsni 3747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
171	6, 170	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ≠ 2)
172	171	necomd 2450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 2 ≠ 𝑃)
173	172	neneqd 2385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 2 = 𝑃)
174	173	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 = 𝑃)
175		2z 9345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℤ
176		uzid 9606	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
177	175, 176	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (ℤ_≥‘2)
178		dvdsprm 12275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
179	177, 102, 178	sylancr 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
180	174, 179	mtbird 674	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 ∥ 𝑃)
181		oexpneg 12018	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (-1↑𝑃) = -(1↑𝑃))
182	169, 103, 180, 181	syl3anc 1249	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -(1↑𝑃))
183		1exp 10639	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → (1↑𝑃) = 1)
184	152, 183	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑𝑃) = 1)
185	184	negeqd 8214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -(1↑𝑃) = -1)
186	182, 185	eqtrd 2226	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -1)
187	186	oveq1d 5933	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
188	168, 187	eqtrd 2226	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
189	188	oveq1d 5933	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
190	166, 189	eqtrd 2226	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)))
191		nnmulcl 9003	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (𝑄 · 𝑥) ∈ ℕ)
192	62, 70, 191	syl2an 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ)
193	192	nnnn0d 9293	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ₀)
194		2nn0 9257	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ₀
195	194	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ₀)
196	162, 193, 195	expmuld 10747	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = ((-1↑2)↑(𝑄 · 𝑥)))
197		neg1sqe1 10705	. . . . . . . . . . . . . . . . 17 ⊢ (-1↑2) = 1
198	197	oveq1i 5928	. . . . . . . . . . . . . . . 16 ⊢ ((-1↑2)↑(𝑄 · 𝑥)) = (1↑(𝑄 · 𝑥))
199	192	nnzd 9438	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℤ)
200		1exp 10639	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 · 𝑥) ∈ ℤ → (1↑(𝑄 · 𝑥)) = 1)
201	199, 200	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑(𝑄 · 𝑥)) = 1)
202	198, 201	eqtrid 2238	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑2)↑(𝑄 · 𝑥)) = 1)
203	196, 202	eqtrd 2226	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2 · (𝑄 · 𝑥))) = 1)
204	161, 190, 203	3eqtr3d 2234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) = 1)
205	204	oveq1d 5933	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = (1 · 𝑄))
206	89	zcnd 9440	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ)
207	107	zcnd 9440	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
208	206, 207, 141	mulassd 8043	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)))
209	141	mullidd 8037	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑄) = 𝑄)
210	205, 208, 209	3eqtr3d 2234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)) = 𝑄)
211	210	fveq2d 5558	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
212	129, 211	eqtr3d 2228	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄))
213	212	mpteq2dva 4119	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(._r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
214	125, 213	eqtrd 2226	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))
215	214	oveq2d 5934	. . . . . 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 15188	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))
220	219	oveq2d 5934	. . . . . 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 2235	. . . . 5 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(._r‘𝑌)(1_r‘𝑌)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))))
222		eqid 2193	. . . . . . . 8 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
223	90	fmpttd 5713	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
224	92	feq3d 5392	. . . . . . . . 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 13071	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝐺))
227	226, 92	eleqtrrd 2273	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌))
228		eqid 2193	. . . . . . 7 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
229	26, 114, 228	ringridm 13520	. . . . . 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 9628	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
232	20, 231	eleqtrdi 2286	. . . . . . 7 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ (ℤ_≥‘1))
233	97, 99	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℤ)
234	28, 233	ffvelcdmd 5694	. . . . . . . 8 ⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝑌))
235	234, 92	eleqtrd 2272	. . . . . . 7 ⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝐺))
236		eqid 2193	. . . . . . . 8 ⊢ (._g‘𝐺) = (._g‘𝐺)
237	85, 236	gsumfzconst 13411	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ ((𝑃 − 1) / 2) ∈ (ℤ_≥‘1) ∧ (𝐿‘𝑄) ∈ (Base‘𝐺)) → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)))
238	17, 232, 235, 237	syl3anc 1249	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)))
239	20	nncnd 8996	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℂ)
240		1cnd 8035	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
241	239, 240	npcand 8334	. . . . . . 7 ⊢ (𝜑 → ((((𝑃 − 1) / 2) − 1) + 1) = ((𝑃 − 1) / 2))
242	241	oveq1d 5933	. . . . . 6 ⊢ (𝜑 → (((((𝑃 − 1) / 2) − 1) + 1)(._g‘𝐺)(𝐿‘𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
243	20	nnnn0d 9293	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
244		zringring 14081	. . . . . . . . . 10 ⊢ ℤ_ring ∈ Ring
245	32, 1	mgpbasg 13422	. . . . . . . . . 10 ⊢ (ℤ_ring ∈ Ring → ℤ = (Base‘((mulGrp‘ℂ_fld) ↾_s ℤ)))
246	244, 245	ax-mp 5	. . . . . . . . 9 ⊢ ℤ = (Base‘((mulGrp‘ℂ_fld) ↾_s ℤ))
247		eqid 2193	. . . . . . . . 9 ⊢ (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ)) = (._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))
248	246, 247, 236	mhmmulg 13233	. . . . . . . 8 ⊢ ((𝐿 ∈ (((mulGrp‘ℂ_fld) ↾_s ℤ) MndHom 𝐺) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
249	34, 243, 233, 248	syl3anc 1249	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)))
250	51	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
251		eqid 2193	. . . . . . . . . . 11 ⊢ (._g‘(mulGrp‘ℂ_fld)) = (._g‘(mulGrp‘ℂ_fld))
252	251, 54, 247	submmulg 13236	. . . . . . . . . 10 ⊢ ((ℤ ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ((𝑃 − 1) / 2) ∈ ℕ₀ ∧ 𝑄 ∈ ℤ) → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
253	250, 243, 233, 252	syl3anc 1249	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘(mulGrp‘ℂ_fld))𝑄) = (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄))
254	233	zcnd 9440	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℂ)
255		cnfldexp 14065	. . . . . . . . . 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 2228	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄) = (𝑄↑((𝑃 − 1) / 2)))
258	257	fveq2d 5558	. . . . . . 7 ⊢ (𝜑 → (𝐿‘(((𝑃 − 1) / 2)(._g‘((mulGrp‘ℂ_fld) ↾_s ℤ))𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
259	249, 258	eqtr3d 2228	. . . . . 6 ⊢ (𝜑 → (((𝑃 − 1) / 2)(._g‘𝐺)(𝐿‘𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
260	238, 242, 259	3eqtrd 2230	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
261	221, 230, 260	3eqtr3d 2234	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2))))
262		subrgsubg 13723	. . . . . . . . . 10 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubGrp‘ℂ_fld))
263	49, 262	ax-mp 5	. . . . . . . . 9 ⊢ ℤ ∈ (SubGrp‘ℂ_fld)
264		subgsubm 13266	. . . . . . . . 9 ⊢ (ℤ ∈ (SubGrp‘ℂ_fld) → ℤ ∈ (SubMnd‘ℂ_fld))
265	263, 264	mp1i 10	. . . . . . . 8 ⊢ (𝜑 → ℤ ∈ (SubMnd‘ℂ_fld))
266	79	fmpttd 5713	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))):(1...((𝑃 − 1) / 2))⟶ℤ)
267		df-zring 14079	. . . . . . . 8 ⊢ ℤ_ring = (ℂ_fld ↾_s ℤ)
268	122, 265, 266, 267	gsumsubm 13066	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
269	79	zcnd 9440	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℂ)
270	18, 21, 269	gsumfzfsum 14076	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
271	268, 270	eqtr3d 2228	. . . . . 6 ⊢ (𝜑 → (ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))
272	271	oveq2d 5934	. . . . 5 ⊢ (𝜑 → (-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))
273	272	fveq2d 5558	. . . 4 ⊢ (𝜑 → (𝐿‘(-1↑(ℤ_ring Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
274	84, 261, 273	3eqtr3d 2234	. . 3 ⊢ (𝜑 → (𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))
275	65	nnnn0d 9293	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
276		zexpcl 10625	. . . . 5 ⊢ ((𝑄 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ₀) → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
277	233, 243, 276	syl2anc 411	. . . 4 ⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ)
278	122, 79	fsumzcl 11545	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)
279		m1expcl 10633	. . . . 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 14137	. . . 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 1249	. . 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 11942	. . 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 1249	. 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 1364 ∈ wcel 2164 ≠ wne 2364 {crab 2476 ∖ cdif 3150 ⊆ wss 3153 {csn 3618 class class class wbr 4029 ↦ cmpt 4090 ran crn 4660 ∘ ccom 4663 ⟶wf 5250 ‘cfv 5254 (class class class)co 5918 ∘_𝑓 cof 6128 Fincfn 6794 ℂcc 7870 0cc0 7872 1c1 7873 + caddc 7875 · cmul 7877 < clt 8054 − cmin 8190 -cneg 8191 # cap 8600 / cdiv 8691 ℕcn 8982 2c2 9033 ℕ₀cn0 9240 ℤcz 9317 ℤ_≥cuz 9592 ℚcq 9684 ...cfz 10074 ⌊cfl 10337 mod cmo 10393 ↑cexp 10609 Σcsu 11496 ∥ cdvds 11930 ℙcprime 12245 Basecbs 12618 ↾_s cress 12619 +_gcplusg 12695 ._rcmulr 12696 0_gc0g 12867 Σ_g cgsu 12868 Mndcmnd 12997 MndHom cmhm 13029 SubMndcsubmnd 13030 ._gcmg 13189 SubGrpcsubg 13237 GrpHom cghm 13310 CMndccmn 13354 Abelcabl 13355 mulGrpcmgp 13416 1_rcur 13455 Ringcrg 13492 CRingccrg 13493 RingHom crh 13646 SubRingcsubrg 13713 ℂ_fldccnfld 14047 ℤ_ringczring 14078 ℤRHomczrh 14099 ℤ/nℤczn 14101

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 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990 ax-arch 7991 ax-caucvg 7992 ax-addf 7994 ax-mulf 7995

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-tp 3626 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-isom 5263 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-of 6130 df-1st 6193 df-2nd 6194 df-tpos 6298 df-recs 6358 df-irdg 6423 df-frec 6444 df-1o 6469 df-2o 6470 df-oadd 6473 df-er 6587 df-ec 6589 df-qs 6593 df-map 6704 df-en 6795 df-dom 6796 df-fin 6797 df-sup 7043 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-5 9044 df-6 9045 df-7 9046 df-8 9047 df-9 9048 df-n0 9241 df-z 9318 df-dec 9449 df-uz 9593 df-q 9685 df-rp 9720 df-fz 10075 df-fzo 10209 df-fl 10339 df-mod 10394 df-seqfrec 10519 df-exp 10610 df-ihash 10847 df-cj 10986 df-re 10987 df-im 10988 df-rsqrt 11142 df-abs 11143 df-clim 11422 df-sumdc 11497 df-dvds 11931 df-gcd 12080 df-prm 12246 df-struct 12620 df-ndx 12621 df-slot 12622 df-base 12624 df-sets 12625 df-iress 12626 df-plusg 12708 df-mulr 12709 df-starv 12710 df-sca 12711 df-vsca 12712 df-ip 12713 df-ple 12715 df-0g 12869 df-igsum 12870 df-iimas 12885 df-qus 12886 df-mgm 12939 df-sgrp 12985 df-mnd 12998 df-mhm 13031 df-submnd 13032 df-grp 13075 df-minusg 13076 df-sbg 13077 df-mulg 13190 df-subg 13240 df-nsg 13241 df-eqg 13242 df-ghm 13311 df-cmn 13356 df-abl 13357 df-mgp 13417 df-rng 13429 df-ur 13456 df-srg 13460 df-ring 13494 df-cring 13495 df-oppr 13564 df-dvdsr 13585 df-unit 13586 df-invr 13617 df-dvr 13628 df-rhm 13648 df-nzr 13676 df-subrg 13715 df-domn 13755 df-idom 13756 df-lmod 13785 df-lssm 13849 df-lsp 13883 df-sra 13931 df-rgmod 13932 df-lidl 13965 df-rsp 13966 df-2idl 13996 df-icnfld 14048 df-zring 14079 df-zrh 14102 df-zn 14104

This theorem is referenced by: lgseisen 15190

W3C validator