Step | Hyp | Ref
| Expression |
1 | | oveq2 5918 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥)) |
2 | 1 | fveq2d 5550 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥))) |
3 | 2 | cbvmptv 4125 |
. . . . . . 7
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) |
4 | 3 | oveq2i 5921 |
. . . . . 6
⊢ (𝐺 Σg
(𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) |
5 | | eqid 2193 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | | eqid 2193 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
7 | | lgseisen.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
8 | 7 | eldifad 3164 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
9 | | lgseisen.7 |
. . . . . . . . . . 11
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
10 | 9 | znidom 14122 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ IDomn) |
11 | 8, 10 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ IDomn) |
12 | 11 | idomcringd 13758 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ CRing) |
13 | | lgseisen.8 |
. . . . . . . . 9
⊢ 𝐺 = (mulGrp‘𝑌) |
14 | 13 | crngmgp 13484 |
. . . . . . . 8
⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd) |
15 | 12, 14 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ CMnd) |
16 | | 1zzd 9334 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
17 | | oddn2prm 12389 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ¬ 2 ∥ 𝑃) |
18 | 7, 17 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ¬ 2 ∥ 𝑃) |
19 | | prmz 12239 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
20 | | oddm1d2 12023 |
. . . . . . . . 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 13759 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Ring) |
24 | | lgseisen.9 |
. . . . . . . . . . . 12
⊢ 𝐿 = (ℤRHom‘𝑌) |
25 | 24 | zrhrhm 14088 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
26 | | zringbas 14062 |
. . . . . . . . . . . 12
⊢ ℤ =
(Base‘ℤring) |
27 | | eqid 2193 |
. . . . . . . . . . . 12
⊢
(Base‘𝑌) =
(Base‘𝑌) |
28 | 26, 27 | rhmf 13643 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
29 | 23, 25, 28 | 3syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
30 | | 2z 9335 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
31 | | elfzelz 10081 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ) |
32 | | zmulcl 9360 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑘
∈ ℤ) → (2 · 𝑘) ∈ ℤ) |
33 | 30, 31, 32 | sylancr 414 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈
ℤ) |
34 | | ffvelcdm 5683 |
. . . . . . . . . 10
⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌)) |
35 | 29, 33, 34 | syl2an 289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌)) |
36 | 35 | fmpttd 5705 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) |
37 | 13, 27 | mgpbasg 13406 |
. . . . . . . . . 10
⊢ (𝑌 ∈ CRing →
(Base‘𝑌) =
(Base‘𝐺)) |
38 | 12, 37 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑌) = (Base‘𝐺)) |
39 | 38 | feq3d 5384 |
. . . . . . . 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 15135 |
. . . . . . 7
⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2))) |
47 | 5, 6, 15, 16, 22, 40, 46 | gsumfzreidx 13396 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀))) |
48 | 4, 47 | eqtr3id 2240 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀))) |
49 | 7, 41, 42, 43, 44 | lgseisenlem1 15134 |
. . . . . . . 8
⊢ (𝜑 → 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) /
2))) |
50 | 44 | fmpt 5700 |
. . . . . . . 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 2194 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) |
54 | | oveq2 5918 |
. . . . . . . 8
⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) |
55 | 54 | fveq2d 5550 |
. . . . . . 7
⊢ (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) |
56 | 51, 52, 53, 55 | fmptcof 5717 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) |
57 | 56 | oveq2d 5926 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))) |
58 | 41 | eldifad 3164 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑄 ∈ ℙ) |
59 | 58 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ) |
60 | | prmz 12239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
61 | 59, 60 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ) |
62 | | 2nn 9133 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℕ |
63 | | elfznn 10110 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
64 | 63 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ) |
65 | | nnmulcl 8993 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℕ ∧ 𝑥
∈ ℕ) → (2 · 𝑥) ∈ ℕ) |
66 | 62, 64, 65 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℕ) |
67 | 66 | nnzd 9428 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℤ) |
68 | 61, 67 | zmulcld 9435 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ) |
69 | 8 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) |
70 | | prmnn 12238 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
71 | 69, 70 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
72 | 68, 71 | zmodcld 10406 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈
ℕ0) |
73 | 43, 72 | eqeltrid 2280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈
ℕ0) |
74 | 73 | nn0zd 9427 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ) |
75 | | m1expcl 10623 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℤ →
(-1↑𝑅) ∈
ℤ) |
76 | 74, 75 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℤ) |
77 | 76, 74 | zmulcld 9435 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ) |
78 | 77, 71 | zmodcld 10406 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈
ℕ0) |
79 | 78 | nn0cnd 9285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ) |
80 | | 2cnd 9045 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℂ) |
81 | | 2ap0 9065 |
. . . . . . . . . . . 12
⊢ 2 #
0 |
82 | 81 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 #
0) |
83 | 79, 80, 82 | divcanap2d 8801 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ·
((((-1↑𝑅) ·
𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃)) |
84 | 83 | fveq2d 5550 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃))) |
85 | | zq 9681 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℚ) |
86 | 8, 19, 85 | 3syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℚ) |
87 | 86 | adantr 276 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℚ) |
88 | 71 | nngt0d 9016 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 𝑃) |
89 | | eqidd 2194 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃)) |
90 | 43 | oveq1i 5920 |
. . . . . . . . . . . . . 14
⊢ (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) |
91 | | zq 9681 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑄 · (2 · 𝑥)) ∈ ℤ → (𝑄 · (2 · 𝑥)) ∈
ℚ) |
92 | 68, 91 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℚ) |
93 | | modqabs2 10419 |
. . . . . . . . . . . . . . 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 2238 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃)) |
96 | 76, 76, 74, 68, 87, 88, 89, 95 | modqmul12d 10439 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)) |
97 | | zq 9681 |
. . . . . . . . . . . . . 14
⊢
(((-1↑𝑅)
· 𝑅) ∈ ℤ
→ ((-1↑𝑅)
· 𝑅) ∈
ℚ) |
98 | 77, 97 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℚ) |
99 | | modqabs2 10419 |
. . . . . . . . . . . . 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 9430 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℂ) |
102 | 61 | zcnd 9430 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ) |
103 | 67 | zcnd 9430 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℂ) |
104 | 101, 102,
103 | mulassd 8033 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥)))) |
105 | 104 | oveq1d 5925 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃)) |
106 | 96, 100, 105 | 3eqtr4d 2236 |
. . . . . . . . . . 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 9427 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ) |
110 | 76, 61 | zmulcld 9435 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ) |
111 | 110, 67 | zmulcld 9435 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) |
112 | | moddvds 11932 |
. . . . . . . . . . . 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 9283 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈
ℕ0) |
116 | 9, 24 | zndvds 14114 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℕ0
∧ (((-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 14065 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
122 | | eqid 2193 |
. . . . . . . . . . 11
⊢
(.r‘𝑌) = (.r‘𝑌) |
123 | 26, 121, 122 | rhmmul 13644 |
. . . . . . . . . 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 2230 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥)))) |
126 | 125 | mpteq2dva 4119 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥))))) |
127 | 16, 22 | fzfigd 10492 |
. . . . . . . 8
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) |
128 | 29 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
129 | 128, 110 | ffvelcdmd 5686 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌)) |
130 | 128, 67 | ffvelcdmd 5686 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌)) |
131 | | eqidd 2194 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) |
132 | | eqidd 2194 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) |
133 | 127, 129,
130, 131, 132 | offval2 6138 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r‘𝑌)(𝐿‘(2 · 𝑥))))) |
134 | 126, 133 | eqtr4d 2229 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) |
135 | 134 | oveq2d 5926 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
136 | 48, 57, 135 | 3eqtrd 2230 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
137 | | eqid 2193 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
138 | 38 | eleq2d 2263 |
. . . . . . . 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 2263 |
. . . . . . . 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 2193 |
. . . . . 6
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) |
145 | | eqid 2193 |
. . . . . 6
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) |
146 | 5, 137, 15, 16, 22, 140, 143, 144, 145 | gsumfzmptfidmadd2 13399 |
. . . . 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 13404 |
. . . . . . . . 9
⊢ (𝑌 ∈ CRing →
(.r‘𝑌) =
(+g‘𝐺)) |
148 | 12, 147 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (.r‘𝑌) = (+g‘𝐺)) |
149 | 148 | ofeqd 6124 |
. . . . . . 7
⊢ (𝜑 →
∘𝑓 (.r‘𝑌) = ∘𝑓
(+g‘𝐺)) |
150 | 149 | oveqd 5927 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(+g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) |
151 | 150 | oveq2d 5926 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓
(+g‘𝐺)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
152 | 148 | oveqd 5927 |
. . . . 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 2236 |
. . . 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 2226 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))) |
155 | 154 | oveq1d 5925 |
. 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 13367 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Mnd) |
157 | | eqid 2193 |
. . . . . 6
⊢
(Unit‘𝑌) =
(Unit‘𝑌) |
158 | 157, 13 | unitsubm 13599 |
. . . . 5
⊢ (𝑌 ∈ Ring →
(Unit‘𝑌) ∈
(SubMnd‘𝐺)) |
159 | 23, 158 | syl 14 |
. . . 4
⊢ (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺)) |
160 | | elfzle2 10084 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
161 | 160 | adantl 277 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
162 | 64 | nnred 8985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ) |
163 | | prmuz2 12259 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
164 | | uz2m1nn 9660 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 1) ∈ ℕ) |
165 | 69, 163, 164 | 3syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ) |
166 | 165 | nnred 8985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ) |
167 | | 2re 9042 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
168 | 167 | a1i 9 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℝ) |
169 | | 2pos 9063 |
. . . . . . . . . . 11
⊢ 0 <
2 |
170 | 169 | a1i 9 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 <
2) |
171 | | lemuldiv2 8891 |
. . . . . . . . . 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 9345 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
176 | | fznn 10145 |
. . . . . . . . 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 11988 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ (2
· 𝑥) ∈
(1...(𝑃 − 1))) →
¬ 𝑃 ∥ (2 ·
𝑥)) |
180 | 71, 178, 179 | syl2anc 411 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥)) |
181 | 9, 157, 24 | znunit 14124 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ0
∧ (2 · 𝑥) ∈
ℤ) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((2 · 𝑥) gcd 𝑃) = 1)) |
182 | 115, 67, 181 | syl2anc 411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((2 · 𝑥) gcd 𝑃) = 1)) |
183 | | coprm 12272 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (2
· 𝑥) ∈ ℤ)
→ (¬ 𝑃 ∥ (2
· 𝑥) ↔ (𝑃 gcd (2 · 𝑥)) = 1)) |
184 | 19 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ (2
· 𝑥) ∈ ℤ)
→ 𝑃 ∈
ℤ) |
185 | | simpr 110 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ (2
· 𝑥) ∈ ℤ)
→ (2 · 𝑥)
∈ ℤ) |
186 | 184, 185 | gcdcomd 12101 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (2
· 𝑥) ∈ ℤ)
→ (𝑃 gcd (2 ·
𝑥)) = ((2 · 𝑥) gcd 𝑃)) |
187 | 186 | eqeq1d 2202 |
. . . . . . . . 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 5705 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌)) |
193 | 156, 16, 22, 159, 192 | gsumfzsubmcl 13397 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) |
194 | | eqid 2193 |
. . . 4
⊢
(/r‘𝑌) = (/r‘𝑌) |
195 | | eqid 2193 |
. . . 4
⊢
(1r‘𝑌) = (1r‘𝑌) |
196 | 157, 194,
195 | dvrid 13617 |
. . 3
⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σg
(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r‘𝑌)) |
197 | 23, 193, 196 | syl2anc 411 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r‘𝑌)) |
198 | 129 | fmpttd 5705 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) |
199 | 38 | feq3d 5384 |
. . . . . 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 13061 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝐺)) |
202 | 201, 38 | eleqtrrd 2273 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌)) |
203 | 27, 157, 194, 122 | dvrcan3 13621 |
. . 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 2235 |
1
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r‘𝑌)) |