Step | Hyp | Ref
| Expression |
1 | | zringbas 20878 |
. . . . 5
β’ β€ =
(Baseββ€ring) |
2 | | zring0 20882 |
. . . . 5
β’ 0 =
(0gββ€ring) |
3 | | zringabl 20876 |
. . . . . 6
β’
β€ring β Abel |
4 | | ablcmn 19570 |
. . . . . 6
β’
(β€ring β Abel β β€ring β
CMnd) |
5 | 3, 4 | mp1i 13 |
. . . . 5
β’ (π β β€ring
β CMnd) |
6 | | lgseisen.1 |
. . . . . . . . . 10
β’ (π β π β (β β
{2})) |
7 | 6 | eldifad 3923 |
. . . . . . . . 9
β’ (π β π β β) |
8 | | lgseisen.7 |
. . . . . . . . . 10
β’ π =
(β€/nβ€βπ) |
9 | 8 | znfld 20970 |
. . . . . . . . 9
β’ (π β β β π β Field) |
10 | 7, 9 | syl 17 |
. . . . . . . 8
β’ (π β π β Field) |
11 | | isfld 20197 |
. . . . . . . . 9
β’ (π β Field β (π β DivRing β§ π β CRing)) |
12 | 11 | simprbi 498 |
. . . . . . . 8
β’ (π β Field β π β CRing) |
13 | 10, 12 | syl 17 |
. . . . . . 7
β’ (π β π β CRing) |
14 | | lgseisen.8 |
. . . . . . . 8
β’ πΊ = (mulGrpβπ) |
15 | 14 | crngmgp 19973 |
. . . . . . 7
β’ (π β CRing β πΊ β CMnd) |
16 | 13, 15 | syl 17 |
. . . . . 6
β’ (π β πΊ β CMnd) |
17 | | cmnmnd 19580 |
. . . . . 6
β’ (πΊ β CMnd β πΊ β Mnd) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ (π β πΊ β Mnd) |
19 | | fzfid 13879 |
. . . . 5
β’ (π β (1...((π β 1) / 2)) β
Fin) |
20 | | crngring 19977 |
. . . . . . . . . 10
β’ (π β CRing β π β Ring) |
21 | 13, 20 | syl 17 |
. . . . . . . . 9
β’ (π β π β Ring) |
22 | | lgseisen.9 |
. . . . . . . . . 10
β’ πΏ = (β€RHomβπ) |
23 | 22 | zrhrhm 20915 |
. . . . . . . . 9
β’ (π β Ring β πΏ β (β€ring
RingHom π)) |
24 | 21, 23 | syl 17 |
. . . . . . . 8
β’ (π β πΏ β (β€ring RingHom
π)) |
25 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
26 | 1, 25 | rhmf 20159 |
. . . . . . . 8
β’ (πΏ β (β€ring
RingHom π) β πΏ:β€βΆ(Baseβπ)) |
27 | 24, 26 | syl 17 |
. . . . . . 7
β’ (π β πΏ:β€βΆ(Baseβπ)) |
28 | | m1expcl 13993 |
. . . . . . . 8
β’ (π β β€ β
(-1βπ) β
β€) |
29 | 28 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β€) β (-1βπ) β
β€) |
30 | 27, 29 | cofmpt 7079 |
. . . . . 6
β’ (π β (πΏ β (π β β€ β¦ (-1βπ))) = (π β β€ β¦ (πΏβ(-1βπ)))) |
31 | | zringmpg 20895 |
. . . . . . . . 9
β’
((mulGrpββfld) βΎs β€) =
(mulGrpββ€ring) |
32 | 31, 14 | rhmmhm 20154 |
. . . . . . . 8
β’ (πΏ β (β€ring
RingHom π) β πΏ β
(((mulGrpββfld) βΎs β€) MndHom
πΊ)) |
33 | 24, 32 | syl 17 |
. . . . . . 7
β’ (π β πΏ β
(((mulGrpββfld) βΎs β€) MndHom
πΊ)) |
34 | | neg1cn 12268 |
. . . . . . . . . . 11
β’ -1 β
β |
35 | | neg1ne0 12270 |
. . . . . . . . . . 11
β’ -1 β
0 |
36 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(mulGrpββfld) =
(mulGrpββfld) |
37 | | eqid 2737 |
. . . . . . . . . . . 12
β’
((mulGrpββfld) βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
38 | 36, 37 | expghm 20899 |
. . . . . . . . . . 11
β’ ((-1
β β β§ -1 β 0) β (π β β€ β¦ (-1βπ)) β
(β€ring GrpHom ((mulGrpββfld)
βΎs (β β {0})))) |
39 | 34, 35, 38 | mp2an 691 |
. . . . . . . . . 10
β’ (π β β€ β¦
(-1βπ)) β
(β€ring GrpHom ((mulGrpββfld)
βΎs (β β {0}))) |
40 | | ghmmhm 19019 |
. . . . . . . . . 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 20822 |
. . . . . . . . . 10
β’
βfld β Ring |
43 | | cnfldbas 20803 |
. . . . . . . . . . . 12
β’ β =
(Baseββfld) |
44 | | cnfld0 20824 |
. . . . . . . . . . . 12
β’ 0 =
(0gββfld) |
45 | | cndrng 20829 |
. . . . . . . . . . . 12
β’
βfld β DivRing |
46 | 43, 44, 45 | drngui 20192 |
. . . . . . . . . . 11
β’ (β
β {0}) = (Unitββfld) |
47 | 46, 36 | unitsubm 20100 |
. . . . . . . . . 10
β’
(βfld β Ring β (β β {0}) β
(SubMndβ(mulGrpββfld))) |
48 | 42, 47 | ax-mp 5 |
. . . . . . . . 9
β’ (β
β {0}) β
(SubMndβ(mulGrpββfld)) |
49 | 37 | resmhm2 18633 |
. . . . . . . . 9
β’ (((π β β€ β¦
(-1βπ)) β
(β€ring MndHom ((mulGrpββfld)
βΎs (β β {0}))) β§ (β β {0}) β
(SubMndβ(mulGrpββfld))) β (π β β€ β¦ (-1βπ)) β
(β€ring MndHom
(mulGrpββfld))) |
50 | 41, 48, 49 | mp2an 691 |
. . . . . . . 8
β’ (π β β€ β¦
(-1βπ)) β
(β€ring MndHom
(mulGrpββfld)) |
51 | | zsubrg 20853 |
. . . . . . . . . 10
β’ β€
β (SubRingββfld) |
52 | 36 | subrgsubm 20238 |
. . . . . . . . . 10
β’ (β€
β (SubRingββfld) β β€ β
(SubMndβ(mulGrpββfld))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
β’ β€
β (SubMndβ(mulGrpββfld)) |
54 | 29 | fmpttd 7064 |
. . . . . . . . . 10
β’ (π β (π β β€ β¦ (-1βπ)):β€βΆβ€) |
55 | 54 | frnd 6677 |
. . . . . . . . 9
β’ (π β ran (π β β€ β¦ (-1βπ)) β
β€) |
56 | | eqid 2737 |
. . . . . . . . . 10
β’
((mulGrpββfld) βΎs β€) =
((mulGrpββfld) βΎs
β€) |
57 | 56 | resmhm2b 18634 |
. . . . . . . . 9
β’ ((β€
β (SubMndβ(mulGrpββfld)) β§ ran (π β β€ β¦
(-1βπ)) β
β€) β ((π β
β€ β¦ (-1βπ)) β (β€ring MndHom
(mulGrpββfld)) β (π β β€ β¦ (-1βπ)) β
(β€ring MndHom ((mulGrpββfld)
βΎs β€)))) |
58 | 53, 55, 57 | sylancr 588 |
. . . . . . . 8
β’ (π β ((π β β€ β¦ (-1βπ)) β
(β€ring MndHom (mulGrpββfld)) β
(π β β€ β¦
(-1βπ)) β
(β€ring MndHom ((mulGrpββfld)
βΎs β€)))) |
59 | 50, 58 | mpbii 232 |
. . . . . . 7
β’ (π β (π β β€ β¦ (-1βπ)) β
(β€ring MndHom ((mulGrpββfld)
βΎs β€))) |
60 | | mhmco 18635 |
. . . . . . 7
β’ ((πΏ β
(((mulGrpββfld) βΎs β€) MndHom
πΊ) β§ (π β β€ β¦
(-1βπ)) β
(β€ring MndHom ((mulGrpββfld)
βΎs β€))) β (πΏ β (π β β€ β¦ (-1βπ))) β
(β€ring MndHom πΊ)) |
61 | 33, 59, 60 | syl2anc 585 |
. . . . . 6
β’ (π β (πΏ β (π β β€ β¦ (-1βπ))) β
(β€ring MndHom πΊ)) |
62 | 30, 61 | eqeltrrd 2839 |
. . . . 5
β’ (π β (π β β€ β¦ (πΏβ(-1βπ))) β (β€ring MndHom
πΊ)) |
63 | | lgseisen.2 |
. . . . . . . . . . 11
β’ (π β π β (β β
{2})) |
64 | 63 | gausslemma2dlem0a 26707 |
. . . . . . . . . 10
β’ (π β π β β) |
65 | 64 | nnred 12169 |
. . . . . . . . 9
β’ (π β π β β) |
66 | 6 | gausslemma2dlem0a 26707 |
. . . . . . . . 9
β’ (π β π β β) |
67 | 65, 66 | nndivred 12208 |
. . . . . . . 8
β’ (π β (π / π) β β) |
68 | 67 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π / π) β β) |
69 | | 2nn 12227 |
. . . . . . . . 9
β’ 2 β
β |
70 | | elfznn 13471 |
. . . . . . . . . 10
β’ (π₯ β (1...((π β 1) / 2)) β π₯ β β) |
71 | 70 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π₯ β β) |
72 | | nnmulcl 12178 |
. . . . . . . . 9
β’ ((2
β β β§ π₯
β β) β (2 Β· π₯) β β) |
73 | 69, 71, 72 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β
β) |
74 | 73 | nnred 12169 |
. . . . . . 7
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β
β) |
75 | 68, 74 | remulcld 11186 |
. . . . . 6
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π / π) Β· (2 Β· π₯)) β β) |
76 | 75 | flcld 13704 |
. . . . 5
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(ββ((π / π) Β· (2 Β· π₯))) β
β€) |
77 | | eqid 2737 |
. . . . . 6
β’ (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯)))) = (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯)))) |
78 | | fvexd 6858 |
. . . . . 6
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(ββ((π / π) Β· (2 Β· π₯))) β V) |
79 | | c0ex 11150 |
. . . . . . 7
β’ 0 β
V |
80 | 79 | a1i 11 |
. . . . . 6
β’ (π β 0 β
V) |
81 | 77, 19, 78, 80 | fsuppmptdm 9317 |
. . . . 5
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯)))) finSupp 0) |
82 | | oveq2 7366 |
. . . . . 6
β’ (π = (ββ((π / π) Β· (2 Β· π₯))) β (-1βπ) = (-1β(ββ((π / π) Β· (2 Β· π₯))))) |
83 | 82 | fveq2d 6847 |
. . . . 5
β’ (π = (ββ((π / π) Β· (2 Β· π₯))) β (πΏβ(-1βπ)) = (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))) |
84 | | oveq2 7366 |
. . . . . 6
β’ (π = (β€ring
Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯))))) β (-1βπ) =
(-1β(β€ring Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯))))))) |
85 | 84 | fveq2d 6847 |
. . . . 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 19717 |
. . . 4
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯))))))) = (πΏβ(-1β(β€ring
Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯)))))))) |
87 | 14, 25 | mgpbas 19903 |
. . . . . . 7
β’
(Baseβπ) =
(BaseβπΊ) |
88 | | eqid 2737 |
. . . . . . . 8
β’
(.rβπ) = (.rβπ) |
89 | 14, 88 | mgpplusg 19901 |
. . . . . . 7
β’
(.rβπ) = (+gβπΊ) |
90 | 27 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β πΏ:β€βΆ(Baseβπ)) |
91 | | m1expcl 13993 |
. . . . . . . . 9
β’
((ββ((π
/ π) Β· (2 Β·
π₯))) β β€ β
(-1β(ββ((π
/ π) Β· (2 Β·
π₯)))) β
β€) |
92 | 76, 91 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(-1β(ββ((π
/ π) Β· (2 Β·
π₯)))) β
β€) |
93 | 90, 92 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯))))) β (Baseβπ)) |
94 | | neg1z 12540 |
. . . . . . . . . 10
β’ -1 β
β€ |
95 | | lgseisen.4 |
. . . . . . . . . . 11
β’ π
= ((π Β· (2 Β· π₯)) mod π) |
96 | 63 | eldifad 3923 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
98 | | prmz 16552 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β€) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β€) |
100 | 73 | nnzd 12527 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β
β€) |
101 | 99, 100 | zmulcld 12614 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (2 Β· π₯)) β β€) |
102 | 7 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
103 | | prmnn 16551 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
105 | 101, 104 | zmodcld 13798 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (2 Β· π₯)) mod π) β
β0) |
106 | 95, 105 | eqeltrid 2842 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π
β
β0) |
107 | | zexpcl 13983 |
. . . . . . . . . 10
β’ ((-1
β β€ β§ π
β β0) β (-1βπ
) β β€) |
108 | 94, 106, 107 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1βπ
) β
β€) |
109 | 108, 99 | zmulcld 12614 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((-1βπ
) Β· π) β β€) |
110 | 90, 109 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ((-1βπ
) Β· π)) β (Baseβπ)) |
111 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))) |
112 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) |
113 | 87, 89, 16, 19, 93, 110, 111, 112 | gsummptfidmadd2 19704 |
. . . . . 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 2738 |
. . . . . . . . 9
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯))))))) |
115 | | eqidd 2738 |
. . . . . . . . 9
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π)))) |
116 | 19, 93, 110, 114, 115 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))) βf
(.rβπ)(π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π)))) = (π₯ β (1...((π β 1) / 2)) β¦ ((πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))(.rβπ)(πΏβ((-1βπ
) Β· π))))) |
117 | 24 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β πΏ β (β€ring RingHom
π)) |
118 | | zringmulr 20881 |
. . . . . . . . . . . 12
β’ Β·
= (.rββ€ring) |
119 | 1, 118, 88 | rhmmul 20160 |
. . . . . . . . . . 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 12608 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (2 Β· π₯)) β β) |
122 | 104 | nnrpd 12956 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β
β+) |
123 | | modval 13777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π Β· (2 Β· π₯)) β β β§ π β β+)
β ((π Β· (2
Β· π₯)) mod π) = ((π Β· (2 Β· π₯)) β (π Β· (ββ((π Β· (2 Β· π₯)) / π))))) |
124 | 121, 122,
123 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (2 Β· π₯)) mod π) = ((π Β· (2 Β· π₯)) β (π Β· (ββ((π Β· (2 Β· π₯)) / π))))) |
125 | 95, 124 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π
= ((π Β· (2 Β· π₯)) β (π Β· (ββ((π Β· (2 Β· π₯)) / π))))) |
126 | 99 | zcnd 12609 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
127 | 73 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β
β) |
128 | 104 | nncnd 12170 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
129 | 104 | nnne0d 12204 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β 0) |
130 | 126, 127,
128, 129 | div23d 11969 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (2 Β· π₯)) / π) = ((π / π) Β· (2 Β· π₯))) |
131 | 130 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(ββ((π Β·
(2 Β· π₯)) / π)) = (ββ((π / π) Β· (2 Β· π₯)))) |
132 | 131 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (ββ((π Β· (2 Β· π₯)) / π))) = (π Β· (ββ((π / π) Β· (2 Β· π₯))))) |
133 | 132 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (2 Β· π₯)) β (π Β· (ββ((π Β· (2 Β· π₯)) / π)))) = ((π Β· (2 Β· π₯)) β (π Β· (ββ((π / π) Β· (2 Β· π₯)))))) |
134 | 125, 133 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π
= ((π Β· (2 Β· π₯)) β (π Β· (ββ((π / π) Β· (2 Β· π₯)))))) |
135 | 134 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (ββ((π / π) Β· (2 Β· π₯)))) + π
) = ((π Β· (ββ((π / π) Β· (2 Β· π₯)))) + ((π Β· (2 Β· π₯)) β (π Β· (ββ((π / π) Β· (2 Β· π₯))))))) |
136 | | prmz 16552 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β€) |
137 | 102, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β€) |
138 | 137, 76 | zmulcld 12614 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (ββ((π / π) Β· (2 Β· π₯)))) β β€) |
139 | 138 | zcnd 12609 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (ββ((π / π) Β· (2 Β· π₯)))) β β) |
140 | 101 | zcnd 12609 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (2 Β· π₯)) β β) |
141 | 139, 140 | pncan3d 11516 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (ββ((π / π) Β· (2 Β· π₯)))) + ((π Β· (2 Β· π₯)) β (π Β· (ββ((π / π) Β· (2 Β· π₯)))))) = (π Β· (2 Β· π₯))) |
142 | | 2cnd 12232 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β 2 β
β) |
143 | 71 | nncnd 12170 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π₯ β β) |
144 | 126, 142,
143 | mul12d 11365 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (2 Β· π₯)) = (2 Β· (π Β· π₯))) |
145 | 135, 141,
144 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (ββ((π / π) Β· (2 Β· π₯)))) + π
) = (2 Β· (π Β· π₯))) |
146 | 145 | oveq2d 7374 |
. . . . . . . . . . . . . 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 12526 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π
β β€) |
150 | | expaddz 14013 |
. . . . . . . . . . . . . . . 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 14015 |
. . . . . . . . . . . . . . . . . 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 11151 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β 1 β
β) |
155 | | eldifsni 4751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (β β {2})
β π β
2) |
156 | 6, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β 2) |
157 | 156 | necomd 3000 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 2 β π) |
158 | 157 | neneqd 2949 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Β¬ 2 = π) |
159 | 158 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β Β¬ 2 = π) |
160 | | 2z 12536 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 2 β
β€ |
161 | | uzid 12779 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (2 β
β€ β 2 β (β€β₯β2)) |
162 | 160, 161 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
(β€β₯β2) |
163 | | dvdsprm 16580 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((2
β (β€β₯β2) β§ π β β) β (2 β₯ π β 2 = π)) |
164 | 162, 102,
163 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 β₯ π β 2 = π)) |
165 | 159, 164 | mtbird 325 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β Β¬ 2 β₯
π) |
166 | | oexpneg 16228 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((1
β β β§ π
β β β§ Β¬ 2 β₯ π) β (-1βπ) = -(1βπ)) |
167 | 154, 104,
165, 166 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1βπ) = -(1βπ)) |
168 | | 1exp 13998 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β€ β
(1βπ) =
1) |
169 | 137, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (1βπ) = 1) |
170 | 169 | negeqd 11396 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β -(1βπ) = -1) |
171 | 167, 170 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1βπ) = -1) |
172 | 171 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((-1βπ)β(ββ((π / π) Β· (2 Β· π₯)))) = (-1β(ββ((π / π) Β· (2 Β· π₯))))) |
173 | 153, 172 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1β(π Β· (ββ((π / π) Β· (2 Β· π₯))))) = (-1β(ββ((π / π) Β· (2 Β· π₯))))) |
174 | 173 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((-1β(π Β· (ββ((π / π) Β· (2 Β· π₯))))) Β· (-1βπ
)) = ((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· (-1βπ
))) |
175 | 151, 174 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1β((π Β· (ββ((π / π) Β· (2 Β· π₯)))) + π
)) = ((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· (-1βπ
))) |
176 | | nnmulcl 12178 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
177 | 64, 70, 176 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· π₯) β β) |
178 | 177 | nnnn0d 12474 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· π₯) β
β0) |
179 | | 2nn0 12431 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β0 |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β 2 β
β0) |
181 | 147, 178,
180 | expmuld 14055 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1β(2
Β· (π Β· π₯))) = ((-1β2)β(π Β· π₯))) |
182 | | neg1sqe1 14101 |
. . . . . . . . . . . . . . . . 17
β’
(-1β2) = 1 |
183 | 182 | oveq1i 7368 |
. . . . . . . . . . . . . . . 16
β’
((-1β2)β(π
Β· π₯)) =
(1β(π Β· π₯)) |
184 | 177 | nnzd 12527 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· π₯) β β€) |
185 | | 1exp 13998 |
. . . . . . . . . . . . . . . . 17
β’ ((π Β· π₯) β β€ β (1β(π Β· π₯)) = 1) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (1β(π Β· π₯)) = 1) |
187 | 183, 186 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
((-1β2)β(π
Β· π₯)) =
1) |
188 | 181, 187 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1β(2
Β· (π Β· π₯))) = 1) |
189 | 146, 175,
188 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· (-1βπ
)) = 1) |
190 | 189 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· (-1βπ
)) Β· π) = (1 Β· π)) |
191 | 92 | zcnd 12609 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(-1β(ββ((π
/ π) Β· (2 Β·
π₯)))) β
β) |
192 | 108 | zcnd 12609 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1βπ
) β
β) |
193 | 191, 192,
126 | mulassd 11179 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· (-1βπ
)) Β· π) = ((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· ((-1βπ
) Β· π))) |
194 | 126 | mulid2d 11174 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (1 Β· π) = π) |
195 | 190, 193,
194 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· ((-1βπ
) Β· π)) = π) |
196 | 195 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ((-1β(ββ((π / π) Β· (2 Β· π₯)))) Β· ((-1βπ
) Β· π))) = (πΏβπ)) |
197 | 120, 196 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))(.rβπ)(πΏβ((-1βπ
) Β· π))) = (πΏβπ)) |
198 | 197 | mpteq2dva 5206 |
. . . . . . . 8
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ ((πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))(.rβπ)(πΏβ((-1βπ
) Β· π)))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβπ))) |
199 | 116, 198 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))) βf
(.rβπ)(π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π)))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβπ))) |
200 | 199 | oveq2d 7374 |
. . . . . 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 26728 |
. . . . . . 7
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π)))) = (1rβπ)) |
205 | 204 | oveq2d 7374 |
. . . . . 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 2786 |
. . . . 5
β’ (π β ((πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))))(.rβπ)(1rβπ)) = (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβπ)))) |
207 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
208 | 93 | fmpttd 7064 |
. . . . . . 7
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))):(1...((π β 1) / 2))βΆ(Baseβπ)) |
209 | | fvexd 6858 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯))))) β V) |
210 | | fvexd 6858 |
. . . . . . . 8
β’ (π β (0gβπΊ) β V) |
211 | 111, 19, 209, 210 | fsuppmptdm 9317 |
. . . . . . 7
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯)))))) finSupp (0gβπΊ)) |
212 | 87, 207, 16, 19, 208, 211 | gsumcl 19693 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯))))))) β (Baseβπ)) |
213 | | eqid 2737 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
214 | 25, 88, 213 | ringridm 19994 |
. . . . . 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 585 |
. . . . 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 7037 |
. . . . . . 7
β’ (π β (πΏβπ) β (Baseβπ)) |
218 | | eqid 2737 |
. . . . . . . 8
β’
(.gβπΊ) = (.gβπΊ) |
219 | 87, 218 | gsumconst 19712 |
. . . . . . 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 16683 |
. . . . . . . . . 10
β’ (π β (β β {2})
β ((π β 1) / 2)
β β) |
222 | 6, 221 | syl 17 |
. . . . . . . . 9
β’ (π β ((π β 1) / 2) β
β) |
223 | 222 | nnnn0d 12474 |
. . . . . . . 8
β’ (π β ((π β 1) / 2) β
β0) |
224 | | hashfz1 14247 |
. . . . . . . 8
β’ (((π β 1) / 2) β
β0 β (β―β(1...((π β 1) / 2))) = ((π β 1) / 2)) |
225 | 223, 224 | syl 17 |
. . . . . . 7
β’ (π β
(β―β(1...((π
β 1) / 2))) = ((π
β 1) / 2)) |
226 | 225 | oveq1d 7373 |
. . . . . 6
β’ (π β
((β―β(1...((π
β 1) / 2)))(.gβπΊ)(πΏβπ)) = (((π β 1) / 2)(.gβπΊ)(πΏβπ))) |
227 | 31, 1 | mgpbas 19903 |
. . . . . . . . 9
β’ β€ =
(Baseβ((mulGrpββfld) βΎs
β€)) |
228 | | eqid 2737 |
. . . . . . . . 9
β’
(.gβ((mulGrpββfld)
βΎs β€)) =
(.gβ((mulGrpββfld) βΎs
β€)) |
229 | 227, 228,
218 | mhmmulg 18918 |
. . . . . . . 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 2737 |
. . . . . . . . . . 11
β’
(.gβ(mulGrpββfld)) =
(.gβ(mulGrpββfld)) |
233 | 232, 56, 228 | submmulg 18921 |
. . . . . . . . . 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 12609 |
. . . . . . . . . 10
β’ (π β π β β) |
236 | | cnfldexp 20833 |
. . . . . . . . . 10
β’ ((π β β β§ ((π β 1) / 2) β
β0) β (((π β 1) /
2)(.gβ(mulGrpββfld))π) = (πβ((π β 1) / 2))) |
237 | 235, 223,
236 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (((π β 1) /
2)(.gβ(mulGrpββfld))π) = (πβ((π β 1) / 2))) |
238 | 234, 237 | eqtr3d 2779 |
. . . . . . . 8
β’ (π β (((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π) = (πβ((π β 1) / 2))) |
239 | 238 | fveq2d 6847 |
. . . . . . 7
β’ (π β (πΏβ(((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π)) = (πΏβ(πβ((π β 1) / 2)))) |
240 | 230, 239 | eqtr3d 2779 |
. . . . . 6
β’ (π β (((π β 1) / 2)(.gβπΊ)(πΏβπ)) = (πΏβ(πβ((π β 1) / 2)))) |
241 | 220, 226,
240 | 3eqtrd 2781 |
. . . . 5
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβπ))) = (πΏβ(πβ((π β 1) / 2)))) |
242 | 206, 215,
241 | 3eqtr3d 2785 |
. . . 4
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(-1β(ββ((π / π) Β· (2 Β· π₯))))))) = (πΏβ(πβ((π β 1) / 2)))) |
243 | | subrgsubg 20231 |
. . . . . . . . . 10
β’ (β€
β (SubRingββfld) β β€ β
(SubGrpββfld)) |
244 | 51, 243 | ax-mp 5 |
. . . . . . . . 9
β’ β€
β (SubGrpββfld) |
245 | | subgsubm 18951 |
. . . . . . . . 9
β’ (β€
β (SubGrpββfld) β β€ β
(SubMndββfld)) |
246 | 244, 245 | mp1i 13 |
. . . . . . . 8
β’ (π β β€ β
(SubMndββfld)) |
247 | 76 | fmpttd 7064 |
. . . . . . . 8
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯)))):(1...((π β 1) /
2))βΆβ€) |
248 | | df-zring 20873 |
. . . . . . . 8
β’
β€ring = (βfld βΎs
β€) |
249 | 19, 246, 247, 248 | gsumsubm 18646 |
. . . . . . 7
β’ (π β (βfld
Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯))))) = (β€ring
Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯)))))) |
250 | 76 | zcnd 12609 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β
(ββ((π / π) Β· (2 Β· π₯))) β
β) |
251 | 19, 250 | gsumfsum 20867 |
. . . . . . 7
β’ (π β (βfld
Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯))))) = Ξ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯)))) |
252 | 249, 251 | eqtr3d 2779 |
. . . . . 6
β’ (π β (β€ring
Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯))))) = Ξ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯)))) |
253 | 252 | oveq2d 7374 |
. . . . 5
β’ (π β
(-1β(β€ring Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯)))))) = (-1βΞ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯))))) |
254 | 253 | fveq2d 6847 |
. . . 4
β’ (π β (πΏβ(-1β(β€ring
Ξ£g (π₯ β (1...((π β 1) / 2)) β¦
(ββ((π / π) Β· (2 Β· π₯))))))) = (πΏβ(-1βΞ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯)))))) |
255 | 86, 242, 254 | 3eqtr3d 2785 |
. . 3
β’ (π β (πΏβ(πβ((π β 1) / 2))) = (πΏβ(-1βΞ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯)))))) |
256 | 66 | nnnn0d 12474 |
. . . 4
β’ (π β π β
β0) |
257 | | zexpcl 13983 |
. . . . 5
β’ ((π β β€ β§ ((π β 1) / 2) β
β0) β (πβ((π β 1) / 2)) β
β€) |
258 | 216, 223,
257 | syl2anc 585 |
. . . 4
β’ (π β (πβ((π β 1) / 2)) β
β€) |
259 | 19, 76 | fsumzcl 15621 |
. . . . 5
β’ (π β Ξ£π₯ β (1...((π β 1) / 2))(ββ((π / π) Β· (2 Β· π₯))) β β€) |
260 | | m1expcl 13993 |
. . . . 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 20959 |
. . . 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 231 |
. 2
β’ (π β π β₯ ((πβ((π β 1) / 2)) β
(-1βΞ£π₯ β
(1...((π β 1) /
2))(ββ((π /
π) Β· (2 Β·
π₯)))))) |
265 | | moddvds 16148 |
. . 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 π)) |