Step | Hyp | Ref
| Expression |
1 | | oveq2 7239 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥)) |
2 | 1 | fveq2d 6739 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥))) |
3 | 2 | cbvmptv 5172 |
. . . . . . 7
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) |
4 | 3 | oveq2i 7242 |
. . . . . 6
⊢ (𝐺 Σg
(𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) |
5 | | lgseisen.8 |
. . . . . . . 8
⊢ 𝐺 = (mulGrp‘𝑌) |
6 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
7 | 5, 6 | mgpbas 19534 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝐺) |
8 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
9 | | lgseisen.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
10 | 9 | eldifad 3892 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
11 | | lgseisen.7 |
. . . . . . . . . . 11
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
12 | 11 | znfld 20549 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
13 | 10, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ Field) |
14 | | isfld 19800 |
. . . . . . . . . 10
⊢ (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing)) |
15 | 14 | simprbi 500 |
. . . . . . . . 9
⊢ (𝑌 ∈ Field → 𝑌 ∈ CRing) |
16 | 13, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ CRing) |
17 | 5 | crngmgp 19594 |
. . . . . . . 8
⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ CMnd) |
19 | | fzfid 13570 |
. . . . . . 7
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) |
20 | | crngring 19598 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Ring) |
22 | | lgseisen.9 |
. . . . . . . . . . . 12
⊢ 𝐿 = (ℤRHom‘𝑌) |
23 | 22 | zrhrhm 20502 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) |
25 | | zringbas 20465 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
26 | 25, 6 | rhmf 19770 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
27 | 24, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
28 | | 2z 12233 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
29 | | elfzelz 13136 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ) |
30 | | zmulcl 12250 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 𝑘
∈ ℤ) → (2 · 𝑘) ∈ ℤ) |
31 | 28, 29, 30 | sylancr 590 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈
ℤ) |
32 | | ffvelrn 6920 |
. . . . . . . . 9
⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌)) |
33 | 27, 31, 32 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌)) |
34 | 33 | fmpttd 6950 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) |
35 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) |
36 | | fvexd 6750 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ V) |
37 | | fvexd 6750 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
38 | 35, 19, 36, 37 | fsuppmptdm 9020 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) finSupp (0g‘𝐺)) |
39 | | lgseisen.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
40 | | lgseisen.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
41 | | lgseisen.4 |
. . . . . . . 8
⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) |
42 | | lgseisen.5 |
. . . . . . . 8
⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) |
43 | | lgseisen.6 |
. . . . . . . 8
⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃) |
44 | 9, 39, 40, 41, 42, 43 | lgseisenlem2 26281 |
. . . . . . 7
⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2))) |
45 | 7, 8, 18, 19, 34, 38, 44 | gsumf1o 19325 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀))) |
46 | 4, 45 | eqtr3id 2793 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀))) |
47 | 9, 39, 40, 41, 42 | lgseisenlem1 26280 |
. . . . . . . 8
⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) /
2))) |
48 | 42 | fmpt 6945 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(1...((𝑃 − 1) /
2))((((-1↑𝑅) ·
𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) /
2))) |
49 | 47, 48 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2))) |
50 | 42 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) |
51 | | eqidd 2739 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) |
52 | | oveq2 7239 |
. . . . . . . 8
⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) |
53 | 52 | fveq2d 6739 |
. . . . . . 7
⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) |
54 | 49, 50, 51, 53 | fmptcof 6963 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) |
55 | 54 | oveq2d 7247 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))) |
56 | 39 | eldifad 3892 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑄 ∈ ℙ) |
57 | 56 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ) |
58 | | prmz 16256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ) |
60 | | 2nn 11927 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℕ |
61 | | elfznn 13165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
62 | 61 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ) |
63 | | nnmulcl 11878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℕ ∧ 𝑥
∈ ℕ) → (2 · 𝑥) ∈ ℕ) |
64 | 60, 62, 63 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℕ) |
65 | 64 | nnzd 12305 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℤ) |
66 | 59, 65 | zmulcld 12312 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ) |
67 | 10 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) |
68 | | prmnn 16255 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
70 | 66, 69 | zmodcld 13489 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈
ℕ0) |
71 | 41, 70 | eqeltrid 2843 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈
ℕ0) |
72 | 71 | nn0zd 12304 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ) |
73 | | m1expcl 13682 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℤ →
(-1↑𝑅) ∈
ℤ) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℤ) |
75 | 74, 72 | zmulcld 12312 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ) |
76 | 75, 69 | zmodcld 13489 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈
ℕ0) |
77 | 76 | nn0cnd 12176 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ) |
78 | | 2cnd 11932 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℂ) |
79 | | 2ne0 11958 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
80 | 79 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ≠
0) |
81 | 77, 78, 80 | divcan2d 11634 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ·
((((-1↑𝑅) ·
𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃)) |
82 | 81 | fveq2d 6739 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃))) |
83 | 69 | nnrpd 12650 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈
ℝ+) |
84 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃)) |
85 | 41 | oveq1i 7241 |
. . . . . . . . . . . . . 14
⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) |
86 | 66 | zred 12306 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ) |
87 | | modabs2 13502 |
. . . . . . . . . . . . . . 15
⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ (((𝑄 · (2
· 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃)) |
88 | 86, 83, 87 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃)) |
89 | 85, 88 | syl5eq 2791 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃)) |
90 | 74, 74, 72, 66, 83, 84, 89 | modmul12d 13522 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)) |
91 | 75 | zred 12306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℝ) |
92 | | modabs2 13502 |
. . . . . . . . . . . . 13
⊢
((((-1↑𝑅)
· 𝑅) ∈ ℝ
∧ 𝑃 ∈
ℝ+) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)) |
93 | 91, 83, 92 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃)) |
94 | 74 | zcnd 12307 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℂ) |
95 | 59 | zcnd 12307 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ) |
96 | 65 | zcnd 12307 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℂ) |
97 | 94, 95, 96 | mulassd 10880 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))) |
98 | 97 | oveq1d 7246 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)) |
99 | 90, 93, 98 | 3eqtr4d 2788 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃)) |
100 | 10, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℕ) |
101 | 100 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
102 | 76 | nn0zd 12304 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ) |
103 | 74, 59 | zmulcld 12312 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ) |
104 | 103, 65 | zmulcld 12312 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) |
105 | | moddvds 15850 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧
(((-1↑𝑅) ·
𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
106 | 101, 102,
104, 105 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
107 | 99, 106 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))) |
108 | 69 | nnnn0d 12174 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈
ℕ0) |
109 | 11, 22 | zndvds 20538 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ0
∧ (((-1↑𝑅)
· 𝑅) mod 𝑃) ∈ ℤ ∧
(((-1↑𝑅) ·
𝑄) · (2 ·
𝑥)) ∈ ℤ) →
((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
110 | 108, 102,
104, 109 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))) |
111 | 107, 110 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥)))) |
112 | 24 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤring RingHom
𝑌)) |
113 | | zringmulr 20468 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
114 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(.r‘𝑌) = (.r‘𝑌) |
115 | 25, 113, 114 | rhmmul 19771 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑌) ∧
((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2
· 𝑥) ∈ ℤ)
→ (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥)))) |
116 | 112, 103,
65, 115 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥)))) |
117 | 82, 111, 116 | 3eqtrd 2782 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥)))) |
118 | 117 | mpteq2dva 5164 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥))))) |
119 | 27 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
120 | 119, 103 | ffvelrnd 6923 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌)) |
121 | 119, 65 | ffvelrnd 6923 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌)) |
122 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) |
123 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) |
124 | 19, 120, 121, 122, 123 | offval2 7506 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥))))) |
125 | 118, 124 | eqtr4d 2781 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) |
126 | 125 | oveq2d 7247 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
127 | 46, 55, 126 | 3eqtrd 2782 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
128 | 5, 114 | mgpplusg 19532 |
. . . . 5
⊢
(.r‘𝑌) = (+g‘𝐺) |
129 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) |
130 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) |
131 | 7, 128, 18, 19, 120, 121, 129, 130 | gsummptfidmadd2 19335 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
132 | 127, 131 | eqtrd 2778 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
133 | 132 | oveq1d 7246 |
. 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 · 𝑥)))))) |
134 | | eqid 2738 |
. . . . . 6
⊢
(Unit‘𝑌) =
(Unit‘𝑌) |
135 | 134, 5 | unitsubm 19712 |
. . . . 5
⊢ (𝑌 ∈ Ring →
(Unit‘𝑌) ∈
(SubMnd‘𝐺)) |
136 | 21, 135 | syl 17 |
. . . 4
⊢ (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺)) |
137 | | elfzle2 13140 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
138 | 137 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
139 | 62 | nnred 11869 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ) |
140 | | prmuz2 16277 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
141 | | uz2m1nn 12543 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 1) ∈ ℕ) |
142 | 67, 140, 141 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ) |
143 | 142 | nnred 11869 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ) |
144 | | 2re 11928 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
145 | 144 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℝ) |
146 | | 2pos 11957 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
147 | 146 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 <
2) |
148 | | lemuldiv2 11737 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
149 | 139, 143,
145, 147, 148 | syl112anc 1376 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
150 | 138, 149 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1)) |
151 | | prmz 16256 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
152 | 67, 151 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) |
153 | | peano2zm 12244 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
154 | 152, 153 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℤ) |
155 | | fznn 13204 |
. . . . . . . . . 10
⊢ ((𝑃 − 1) ∈ ℤ
→ ((2 · 𝑥)
∈ (1...(𝑃 − 1))
↔ ((2 · 𝑥)
∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1)))) |
156 | 154, 155 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2
· 𝑥) ≤ (𝑃 − 1)))) |
157 | 64, 150, 156 | mpbir2and 713 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1))) |
158 | | fzm1ndvds 15907 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ (2
· 𝑥) ∈
(1...(𝑃 − 1))) →
¬ 𝑃 ∥ (2 ·
𝑥)) |
159 | 69, 157, 158 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥)) |
160 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘𝑌) = (0g‘𝑌) |
161 | 11, 22, 160 | zndvds0 20539 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ0
∧ (2 · 𝑥) ∈
ℤ) → ((𝐿‘(2 · 𝑥)) = (0g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥))) |
162 | 108, 65, 161 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) = (0g‘𝑌) ↔ 𝑃 ∥ (2 · 𝑥))) |
163 | 162 | necon3abid 2978 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ≠
(0g‘𝑌)
↔ ¬ 𝑃 ∥ (2
· 𝑥))) |
164 | 159, 163 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ≠ (0g‘𝑌)) |
165 | 14 | simplbi 501 |
. . . . . . . . 9
⊢ (𝑌 ∈ Field → 𝑌 ∈
DivRing) |
166 | 13, 165 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ DivRing) |
167 | 166 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑌 ∈ DivRing) |
168 | 6, 134, 160 | drngunit 19796 |
. . . . . . 7
⊢ (𝑌 ∈ DivRing → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g‘𝑌)))) |
169 | 167, 168 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g‘𝑌)))) |
170 | 121, 164,
169 | mpbir2and 713 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌)) |
171 | 170 | fmpttd 6950 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌)) |
172 | | fvexd 6750 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ V) |
173 | 130, 19, 172, 37 | fsuppmptdm 9020 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) finSupp (0g‘𝐺)) |
174 | 8, 18, 19, 136, 171, 173 | gsumsubmcl 19328 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) |
175 | | eqid 2738 |
. . . 4
⊢
(/r‘𝑌) = (/r‘𝑌) |
176 | | eqid 2738 |
. . . 4
⊢
(1r‘𝑌) = (1r‘𝑌) |
177 | 134, 175,
176 | dvrid 19730 |
. . 3
⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σg
(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r‘𝑌)) |
178 | 21, 174, 177 | syl2anc 587 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r‘𝑌)) |
179 | 120 | fmpttd 6950 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) |
180 | | fvexd 6750 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ V) |
181 | 129, 19, 180, 37 | fsuppmptdm 9020 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) finSupp (0g‘𝐺)) |
182 | 7, 8, 18, 19, 179, 181 | gsumcl 19324 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌)) |
183 | 6, 134, 175, 114 | dvrcan3 19734 |
. . 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↑𝑅) · 𝑄))))) |
184 | 21, 182, 174, 183 | syl3anc 1373 |
. 2
⊢ (𝜑 → (((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) |
185 | 133, 178,
184 | 3eqtr3rd 2787 |
1
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r‘𝑌)) |