lgseisenlem3 - Intuitionistic Logic Explorer

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

Theorem lgseisenlem3 15280

Description: Lemma for lgseisen 15282. (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 5930	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
2	1	fveq2d 5562	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥)))
3	2	cbvmptv 4129	. . . . . . 7 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
4	3	oveq2i 5933	. . . . . 6 ⊢ (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
5		eqid 2196	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
6		eqid 2196	. . . . . . 7 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
7		lgseisen.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
8	7	eldifad 3168	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℙ)
9		lgseisen.7	. . . . . . . . . . 11 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
10	9	znidom 14189	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ IDomn)
11	8, 10	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ IDomn)
12	11	idomcringd 13810	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ CRing)
13		lgseisen.8	. . . . . . . . 9 ⊢ 𝐺 = (mulGrp‘𝑌)
14	13	crngmgp 13536	. . . . . . . 8 ⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
15	12, 14	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
16		1zzd 9350	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
17		oddn2prm 12406	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ¬ 2 ∥ 𝑃)
18	7, 17	syl 14	. . . . . . . 8 ⊢ (𝜑 → ¬ 2 ∥ 𝑃)
19		prmz 12255	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
20		oddm1d2 12039	. . . . . . . . 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 13811	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Ring)
24		lgseisen.9	. . . . . . . . . . . 12 ⊢ 𝐿 = (ℤRHom‘𝑌)
25	24	zrhrhm 14155	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
26		zringbas 14128	. . . . . . . . . . . 12 ⊢ ℤ = (Base‘ℤ_ring)
27		eqid 2196	. . . . . . . . . . . 12 ⊢ (Base‘𝑌) = (Base‘𝑌)
28	26, 27	rhmf 13695	. . . . . . . . . . 11 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
29	23, 25, 28	3syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
30		2z 9351	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
31		elfzelz 10097	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ)
32		zmulcl 9376	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · 𝑘) ∈ ℤ)
33	30, 31, 32	sylancr 414	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈ ℤ)
34		ffvelcdm 5695	. . . . . . . . . 10 ⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
35	29, 33, 34	syl2an 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
36	35	fmpttd 5717	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
37	13, 27	mgpbasg 13458	. . . . . . . . . 10 ⊢ (𝑌 ∈ CRing → (Base‘𝑌) = (Base‘𝐺))
38	12, 37	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑌) = (Base‘𝐺))
39	38	feq3d 5396	. . . . . . . 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 15279	. . . . . . 7 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
47	5, 6, 15, 16, 22, 40, 46	gsumfzreidx 13443	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
48	4, 47	eqtr3id 2243	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
49	7, 41, 42, 43, 44	lgseisenlem1 15278	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
50	44	fmpt 5712	. . . . . . . 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 2197	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))))
54		oveq2 5930	. . . . . . . 8 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
55	54	fveq2d 5562	. . . . . . 7 ⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))
56	51, 52, 53, 55	fmptcof 5729	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))
57	56	oveq2d 5938	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))))
58	41	eldifad 3168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 ∈ ℙ)
59	58	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
60		prmz 12255	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
61	59, 60	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
62		2nn 9149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℕ
63		elfznn 10126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
64	63	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
65		nnmulcl 9008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
66	62, 64, 65	sylancr 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
67	66	nnzd 9444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
68	61, 67	zmulcld 9451	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
69	8	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
70		prmnn 12254	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
71	69, 70	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
72	68, 71	zmodcld 10422	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ₀)
73	43, 72	eqeltrid 2283	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ₀)
74	73	nn0zd 9443	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
75		m1expcl 10639	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
76	74, 75	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
77	76, 74	zmulcld 9451	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
78	77, 71	zmodcld 10422	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ₀)
79	78	nn0cnd 9301	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
80		2cnd 9060	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
81		2ap0 9080	. . . . . . . . . . . 12 ⊢ 2 # 0
82	81	a1i 9	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 # 0)
83	79, 80, 82	divcanap2d 8816	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃))
84	83	fveq2d 5562	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)))
85		zq 9697	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℚ)
86	8, 19, 85	3syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℚ)
87	86	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℚ)
88	71	nngt0d 9031	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 𝑃)
89		eqidd 2197	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
90	43	oveq1i 5932	. . . . . . . . . . . . . 14 ⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
91		zq 9697	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 · (2 · 𝑥)) ∈ ℤ → (𝑄 · (2 · 𝑥)) ∈ ℚ)
92	68, 91	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℚ)
93		modqabs2 10435	. . . . . . . . . . . . . . 15 ⊢ (((𝑄 · (2 · 𝑥)) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
94	92, 87, 88, 93	syl3anc 1249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
95	90, 94	eqtrid 2241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
96	76, 76, 74, 68, 87, 88, 89, 95	modqmul12d 10455	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
97		zq 9697	. . . . . . . . . . . . . 14 ⊢ (((-1↑𝑅) · 𝑅) ∈ ℤ → ((-1↑𝑅) · 𝑅) ∈ ℚ)
98	77, 97	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℚ)
99		modqabs2 10435	. . . . . . . . . . . . 13 ⊢ ((((-1↑𝑅) · 𝑅) ∈ ℚ ∧ 𝑃 ∈ ℚ ∧ 0 < 𝑃) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
100	98, 87, 88, 99	syl3anc 1249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
101	76	zcnd 9446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
102	61	zcnd 9446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
103	67	zcnd 9446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
104	101, 102, 103	mulassd 8048	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
105	104	oveq1d 5937	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
106	96, 100, 105	3eqtr4d 2239	. . . . . . . . . . 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 9443	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ)
110	76, 61	zmulcld 9451	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
111	110, 67	zmulcld 9451	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ)
112		moddvds 11948	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℕ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
113	108, 109, 111, 112	syl3anc 1249	. . . . . . . . . . 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 9299	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ₀)
116	9, 24	zndvds 14181	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ₀ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
117	115, 109, 111, 116	syl3anc 1249	. . . . . . . . . 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 14131	. . . . . . . . . . 11 ⊢ · = (._r‘ℤ_ring)
122		eqid 2196	. . . . . . . . . . 11 ⊢ (._r‘𝑌) = (._r‘𝑌)
123	26, 121, 122	rhmmul 13696	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑌) ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
124	120, 110, 67, 123	syl3anc 1249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
125	84, 118, 124	3eqtrd 2233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥))))
126	125	mpteq2dva 4123	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
127	16, 22	fzfigd 10508	. . . . . . . 8 ⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
128	29	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
129	128, 110	ffvelcdmd 5698	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
130	128, 67	ffvelcdmd 5698	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌))
131		eqidd 2197	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
132		eqidd 2197	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
133	127, 129, 130, 131, 132	offval2 6151	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(._r‘𝑌)(𝐿‘(2 · 𝑥)))))
134	126, 133	eqtr4d 2232	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
135	134	oveq2d 5938	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
136	48, 57, 135	3eqtrd 2233	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
137		eqid 2196	. . . . . 6 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
138	38	eleq2d 2266	. . . . . . . 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 2266	. . . . . . . 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 2196	. . . . . 6 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
145		eqid 2196	. . . . . 6 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
146	5, 137, 15, 16, 22, 140, 143, 144, 145	gsumfzmptfidmadd2 13446	. . . . 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 13456	. . . . . . . . 9 ⊢ (𝑌 ∈ CRing → (._r‘𝑌) = (+_g‘𝐺))
148	12, 147	syl 14	. . . . . . . 8 ⊢ (𝜑 → (._r‘𝑌) = (+_g‘𝐺))
149	148	ofeqd 6137	. . . . . . 7 ⊢ (𝜑 → ∘_𝑓 (._r‘𝑌) = ∘_𝑓 (+_g‘𝐺))
150	149	oveqd 5939	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
151	150	oveq2d 5938	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (._r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σ_g ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘_𝑓 (+_g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
152	148	oveqd 5939	. . . . 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 2239	. . . 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 2229	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(._r‘𝑌)(𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
155	154	oveq1d 5937	. 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 13414	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Mnd)
157		eqid 2196	. . . . . 6 ⊢ (Unit‘𝑌) = (Unit‘𝑌)
158	157, 13	unitsubm 13651	. . . . 5 ⊢ (𝑌 ∈ Ring → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
159	23, 158	syl 14	. . . 4 ⊢ (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
160		elfzle2 10100	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
161	160	adantl 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
162	64	nnred 9000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
163		prmuz2 12275	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
164		uz2m1nn 9676	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
165	69, 163, 164	3syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
166	165	nnred 9000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
167		2re 9057	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
168	167	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
169		2pos 9078	. . . . . . . . . . 11 ⊢ 0 < 2
170	169	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
171		lemuldiv2 8906	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
172	162, 166, 168, 170, 171	syl112anc 1253	. . . . . . . . 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 9361	. . . . . . . . 9 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
176		fznn 10161	. . . . . . . . 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 946	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
179		fzm1ndvds 12004	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
180	71, 178, 179	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
181	9, 157, 24	znunit 14191	. . . . . . . 8 ⊢ ((𝑃 ∈ ℕ₀ ∧ (2 · 𝑥) ∈ ℤ) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((2 · 𝑥) gcd 𝑃) = 1))
182	115, 67, 181	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((2 · 𝑥) gcd 𝑃) = 1))
183		coprm 12288	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → (¬ 𝑃 ∥ (2 · 𝑥) ↔ (𝑃 gcd (2 · 𝑥)) = 1))
184	19	adantr 276	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → 𝑃 ∈ ℤ)
185		simpr 110	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → (2 · 𝑥) ∈ ℤ)
186	184, 185	gcdcomd 12117	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ (2 · 𝑥) ∈ ℤ) → (𝑃 gcd (2 · 𝑥)) = ((2 · 𝑥) gcd 𝑃))
187	186	eqeq1d 2205	. . . . . . . . 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 5717	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌))
193	156, 16, 22, 159, 192	gsumfzsubmcl 13444	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌))
194		eqid 2196	. . . 4 ⊢ (/_r‘𝑌) = (/_r‘𝑌)
195		eqid 2196	. . . 4 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
196	157, 194, 195	dvrid 13669	. . 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 5717	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
199	38	feq3d 5396	. . . . . 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 13107	. . . 4 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝐺))
202	201, 38	eleqtrrd 2276	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌))
203	27, 157, 194, 122	dvrcan3 13673	. . 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 1249	. 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 2238	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 1364 ∈ wcel 2167 ≠ wne 2367 ∀wral 2475 ∖ cdif 3154 {csn 3622 class class class wbr 4033 ↦ cmpt 4094 ∘ ccom 4667 ⟶wf 5254 ‘cfv 5258 (class class class)co 5922 ∘_𝑓 cof 6133 Fincfn 6799 ℝcr 7876 0cc0 7877 1c1 7878 · cmul 7882 < clt 8059 ≤ cle 8060 − cmin 8195 -cneg 8196 # cap 8605 / cdiv 8696 ℕcn 8987 2c2 9038 ℕ₀cn0 9246 ℤcz 9323 ℤ_≥cuz 9598 ℚcq 9690 ...cfz 10080 mod cmo 10399 ↑cexp 10615 ∥ cdvds 11936 gcd cgcd 12085 ℙcprime 12251 Basecbs 12654 +_gcplusg 12731 ._rcmulr 12732 0_gc0g 12903 Σ_g cgsu 12904 SubMndcsubmnd 13066 CMndccmn 13390 mulGrpcmgp 13452 1_rcur 13491 Ringcrg 13528 CRingccrg 13529 Unitcui 13619 /_rcdvr 13663 RingHom crh 13682 IDomncidom 13789 ℤ_ringczring 14122 ℤRHomczrh 14143 ℤ/nℤczn 14145

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7968 ax-resscn 7969 ax-1cn 7970 ax-1re 7971 ax-icn 7972 ax-addcl 7973 ax-addrcl 7974 ax-mulcl 7975 ax-mulrcl 7976 ax-addcom 7977 ax-mulcom 7978 ax-addass 7979 ax-mulass 7980 ax-distr 7981 ax-i2m1 7982 ax-0lt1 7983 ax-1rid 7984 ax-0id 7985 ax-rnegex 7986 ax-precex 7987 ax-cnre 7988 ax-pre-ltirr 7989 ax-pre-ltwlin 7990 ax-pre-lttrn 7991 ax-pre-apti 7992 ax-pre-ltadd 7993 ax-pre-mulgt0 7994 ax-pre-mulext 7995 ax-arch 7996 ax-caucvg 7997 ax-addf 7999 ax-mulf 8000

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 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-tp 3630 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-of 6135 df-1st 6198 df-2nd 6199 df-tpos 6303 df-recs 6363 df-irdg 6428 df-frec 6449 df-1o 6474 df-2o 6475 df-oadd 6478 df-er 6592 df-ec 6594 df-qs 6598 df-map 6709 df-en 6800 df-dom 6801 df-fin 6802 df-sup 7048 df-pnf 8061 df-mnf 8062 df-xr 8063 df-ltxr 8064 df-le 8065 df-sub 8197 df-neg 8198 df-reap 8599 df-ap 8606 df-div 8697 df-inn 8988 df-2 9046 df-3 9047 df-4 9048 df-5 9049 df-6 9050 df-7 9051 df-8 9052 df-9 9053 df-n0 9247 df-z 9324 df-dec 9455 df-uz 9599 df-q 9691 df-rp 9726 df-fz 10081 df-fzo 10215 df-fl 10345 df-mod 10400 df-seqfrec 10525 df-exp 10616 df-ihash 10853 df-cj 10992 df-re 10993 df-im 10994 df-rsqrt 11148 df-abs 11149 df-dvds 11937 df-gcd 12086 df-prm 12252 df-struct 12656 df-ndx 12657 df-slot 12658 df-base 12660 df-sets 12661 df-iress 12662 df-plusg 12744 df-mulr 12745 df-starv 12746 df-sca 12747 df-vsca 12748 df-ip 12749 df-tset 12750 df-ple 12751 df-ds 12753 df-unif 12754 df-0g 12905 df-igsum 12906 df-topgen 12907 df-iimas 12921 df-qus 12922 df-mgm 12975 df-sgrp 13021 df-mnd 13034 df-mhm 13067 df-submnd 13068 df-grp 13111 df-minusg 13112 df-sbg 13113 df-mulg 13226 df-subg 13276 df-nsg 13277 df-eqg 13278 df-ghm 13347 df-cmn 13392 df-abl 13393 df-mgp 13453 df-rng 13465 df-ur 13492 df-srg 13496 df-ring 13530 df-cring 13531 df-oppr 13600 df-dvdsr 13621 df-unit 13622 df-invr 13653 df-dvr 13664 df-rhm 13684 df-nzr 13712 df-subrg 13751 df-domn 13791 df-idom 13792 df-lmod 13821 df-lssm 13885 df-lsp 13919 df-sra 13967 df-rgmod 13968 df-lidl 14001 df-rsp 14002 df-2idl 14032 df-bl 14078 df-mopn 14079 df-fg 14081 df-metu 14082 df-cnfld 14089 df-zring 14123 df-zrh 14146 df-zn 14148

This theorem is referenced by: lgseisenlem4 15281

W3C validator