| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zringbas 21465 | . . . . 5
⊢ ℤ =
(Base‘ℤring) | 
| 2 |  | zring0 21470 | . . . . 5
⊢ 0 =
(0g‘ℤring) | 
| 3 |  | zringabl 21463 | . . . . . 6
⊢
ℤring ∈ Abel | 
| 4 |  | ablcmn 19806 | . . . . . 6
⊢
(ℤring ∈ Abel → ℤring ∈
CMnd) | 
| 5 | 3, 4 | mp1i 13 | . . . . 5
⊢ (𝜑 → ℤring
∈ CMnd) | 
| 6 |  | lgseisen.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) | 
| 7 | 6 | eldifad 3962 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 8 |  | lgseisen.7 | . . . . . . . . . 10
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) | 
| 9 | 8 | znfld 21580 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) | 
| 10 | 7, 9 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ Field) | 
| 11 |  | isfld 20741 | . . . . . . . . 9
⊢ (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing)) | 
| 12 | 11 | simprbi 496 | . . . . . . . 8
⊢ (𝑌 ∈ Field → 𝑌 ∈ CRing) | 
| 13 | 10, 12 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ CRing) | 
| 14 |  | lgseisen.8 | . . . . . . . 8
⊢ 𝐺 = (mulGrp‘𝑌) | 
| 15 | 14 | crngmgp 20239 | . . . . . . 7
⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd) | 
| 16 | 13, 15 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ CMnd) | 
| 17 |  | cmnmnd 19816 | . . . . . 6
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | 
| 18 | 16, 17 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) | 
| 19 |  | fzfid 14015 | . . . . 5
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) | 
| 20 |  | crngring 20243 | . . . . . . . . . 10
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) | 
| 21 | 13, 20 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ Ring) | 
| 22 |  | lgseisen.9 | . . . . . . . . . 10
⊢ 𝐿 = (ℤRHom‘𝑌) | 
| 23 | 22 | zrhrhm 21523 | . . . . . . . . 9
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) | 
| 24 | 21, 23 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) | 
| 25 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 26 | 1, 25 | rhmf 20486 | . . . . . . . 8
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) | 
| 27 | 24, 26 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) | 
| 28 |  | m1expcl 14128 | . . . . . . . 8
⊢ (𝑘 ∈ ℤ →
(-1↑𝑘) ∈
ℤ) | 
| 29 | 28 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈
ℤ) | 
| 30 | 27, 29 | cofmpt 7151 | . . . . . 6
⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) = (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘)))) | 
| 31 |  | zringmpg 21483 | . . . . . . . . 9
⊢
((mulGrp‘ℂfld) ↾s ℤ) =
(mulGrp‘ℤring) | 
| 32 | 31, 14 | rhmmhm 20480 | . . . . . . . 8
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺)) | 
| 33 | 24, 32 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺)) | 
| 34 |  | neg1cn 12381 | . . . . . . . . . . 11
⊢ -1 ∈
ℂ | 
| 35 |  | neg1ne0 12383 | . . . . . . . . . . 11
⊢ -1 ≠
0 | 
| 36 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) | 
| 37 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) | 
| 38 | 36, 37 | expghm 21487 | . . . . . . . . . . 11
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring GrpHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))) | 
| 39 | 34, 35, 38 | mp2an 692 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring GrpHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) | 
| 40 |  | ghmmhm 19245 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring GrpHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))) | 
| 41 | 39, 40 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) | 
| 42 |  | cnring 21404 | . . . . . . . . . 10
⊢
ℂfld ∈ Ring | 
| 43 |  | cnfldbas 21369 | . . . . . . . . . . . 12
⊢ ℂ =
(Base‘ℂfld) | 
| 44 |  | cnfld0 21406 | . . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) | 
| 45 |  | cndrng 21412 | . . . . . . . . . . . 12
⊢
ℂfld ∈ DivRing | 
| 46 | 43, 44, 45 | drngui 20736 | . . . . . . . . . . 11
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) | 
| 47 | 46, 36 | unitsubm 20387 | . . . . . . . . . 10
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld))) | 
| 48 | 42, 47 | ax-mp 5 | . . . . . . . . 9
⊢ (ℂ
∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld)) | 
| 49 | 37 | resmhm2 18835 | . . . . . . . . 9
⊢ (((𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) ∧ (ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom
(mulGrp‘ℂfld))) | 
| 50 | 41, 48, 49 | mp2an 692 | . . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom
(mulGrp‘ℂfld)) | 
| 51 |  | zsubrg 21439 | . . . . . . . . . 10
⊢ ℤ
∈ (SubRing‘ℂfld) | 
| 52 | 36 | subrgsubm 20586 | . . . . . . . . . 10
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubMnd‘(mulGrp‘ℂfld))) | 
| 53 | 51, 52 | ax-mp 5 | . . . . . . . . 9
⊢ ℤ
∈ (SubMnd‘(mulGrp‘ℂfld)) | 
| 54 | 29 | fmpttd 7134 | . . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)):ℤ⟶ℤ) | 
| 55 | 54 | frnd 6743 | . . . . . . . . 9
⊢ (𝜑 → ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆
ℤ) | 
| 56 |  | eqid 2736 | . . . . . . . . . 10
⊢
((mulGrp‘ℂfld) ↾s ℤ) =
((mulGrp‘ℂfld) ↾s
ℤ) | 
| 57 | 56 | resmhm2b 18836 | . . . . . . . . 9
⊢ ((ℤ
∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ ran (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ⊆
ℤ) → ((𝑘 ∈
ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom
(mulGrp‘ℂfld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ)))) | 
| 58 | 53, 55, 57 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom (mulGrp‘ℂfld)) ↔
(𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ)))) | 
| 59 | 50, 58 | mpbii 233 | . . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ))) | 
| 60 |  | mhmco 18837 | . . . . . . 7
⊢ ((𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺) ∧ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ))) → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈
(ℤring MndHom 𝐺)) | 
| 61 | 33, 59, 60 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈
(ℤring MndHom 𝐺)) | 
| 62 | 30, 61 | eqeltrrd 2841 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))) ∈ (ℤring MndHom
𝐺)) | 
| 63 |  | lgseisen.2 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) | 
| 64 | 63 | gausslemma2dlem0a 27401 | . . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℕ) | 
| 65 | 64 | nnred 12282 | . . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ℝ) | 
| 66 | 6 | gausslemma2dlem0a 27401 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 67 | 65, 66 | nndivred 12321 | . . . . . . . 8
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) | 
| 68 | 67 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℝ) | 
| 69 |  | 2nn 12340 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 70 |  | elfznn 13594 | . . . . . . . . . 10
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) | 
| 71 | 70 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ) | 
| 72 |  | nnmulcl 12291 | . . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑥
∈ ℕ) → (2 · 𝑥) ∈ ℕ) | 
| 73 | 69, 71, 72 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℕ) | 
| 74 | 73 | nnred 12282 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℝ) | 
| 75 | 68, 74 | remulcld 11292 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℝ) | 
| 76 | 75 | flcld 13839 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈
ℤ) | 
| 77 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) | 
| 78 |  | fvexd 6920 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ V) | 
| 79 |  | c0ex 11256 | . . . . . . 7
⊢ 0 ∈
V | 
| 80 | 79 | a1i 11 | . . . . . 6
⊢ (𝜑 → 0 ∈
V) | 
| 81 | 77, 19, 78, 80 | fsuppmptdm 9417 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) finSupp 0) | 
| 82 |  | oveq2 7440 | . . . . . 6
⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (-1↑𝑘) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | 
| 83 | 82 | fveq2d 6909 | . . . . 5
⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) | 
| 84 |  | oveq2 7440 | . . . . . 6
⊢ (𝑘 = (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (-1↑𝑘) =
(-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) | 
| 85 | 84 | fveq2d 6909 | . . . . 5
⊢ (𝑘 = (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) | 
| 86 | 1, 2, 5, 18, 19, 62, 76, 81, 83, 85 | gsummhm2 19958 | . . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑(ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) | 
| 87 | 14, 25 | mgpbas 20143 | . . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝐺) | 
| 88 |  | eqid 2736 | . . . . . . . 8
⊢
(.r‘𝑌) = (.r‘𝑌) | 
| 89 | 14, 88 | mgpplusg 20142 | . . . . . . 7
⊢
(.r‘𝑌) = (+g‘𝐺) | 
| 90 | 27 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) | 
| 91 |  | m1expcl 14128 | . . . . . . . . 9
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥))) ∈ ℤ →
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈
ℤ) | 
| 92 | 76, 91 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈
ℤ) | 
| 93 | 90, 92 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝑌)) | 
| 94 |  | neg1z 12655 | . . . . . . . . . 10
⊢ -1 ∈
ℤ | 
| 95 |  | lgseisen.4 | . . . . . . . . . . 11
⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) | 
| 96 | 63 | eldifad 3962 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑄 ∈ ℙ) | 
| 97 | 96 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ) | 
| 98 |  | prmz 16713 | . . . . . . . . . . . . . 14
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) | 
| 99 | 97, 98 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ) | 
| 100 | 73 | nnzd 12642 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℤ) | 
| 101 | 99, 100 | zmulcld 12730 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ) | 
| 102 | 7 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) | 
| 103 |  | prmnn 16712 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 104 | 102, 103 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) | 
| 105 | 101, 104 | zmodcld 13933 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈
ℕ0) | 
| 106 | 95, 105 | eqeltrid 2844 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈
ℕ0) | 
| 107 |  | zexpcl 14118 | . . . . . . . . . 10
⊢ ((-1
∈ ℤ ∧ 𝑅
∈ ℕ0) → (-1↑𝑅) ∈ ℤ) | 
| 108 | 94, 106, 107 | sylancr 587 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℤ) | 
| 109 | 108, 99 | zmulcld 12730 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ) | 
| 110 | 90, 109 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌)) | 
| 111 |  | eqid 2736 | . . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) | 
| 112 |  | eqid 2736 | . . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) | 
| 113 | 87, 89, 16, 19, 93, 110, 111, 112 | gsummptfidmadd2 19945 | . . . . . 6
⊢ (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))) | 
| 114 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) | 
| 115 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) | 
| 116 | 19, 93, 110, 114, 115 | offval2 7718 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))) | 
| 117 | 24 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤring RingHom
𝑌)) | 
| 118 |  | zringmulr 21469 | . . . . . . . . . . . 12
⊢  ·
= (.r‘ℤring) | 
| 119 | 1, 118, 88 | rhmmul 20487 | . . . . . . . . . . 11
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑌) ∧
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈ ℤ ∧
((-1↑𝑅) · 𝑄) ∈ ℤ) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) | 
| 120 | 117, 92, 109, 119 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) | 
| 121 | 101 | zred 12724 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ) | 
| 122 | 104 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈
ℝ+) | 
| 123 |  | modval 13912 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ ((𝑄 · (2
· 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))))) | 
| 124 | 121, 122,
123 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))))) | 
| 125 | 95, 124 | eqtrid 2788 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))))) | 
| 126 | 99 | zcnd 12725 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ) | 
| 127 | 73 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℂ) | 
| 128 | 104 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ) | 
| 129 | 104 | nnne0d 12317 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ≠ 0) | 
| 130 | 126, 127,
128, 129 | div23d 12081 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑥))) | 
| 131 | 130 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 ·
(2 · 𝑥)) / 𝑃)) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) | 
| 132 | 131 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))) = (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | 
| 133 | 132 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) | 
| 134 | 125, 133 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) | 
| 135 | 134 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) | 
| 136 |  | prmz 16713 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 137 | 102, 136 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) | 
| 138 | 137, 76 | zmulcld 12730 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) | 
| 139 | 138 | zcnd 12725 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ) | 
| 140 | 101 | zcnd 12725 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℂ) | 
| 141 | 139, 140 | pncan3d 11624 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑄 · (2 · 𝑥))) | 
| 142 |  | 2cnd 12345 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℂ) | 
| 143 | 71 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℂ) | 
| 144 | 126, 142,
143 | mul12d 11471 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) = (2 · (𝑄 · 𝑥))) | 
| 145 | 135, 141,
144 | 3eqtrd 2780 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = (2 · (𝑄 · 𝑥))) | 
| 146 | 145 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = (-1↑(2 · (𝑄 · 𝑥)))) | 
| 147 | 34 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈
ℂ) | 
| 148 | 35 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ≠
0) | 
| 149 | 106 | nn0zd 12641 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ) | 
| 150 |  | expaddz 14148 | . . . . . . . . . . . . . . . 16
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ 𝑅 ∈ ℤ)) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅))) | 
| 151 | 147, 148,
138, 149, 150 | syl22anc 838 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅))) | 
| 152 |  | expmulz 14150 | . . . . . . . . . . . . . . . . . 18
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (𝑃 ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | 
| 153 | 147, 148,
137, 76, 152 | syl22anc 838 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | 
| 154 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈
ℂ) | 
| 155 |  | eldifsni 4789 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) | 
| 156 | 6, 155 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑃 ≠ 2) | 
| 157 | 156 | necomd 2995 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 2 ≠ 𝑃) | 
| 158 | 157 | neneqd 2944 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 2 = 𝑃) | 
| 159 | 158 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 = 𝑃) | 
| 160 |  | 2z 12651 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℤ | 
| 161 |  | uzid 12894 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) | 
| 162 | 160, 161 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
(ℤ≥‘2) | 
| 163 |  | dvdsprm 16741 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) | 
| 164 | 162, 102,
163 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) | 
| 165 | 159, 164 | mtbird 325 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 ∥
𝑃) | 
| 166 |  | oexpneg 16383 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℂ ∧ 𝑃
∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (-1↑𝑃) = -(1↑𝑃)) | 
| 167 | 154, 104,
165, 166 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -(1↑𝑃)) | 
| 168 |  | 1exp 14133 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℤ →
(1↑𝑃) =
1) | 
| 169 | 137, 168 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑𝑃) = 1) | 
| 170 | 169 | negeqd 11503 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -(1↑𝑃) = -1) | 
| 171 | 167, 170 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -1) | 
| 172 | 171 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | 
| 173 | 153, 172 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | 
| 174 | 173 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅))) | 
| 175 | 151, 174 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅))) | 
| 176 |  | nnmulcl 12291 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (𝑄 · 𝑥) ∈ ℕ) | 
| 177 | 64, 70, 176 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ) | 
| 178 | 177 | nnnn0d 12589 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈
ℕ0) | 
| 179 |  | 2nn0 12545 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ0 | 
| 180 | 179 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℕ0) | 
| 181 | 147, 178,
180 | expmuld 14190 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2
· (𝑄 · 𝑥))) = ((-1↑2)↑(𝑄 · 𝑥))) | 
| 182 |  | neg1sqe1 14236 | . . . . . . . . . . . . . . . . 17
⊢
(-1↑2) = 1 | 
| 183 | 182 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢
((-1↑2)↑(𝑄
· 𝑥)) =
(1↑(𝑄 · 𝑥)) | 
| 184 | 177 | nnzd 12642 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℤ) | 
| 185 |  | 1exp 14133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑄 · 𝑥) ∈ ℤ → (1↑(𝑄 · 𝑥)) = 1) | 
| 186 | 184, 185 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑(𝑄 · 𝑥)) = 1) | 
| 187 | 183, 186 | eqtrid 2788 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
((-1↑2)↑(𝑄
· 𝑥)) =
1) | 
| 188 | 181, 187 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2
· (𝑄 · 𝑥))) = 1) | 
| 189 | 146, 175,
188 | 3eqtr3d 2784 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) = 1) | 
| 190 | 189 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = (1 · 𝑄)) | 
| 191 | 92 | zcnd 12725 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈
ℂ) | 
| 192 | 108 | zcnd 12725 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℂ) | 
| 193 | 191, 192,
126 | mulassd 11285 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) | 
| 194 | 126 | mullidd 11280 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑄) = 𝑄) | 
| 195 | 190, 193,
194 | 3eqtr3d 2784 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)) = 𝑄) | 
| 196 | 195 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄)) | 
| 197 | 120, 196 | eqtr3d 2778 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄)) | 
| 198 | 197 | mpteq2dva 5241 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) | 
| 199 | 116, 198 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) | 
| 200 | 199 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘f
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))) | 
| 201 |  | lgseisen.3 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ≠ 𝑄) | 
| 202 |  | lgseisen.5 | . . . . . . . 8
⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) | 
| 203 |  | lgseisen.6 | . . . . . . . 8
⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃) | 
| 204 | 6, 63, 201, 95, 202, 203, 8, 14, 22 | lgseisenlem3 27422 | . . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r‘𝑌)) | 
| 205 | 204 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌))) | 
| 206 | 113, 200,
205 | 3eqtr3rd 2785 | . . . . 5
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))) | 
| 207 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 208 | 93 | fmpttd 7134 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) | 
| 209 |  | fvexd 6920 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ V) | 
| 210 |  | fvexd 6920 | . . . . . . . 8
⊢ (𝜑 → (0g‘𝐺) ∈ V) | 
| 211 | 111, 19, 209, 210 | fsuppmptdm 9417 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) finSupp (0g‘𝐺)) | 
| 212 | 87, 207, 16, 19, 208, 211 | gsumcl 19934 | . . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌)) | 
| 213 |  | eqid 2736 | . . . . . . 7
⊢
(1r‘𝑌) = (1r‘𝑌) | 
| 214 | 25, 88, 213 | ringridm 20268 | . . . . . 6
⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σg
(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) | 
| 215 | 21, 212, 214 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) | 
| 216 | 96, 98 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℤ) | 
| 217 | 27, 216 | ffvelcdmd 7104 | . . . . . . 7
⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝑌)) | 
| 218 |  | eqid 2736 | . . . . . . . 8
⊢
(.g‘𝐺) = (.g‘𝐺) | 
| 219 | 87, 218 | gsumconst 19953 | . . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (1...((𝑃 − 1) / 2)) ∈ Fin
∧ (𝐿‘𝑄) ∈ (Base‘𝑌)) → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = ((♯‘(1...((𝑃 − 1) /
2)))(.g‘𝐺)(𝐿‘𝑄))) | 
| 220 | 18, 19, 217, 219 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = ((♯‘(1...((𝑃 − 1) /
2)))(.g‘𝐺)(𝐿‘𝑄))) | 
| 221 |  | oddprm 16849 | . . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) | 
| 222 | 6, 221 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) | 
| 223 | 222 | nnnn0d 12589 | . . . . . . . 8
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) | 
| 224 |  | hashfz1 14386 | . . . . . . . 8
⊢ (((𝑃 − 1) / 2) ∈
ℕ0 → (♯‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) / 2)) | 
| 225 | 223, 224 | syl 17 | . . . . . . 7
⊢ (𝜑 →
(♯‘(1...((𝑃
− 1) / 2))) = ((𝑃
− 1) / 2)) | 
| 226 | 225 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 →
((♯‘(1...((𝑃
− 1) / 2)))(.g‘𝐺)(𝐿‘𝑄)) = (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄))) | 
| 227 | 31, 1 | mgpbas 20143 | . . . . . . . . 9
⊢ ℤ =
(Base‘((mulGrp‘ℂfld) ↾s
ℤ)) | 
| 228 |  | eqid 2736 | . . . . . . . . 9
⊢
(.g‘((mulGrp‘ℂfld)
↾s ℤ)) =
(.g‘((mulGrp‘ℂfld) ↾s
ℤ)) | 
| 229 | 227, 228,
218 | mhmmulg 19134 | . . . . . . . 8
⊢ ((𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺) ∧ ((𝑃 − 1) / 2) ∈
ℕ0 ∧ 𝑄
∈ ℤ) → (𝐿‘(((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) = (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄))) | 
| 230 | 33, 223, 216, 229 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (𝐿‘(((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) = (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄))) | 
| 231 | 53 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ℤ ∈
(SubMnd‘(mulGrp‘ℂfld))) | 
| 232 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) | 
| 233 | 232, 56, 228 | submmulg 19137 | . . . . . . . . . 10
⊢ ((ℤ
∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ ((𝑃 − 1) / 2) ∈
ℕ0 ∧ 𝑄
∈ ℤ) → (((𝑃
− 1) / 2)(.g‘(mulGrp‘ℂfld))𝑄) = (((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) | 
| 234 | 231, 223,
216, 233 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝜑 → (((𝑃 − 1) /
2)(.g‘(mulGrp‘ℂfld))𝑄) = (((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) | 
| 235 | 216 | zcnd 12725 | . . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℂ) | 
| 236 |  | cnfldexp 21418 | . . . . . . . . . 10
⊢ ((𝑄 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (((𝑃 − 1) /
2)(.g‘(mulGrp‘ℂfld))𝑄) = (𝑄↑((𝑃 − 1) / 2))) | 
| 237 | 235, 223,
236 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (((𝑃 − 1) /
2)(.g‘(mulGrp‘ℂfld))𝑄) = (𝑄↑((𝑃 − 1) / 2))) | 
| 238 | 234, 237 | eqtr3d 2778 | . . . . . . . 8
⊢ (𝜑 → (((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄) = (𝑄↑((𝑃 − 1) / 2))) | 
| 239 | 238 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 → (𝐿‘(((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) | 
| 240 | 230, 239 | eqtr3d 2778 | . . . . . 6
⊢ (𝜑 → (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) | 
| 241 | 220, 226,
240 | 3eqtrd 2780 | . . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) | 
| 242 | 206, 215,
241 | 3eqtr3d 2784 | . . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) | 
| 243 |  | subrgsubg 20578 | . . . . . . . . . 10
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubGrp‘ℂfld)) | 
| 244 | 51, 243 | ax-mp 5 | . . . . . . . . 9
⊢ ℤ
∈ (SubGrp‘ℂfld) | 
| 245 |  | subgsubm 19167 | . . . . . . . . 9
⊢ (ℤ
∈ (SubGrp‘ℂfld) → ℤ ∈
(SubMnd‘ℂfld)) | 
| 246 | 244, 245 | mp1i 13 | . . . . . . . 8
⊢ (𝜑 → ℤ ∈
(SubMnd‘ℂfld)) | 
| 247 | 76 | fmpttd 7134 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))):(1...((𝑃 − 1) /
2))⟶ℤ) | 
| 248 |  | df-zring 21459 | . . . . . . . 8
⊢
ℤring = (ℂfld ↾s
ℤ) | 
| 249 | 19, 246, 247, 248 | gsumsubm 18849 | . . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) | 
| 250 | 76 | zcnd 12725 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈
ℂ) | 
| 251 | 19, 250 | gsumfsum 21453 | . . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) | 
| 252 | 249, 251 | eqtr3d 2778 | . . . . . 6
⊢ (𝜑 → (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) | 
| 253 | 252 | oveq2d 7448 | . . . . 5
⊢ (𝜑 →
(-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) | 
| 254 | 253 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (𝐿‘(-1↑(ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) | 
| 255 | 86, 242, 254 | 3eqtr3d 2784 | . . 3
⊢ (𝜑 → (𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) | 
| 256 | 66 | nnnn0d 12589 | . . . 4
⊢ (𝜑 → 𝑃 ∈
ℕ0) | 
| 257 |  | zexpcl 14118 | . . . . 5
⊢ ((𝑄 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝑄↑((𝑃 − 1) / 2)) ∈
ℤ) | 
| 258 | 216, 223,
257 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈
ℤ) | 
| 259 | 19, 76 | fsumzcl 15772 | . . . . 5
⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ) | 
| 260 |  | m1expcl 14128 | . . . . 5
⊢
(Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))) ∈ ℤ →
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈
ℤ) | 
| 261 | 259, 260 | syl 17 | . . . 4
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) | 
| 262 | 8, 22 | zndvds 21569 | . . . 4
⊢ ((𝑃 ∈ ℕ0
∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ
∧ (-1↑Σ𝑥
∈ (1...((𝑃 − 1)
/ 2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℤ)
→ ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) | 
| 263 | 256, 258,
261, 262 | syl3anc 1372 | . . 3
⊢ (𝜑 → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) | 
| 264 | 255, 263 | mpbid 232 | . 2
⊢ (𝜑 → 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))))) | 
| 265 |  | moddvds 16302 | . . 3
⊢ ((𝑃 ∈ ℕ ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℤ)
→ (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) | 
| 266 | 66, 258, 261, 265 | syl3anc 1372 | . 2
⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) | 
| 267 | 264, 266 | mpbird 257 | 1
⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃)) |