lgseisenlem3 - Intuitionistic Logic Explorer

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

Theorem lgseisenlem3 16071

Description: Lemma for lgseisen 16073. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-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
lgseisenlem3	⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))

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

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

Step	Hyp	Ref	Expression
1		oveq2 6066	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
2	1	fveq2d 5679	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥)))
3	2	cbvmptv 4211	. . . . . . 7 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
4	3	oveq2i 6069	. . . . . 6 ⊢ (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
5		eqid 2234	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
6		eqid 2234	. . . . . . 7 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
7		lgseisen.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
8	7	eldifad 3225	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℙ)
9		lgseisen.7	. . . . . . . . . . 11 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
10	9	znidom 14931	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ IDomn)
11	8, 10	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ IDomn)
12	11	idomcringd 14525	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ CRing)
13		lgseisen.8	. . . . . . . . 9 ⊢ 𝐺 = (mulGrp‘𝑌)
14	13	crngmgp 14247	. . . . . . . 8 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
15	12, 14	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
16		1zzd 9621	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
17		oddn2prm 12984	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 2 ∥ 𝑃)
18	7, 17	syl 14	. . . . . . . 8 ⊢ (𝜑 → ¬ 2 ∥ 𝑃)
19		prmz 12833	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
20		oddm1d2 12603	. . . . . . . . 9 ⊢ (𝑃 ∈ ℤ → (¬ 2 ∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈ ℤ))
21	8, 19, 20	3syl 17	. . . . . . . 8 ⊢ (𝜑 → (¬ 2 ∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈ ℤ))
22	18, 21	mpbid 147	. . . . . . 7 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℤ)
23	11	idomringd 14526	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Ring)
24		lgseisen.9	. . . . . . . . . . . 12 ⊢ 𝐿 = (ℤRHom‘𝑌)
25	24	zrhrhm 14897	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
26		zringbas 14870	. . . . . . . . . . . 12 ⊢ ℤ = (Base‘ℤ_ring)
27		eqid 2234	. . . . . . . . . . . 12 ⊢ (Base‘𝑌) = (Base‘𝑌)
28	26, 27	rhmf 14408	. . . . . . . . . . 11 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
29	23, 25, 28	3syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
30		2z 9622	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
31		elfzelz 10378	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ)
32		zmulcl 9648	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · 𝑘) ∈ ℤ)
33	30, 31, 32	sylancr 414	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈ ℤ)
34		ffvelcdm 5815	. . . . . . . . . 10 ⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
35	29, 33, 34	syl2an 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
36	35	fmpttd 5837	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
37	13, 27	mgpbasg 14165	. . . . . . . . . 10 ⊢ (𝑌 ∈ CRing → (Base‘𝑌) = (Base‘𝐺))
38	12, 37	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑌) = (Base‘𝐺))
39	38	feq3d 5502	. . . . . . . 8 ⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌) ↔ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝐺)))
40	36, 39	mpbid 147	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝐺))
41		lgseisen.2	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
42		lgseisen.3	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
43		lgseisen.4	. . . . . . . 8 ⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
44		lgseisen.5	. . . . . . . 8 ⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
45		lgseisen.6	. . . . . . . 8 ⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
46	7, 41, 42, 43, 44, 45	lgseisenlem2 16070	. . . . . . 7 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
47	5, 6, 15, 16, 22, 40, 46	gsumfzreidx 14090	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
48	4, 47	eqtr3id 2281	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
49	7, 41, 42, 43, 44	lgseisenlem1 16069	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
50	44	fmpt 5832	. . . . . . . 8 ⊢ (∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
51	49, 50	sylibr 134	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
52	44	a1i 9	. . . . . . 7 ⊢ (𝜑 → 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
53		eqidd 2235	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))))
54		oveq2 6066	. . . . . . . 8 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
55	54	fveq2d 5679	. . . . . . 7 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))
56	51, 52, 53, 55	fmptcof 5849	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))
57	56	oveq2d 6074	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))))
58	41	eldifad 3225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 ∈ ℙ)
59	58	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
60		prmz 12833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
61	59, 60	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
62		2nn 9416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℕ
63		elfznn 10409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
64	63	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
65		nnmulcl 9275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
66	62, 64, 65	sylancr 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
67	66	nnzd 9717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
68	61, 67	zmulcld 9724	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
69	8	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
70		prmnn 12832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
71	69, 70	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
72	68, 71	zmodcld 10731	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
73	43, 72	eqeltrid 2321	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
74	73	nn0zd 9716	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
75		m1expcl 10948	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
76	74, 75	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
77	76, 74	zmulcld 9724	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
78	77, 71	zmodcld 10731	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
79	78	nn0cnd 9572	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
80		2cnd 9327	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
81		2ap0 9347	. . . . . . . . . . . 12 ⊢ 2 # 0
82	81	a1i 9	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 # 0)
83	79, 80, 82	divcanap2d 9083	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃))
84	83	fveq2d 5679	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)))
85		zq 9976	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℚ)
86	8, 19, 85	3syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℚ)
87	86	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℚ)
88	71	nngt0d 9298	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 𝑃)
89		eqidd 2235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
90	43	oveq1i 6068	. . . . . . . . . . . . . 14 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
91		zq 9976	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 · (2 · 𝑥)) ∈ ℤ → (𝑄 · (2 · 𝑥)) ∈ ℚ)
92	68, 91	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℚ)
93		modqabs2 10744	. . . . . . . . . . . . . . 15 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
94	92, 87, 88, 93	syl3anc 1274	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
95	90, 94	eqtrid 2279	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
96	76, 76, 74, 68, 87, 88, 89, 95	modqmul12d 10764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
97		zq 9976	. . . . . . . . . . . . . 14 ⊢ (((-1↑𝑅) · 𝑅) ∈ ℤ → ((-1↑𝑅) · 𝑅) ∈ ℚ)
98	77, 97	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℚ)
99		modqabs2 10744	. . . . . . . . . . . . 13 ⊢ ((((-1↑𝑅) · 𝑅) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
100	98, 87, 88, 99	syl3anc 1274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
101	76	zcnd 9719	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
102	61	zcnd 9719	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
103	67	zcnd 9719	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
104	101, 102, 103	mulassd 8313	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
105	104	oveq1d 6073	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
106	96, 100, 105	3eqtr4d 2277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃))
107	8, 70	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
108	107	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
109	78	nn0zd 9716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ)
110	76, 61	zmulcld 9724	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
111	110, 67	zmulcld 9724	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ)
112		moddvds 12510	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℕ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
113	108, 109, 111, 112	syl3anc 1274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
114	106, 113	mpbid 147	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
115	71	nnnn0d 9570	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ₀)
116	9, 24	zndvds 14923	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ₀ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
117	115, 109, 111, 116	syl3anc 1274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
118	114, 117	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
119	23, 25	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
120	119	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
121		zringmulr 14873	. . . . . . . . . . 11 ⊢ · = (._r‘ℤ_ring)
122		eqid 2234	. . . . . . . . . . 11 ⊢ (._r‘𝑌) = (._r‘𝑌)
123	26, 121, 122	rhmmul 14409	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
124	120, 110, 67, 123	syl3anc 1274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
125	84, 118, 124	3eqtrd 2271	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
126	125	mpteq2dva 4205	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
127	16, 22	fzfigd 10817	. . . . . . . 8 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
128	29	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
129	128, 110	ffvelcdmd 5818	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
130	128, 67	ffvelcdmd 5818	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌))
131		eqidd 2235	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
132		eqidd 2235	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
133	127, 129, 130, 131, 132	offval2 6291	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
134	126, 133	eqtr4d 2270	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
135	134	oveq2d 6074	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
136	48, 57, 135	3eqtrd 2271	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
137		eqid 2234	. . . . . 6 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
138	38	eleq2d 2304	. . . . . . . 8 ⊢ (𝜑 → ((𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌) ↔ (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝐺)))
139	138	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌) ↔ (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝐺)))
140	129, 139	mpbid 147	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝐺))
141	38	eleq2d 2304	. . . . . . . 8 ⊢ (𝜑 → ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ↔ (𝐿‘(2 · 𝑥)) ∈ (Base‘𝐺)))
142	141	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ↔ (𝐿‘(2 · 𝑥)) ∈ (Base‘𝐺)))
143	130, 142	mpbid 147	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝐺))
144		eqid 2234	. . . . . 6 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
145		eqid 2234	. . . . . 6 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
146	5, 137, 15, 16, 22, 140, 143, 144, 145	gsumfzmptfidmadd2 14093	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(+_g‘𝐺)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
147	13, 122	mgpplusgg 14163	. . . . . . . . 9 ⊢ (𝑌 ∈ CRing → (._r‘𝑌) = (+_g‘𝐺))
148	12, 147	syl 14	. . . . . . . 8 ⊢ (𝜑 → (._r‘𝑌) = (+_g‘𝐺))
149	148	ofeqd 6277	. . . . . . 7 ⊢ (𝜑 → ∘_𝑓 (._r‘𝑌) = ∘_𝑓 (+_g‘𝐺))
150	149	oveqd 6075	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
151	150	oveq2d 6074	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
152	148	oveqd 6075	. . . . 5 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(+_g‘𝐺)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
153	146, 151, 152	3eqtr4d 2277	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
154	136, 153	eqtrd 2267	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
155	154	oveq1d 6073	. 2 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
156	15	cmnmndd 14061	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Mnd)
157		eqid 2234	. . . . . 6 ⊢ (Unit‘𝑌) = (Unit‘𝑌)
158	157, 13	unitsubm 14364	. . . . 5 ⊢ (𝑌 ∈ Ring → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
159	23, 158	syl 14	. . . 4 ⊢ (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
160		elfzle2 10382	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
161	160	adantl 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
162	64	nnred 9267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
163		prmuz2 12853	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
164		uz2m1nn 9955	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
165	69, 163, 164	3syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
166	165	nnred 9267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
167		2re 9324	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
168	167	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
169		2pos 9345	. . . . . . . . . . 11 ⊢ 0 < 2
170	169	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
171		lemuldiv2 9173	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
172	162, 166, 168, 170, 171	syl112anc 1278	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
173	161, 172	mpbird 167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
174	69, 19	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
175		peano2zm 9632	. . . . . . . . 9 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
176		fznn 10445	. . . . . . . . 9 ⊢ ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
177	174, 175, 176	3syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
178	66, 173, 177	mpbir2and 953	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
179		fzm1ndvds 12567	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
180	71, 178, 179	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
181	9, 157, 24	znunit 14933	. . . . . . . 8 ⊢ ((𝑃 ∈ ℕ₀ ∧ (2 · 𝑥) ∈ ℤ) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((2 · 𝑥) gcd 𝑃) = 1))
182	115, 67, 181	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((2 · 𝑥) gcd 𝑃) = 1))
183		coprm 12866	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → (¬ 𝑃 ∥ (2 · 𝑥) ↔ (𝑃 gcd (2 · 𝑥)) = 1))
184	19	adantr 276	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → 𝑃 ∈ ℤ)
185		simpr 110	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
186	184, 185	gcdcomd 12695	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → (𝑃 gcd (2 · 𝑥)) = ((2 · 𝑥) gcd 𝑃))
187	186	eqeq1d 2243	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → ((𝑃 gcd (2 · 𝑥)) = 1 ↔ ((2 · 𝑥) gcd 𝑃) = 1))
188	183, 187	bitrd 188	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → (¬ 𝑃 ∥ (2 · 𝑥) ↔ ((2 · 𝑥) gcd 𝑃) = 1))
189	69, 67, 188	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑃 ∥ (2 · 𝑥) ↔ ((2 · 𝑥) gcd 𝑃) = 1))
190	182, 189	bitr4d 191	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ¬ 𝑃 ∥ (2 · 𝑥)))
191	180, 190	mpbird 167	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌))
192	191	fmpttd 5837	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌))
193	156, 16, 22, 159, 192	gsumfzsubmcl 14091	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌))
194		eqid 2234	. . . 4 ⊢ (/_r‘𝑌) = (/_r‘𝑌)
195		eqid 2234	. . . 4 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
196	157, 194, 195	dvrid 14382	. . 3 ⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1_r‘𝑌))
197	23, 193, 196	syl2anc 411	. 2 ⊢ (𝜑 → ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1_r‘𝑌))
198	129	fmpttd 5837	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
199	38	feq3d 5502	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌) ↔ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝐺)))
200	198, 199	mpbid 147	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝐺))
201	5, 6, 156, 16, 22, 200	gsumfzcl 13754	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝐺))
202	201, 38	eleqtrrd 2314	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌))
203	27, 157, 194, 122	dvrcan3 14386	. . 3 ⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌) ∧ (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → (((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))
204	23, 202, 193, 203	syl3anc 1274	. 2 ⊢ (𝜑 → (((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/_r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))
205	155, 197, 204	3eqtr3rd 2276	1 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1_r‘𝑌))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1398 ∈ wcel 2205 ≠ wne 2414 ∀wral 2522 ∖ cdif 3211 {csn 3694 class class class wbr 4114 ↦ cmpt 4176 ∘ ccom 4758 ⟶wf 5353 ‘cfv 5357 (class class class)co 6058 ∘_𝑓 cof 6273 Fincfn 6988 ℝcr 8142 0cc0 8143 1c1 8144 · cmul 8148 < clt 8324 ≤ cle 8325 − cmin 8460 -cneg 8461 # cap 8872 / cdiv 8963 ℕcn 9254 2c2 9305 ℕ₀cn0 9513 ℤcz 9594 ℤ_≥cuz 9871 ℚcq 9969 ...cfz 10361 mod cmo 10708 ↑cexp 10924 ∥ cdvds 12498 gcd cgcd 12674 ℙcprime 12829 Basecbs 13296 +_gcplusg 13374 ._rcmulr 13375 0_gc0g 13553 Σ_g cgsu 13554 SubMndcsubmnd 13713 CMndccmn 14037 mulGrpcmgp 14159 1_rcur 14202 Ringcrg 14239 CRingccrg 14240 Unitcui 14331 /_rcdvr 14376 RingHom crh 14395 IDomncidom 14503 ℤ_ringczring 14864 ℤRHomczrh 14885 ℤ/nℤczn 14887

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 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-mulrcl 8242 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-precex 8253 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259 ax-pre-mulgt0 8260 ax-pre-mulext 8261 ax-arch 8262 ax-caucvg 8263 ax-addf 8265 ax-mulf 8266

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 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-tp 3702 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-po 4422 df-iso 4423 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-of 6275 df-1st 6347 df-2nd 6348 df-tpos 6489 df-recs 6549 df-irdg 6614 df-frec 6635 df-1o 6660 df-2o 6661 df-oadd 6664 df-er 6780 df-ec 6782 df-qs 6786 df-map 6897 df-en 6989 df-dom 6990 df-fin 6991 df-sup 7288 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-reap 8866 df-ap 8873 df-div 8964 df-inn 9255 df-2 9313 df-3 9314 df-4 9315 df-5 9316 df-6 9317 df-7 9318 df-8 9319 df-9 9320 df-n0 9514 df-z 9595 df-dec 9728 df-uz 9872 df-q 9970 df-rp 10005 df-fz 10362 df-fzo 10499 df-fl 10654 df-mod 10709 df-seqfrec 10834 df-exp 10925 df-ihash 11164 df-cj 11552 df-re 11553 df-im 11554 df-rsqrt 11708 df-abs 11709 df-dvds 12499 df-gcd 12675 df-prm 12830 df-struct 13298 df-ndx 13299 df-slot 13300 df-base 13302 df-sets 13303 df-iress 13304 df-plusg 13387 df-mulr 13388 df-starv 13389 df-sca 13390 df-vsca 13391 df-ip 13392 df-tset 13393 df-ple 13394 df-ds 13396 df-unif 13397 df-0g 13555 df-igsum 13556 df-topgen 13557 df-iimas 13567 df-qus 13568 df-mgm 13619 df-sgrp 13665 df-mnd 13678 df-mhm 13714 df-submnd 13715 df-grp 13758 df-minusg 13759 df-sbg 13760 df-mulg 13873 df-subg 13923 df-nsg 13924 df-eqg 13925 df-ghm 13994 df-cmn 14039 df-abl 14040 df-mgp 14160 df-rng 14172 df-ur 14203 df-srg 14207 df-ring 14241 df-cring 14242 df-oppr 14311 df-dvdsr 14333 df-unit 14334 df-invr 14366 df-dvr 14377 df-rhm 14397 df-nzr 14425 df-subrg 14465 df-domn 14505 df-idom 14506 df-lmod 14563 df-lssm 14627 df-lsp 14661 df-sra 14709 df-rgmod 14710 df-lidl 14743 df-rsp 14744 df-2idl 14774 df-bl 14820 df-mopn 14821 df-fg 14823 df-metu 14824 df-cnfld 14831 df-zring 14865 df-zrh 14888 df-zn 14890

This theorem is referenced by: lgseisenlem4 16072

W3C validator