Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = π₯ β (2 Β· π) = (2 Β· π₯)) |
2 | 1 | fveq2d 6847 |
. . . . . . . 8
β’ (π = π₯ β (πΏβ(2 Β· π)) = (πΏβ(2 Β· π₯))) |
3 | 2 | cbvmptv 5219 |
. . . . . . 7
β’ (π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))) |
4 | 3 | oveq2i 7369 |
. . . . . 6
β’ (πΊ Ξ£g
(π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π)))) = (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))) |
5 | | lgseisen.8 |
. . . . . . . 8
β’ πΊ = (mulGrpβπ) |
6 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
7 | 5, 6 | mgpbas 19903 |
. . . . . . 7
β’
(Baseβπ) =
(BaseβπΊ) |
8 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
9 | | lgseisen.1 |
. . . . . . . . . . 11
β’ (π β π β (β β
{2})) |
10 | 9 | eldifad 3923 |
. . . . . . . . . 10
β’ (π β π β β) |
11 | | lgseisen.7 |
. . . . . . . . . . 11
β’ π =
(β€/nβ€βπ) |
12 | 11 | znfld 20970 |
. . . . . . . . . 10
β’ (π β β β π β Field) |
13 | 10, 12 | syl 17 |
. . . . . . . . 9
β’ (π β π β Field) |
14 | | isfld 20197 |
. . . . . . . . . 10
β’ (π β Field β (π β DivRing β§ π β CRing)) |
15 | 14 | simprbi 498 |
. . . . . . . . 9
β’ (π β Field β π β CRing) |
16 | 13, 15 | syl 17 |
. . . . . . . 8
β’ (π β π β CRing) |
17 | 5 | crngmgp 19973 |
. . . . . . . 8
β’ (π β CRing β πΊ β CMnd) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ (π β πΊ β CMnd) |
19 | | fzfid 13879 |
. . . . . . 7
β’ (π β (1...((π β 1) / 2)) β
Fin) |
20 | | crngring 19977 |
. . . . . . . . . . . 12
β’ (π β CRing β π β Ring) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β Ring) |
22 | | lgseisen.9 |
. . . . . . . . . . . 12
β’ πΏ = (β€RHomβπ) |
23 | 22 | zrhrhm 20915 |
. . . . . . . . . . 11
β’ (π β Ring β πΏ β (β€ring
RingHom π)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . 10
β’ (π β πΏ β (β€ring RingHom
π)) |
25 | | zringbas 20878 |
. . . . . . . . . . 11
β’ β€ =
(Baseββ€ring) |
26 | 25, 6 | rhmf 20159 |
. . . . . . . . . 10
β’ (πΏ β (β€ring
RingHom π) β πΏ:β€βΆ(Baseβπ)) |
27 | 24, 26 | syl 17 |
. . . . . . . . 9
β’ (π β πΏ:β€βΆ(Baseβπ)) |
28 | | 2z 12536 |
. . . . . . . . . 10
β’ 2 β
β€ |
29 | | elfzelz 13442 |
. . . . . . . . . 10
β’ (π β (1...((π β 1) / 2)) β π β β€) |
30 | | zmulcl 12553 |
. . . . . . . . . 10
β’ ((2
β β€ β§ π
β β€) β (2 Β· π) β β€) |
31 | 28, 29, 30 | sylancr 588 |
. . . . . . . . 9
β’ (π β (1...((π β 1) / 2)) β (2 Β· π) β
β€) |
32 | | ffvelcdm 7033 |
. . . . . . . . 9
β’ ((πΏ:β€βΆ(Baseβπ) β§ (2 Β· π) β β€) β (πΏβ(2 Β· π)) β (Baseβπ)) |
33 | 27, 31, 32 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β (1...((π β 1) / 2))) β (πΏβ(2 Β· π)) β (Baseβπ)) |
34 | 33 | fmpttd 7064 |
. . . . . . 7
β’ (π β (π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))):(1...((π β 1) / 2))βΆ(Baseβπ)) |
35 | | eqid 2737 |
. . . . . . . 8
β’ (π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) = (π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) |
36 | | fvexd 6858 |
. . . . . . . 8
β’ ((π β§ π β (1...((π β 1) / 2))) β (πΏβ(2 Β· π)) β V) |
37 | | fvexd 6858 |
. . . . . . . 8
β’ (π β (0gβπΊ) β V) |
38 | 35, 19, 36, 37 | fsuppmptdm 9317 |
. . . . . . 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 26727 |
. . . . . . 7
β’ (π β π:(1...((π β 1) / 2))β1-1-ontoβ(1...((π β 1) / 2))) |
45 | 7, 8, 18, 19, 34, 38, 44 | gsumf1o 19694 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π)))) = (πΊ Ξ£g ((π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) β π))) |
46 | 4, 45 | eqtr3id 2791 |
. . . . 5
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))) = (πΊ Ξ£g ((π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) β π))) |
47 | 9, 39, 40, 41, 42 | lgseisenlem1 26726 |
. . . . . . . 8
β’ (π β π:(1...((π β 1) / 2))βΆ(1...((π β 1) /
2))) |
48 | 42 | fmpt 7059 |
. . . . . . . 8
β’
(βπ₯ β
(1...((π β 1) /
2))((((-1βπ
) Β·
π
) mod π) / 2) β (1...((π β 1) / 2)) β π:(1...((π β 1) / 2))βΆ(1...((π β 1) /
2))) |
49 | 47, 48 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β (1...((π β 1) / 2))((((-1βπ
) Β· π
) mod π) / 2) β (1...((π β 1) / 2))) |
50 | 42 | a1i 11 |
. . . . . . 7
β’ (π β π = (π₯ β (1...((π β 1) / 2)) β¦ ((((-1βπ
) Β· π
) mod π) / 2))) |
51 | | eqidd 2738 |
. . . . . . 7
β’ (π β (π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) = (π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π)))) |
52 | | oveq2 7366 |
. . . . . . . 8
β’ (π = ((((-1βπ
) Β· π
) mod π) / 2) β (2 Β· π) = (2 Β· ((((-1βπ
) Β· π
) mod π) / 2))) |
53 | 52 | fveq2d 6847 |
. . . . . . 7
β’ (π = ((((-1βπ
) Β· π
) mod π) / 2) β (πΏβ(2 Β· π)) = (πΏβ(2 Β· ((((-1βπ
) Β· π
) mod π) / 2)))) |
54 | 49, 50, 51, 53 | fmptcof 7077 |
. . . . . 6
β’ (π β ((π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) β π) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· ((((-1βπ
) Β· π
) mod π) / 2))))) |
55 | 54 | oveq2d 7374 |
. . . . 5
β’ (π β (πΊ Ξ£g ((π β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π))) β π)) = (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· ((((-1βπ
) Β· π
) mod π) / 2)))))) |
56 | 39 | eldifad 3923 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
58 | | prmz 16552 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β€) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β€) |
60 | | 2nn 12227 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β
β |
61 | | elfznn 13471 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (1...((π β 1) / 2)) β π₯ β β) |
62 | 61 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π₯ β β) |
63 | | nnmulcl 12178 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((2
β β β§ π₯
β β) β (2 Β· π₯) β β) |
64 | 60, 62, 63 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β
β) |
65 | 64 | nnzd 12527 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β
β€) |
66 | 59, 65 | zmulcld 12614 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (2 Β· π₯)) β β€) |
67 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
68 | | prmnn 16551 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
70 | 66, 69 | zmodcld 13798 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((π Β· (2 Β· π₯)) mod π) β
β0) |
71 | 41, 70 | eqeltrid 2842 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π
β
β0) |
72 | 71 | nn0zd 12526 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π
β β€) |
73 | | m1expcl 13993 |
. . . . . . . . . . . . . . 15
β’ (π
β β€ β
(-1βπ
) β
β€) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1βπ
) β
β€) |
75 | 74, 72 | zmulcld 12614 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((-1βπ
) Β· π
) β β€) |
76 | 75, 69 | zmodcld 13798 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((-1βπ
) Β· π
) mod π) β
β0) |
77 | 76 | nn0cnd 12476 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((-1βπ
) Β· π
) mod π) β β) |
78 | | 2cnd 12232 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β 2 β
β) |
79 | | 2ne0 12258 |
. . . . . . . . . . . 12
β’ 2 β
0 |
80 | 79 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β 2 β
0) |
81 | 77, 78, 80 | divcan2d 11934 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β·
((((-1βπ
) Β·
π
) mod π) / 2)) = (((-1βπ
) Β· π
) mod π)) |
82 | 81 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(2 Β· ((((-1βπ
) Β· π
) mod π) / 2))) = (πΏβ(((-1βπ
) Β· π
) mod π))) |
83 | 69 | nnrpd 12956 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β
β+) |
84 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((-1βπ
) mod π) = ((-1βπ
) mod π)) |
85 | 41 | oveq1i 7368 |
. . . . . . . . . . . . . 14
β’ (π
mod π) = (((π Β· (2 Β· π₯)) mod π) mod π) |
86 | 66 | zred 12608 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π Β· (2 Β· π₯)) β β) |
87 | | modabs2 13811 |
. . . . . . . . . . . . . . 15
β’ (((π Β· (2 Β· π₯)) β β β§ π β β+)
β (((π Β· (2
Β· π₯)) mod π) mod π) = ((π Β· (2 Β· π₯)) mod π)) |
88 | 86, 83, 87 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((π Β· (2 Β· π₯)) mod π) mod π) = ((π Β· (2 Β· π₯)) mod π)) |
89 | 85, 88 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π
mod π) = ((π Β· (2 Β· π₯)) mod π)) |
90 | 74, 74, 72, 66, 83, 84, 89 | modmul12d 13831 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((-1βπ
) Β· π
) mod π) = (((-1βπ
) Β· (π Β· (2 Β· π₯))) mod π)) |
91 | 75 | zred 12608 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((-1βπ
) Β· π
) β β) |
92 | | modabs2 13811 |
. . . . . . . . . . . . 13
β’
((((-1βπ
)
Β· π
) β β
β§ π β
β+) β ((((-1βπ
) Β· π
) mod π) mod π) = (((-1βπ
) Β· π
) mod π)) |
93 | 91, 83, 92 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((((-1βπ
) Β· π
) mod π) mod π) = (((-1βπ
) Β· π
) mod π)) |
94 | 74 | zcnd 12609 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (-1βπ
) β
β) |
95 | 59 | zcnd 12609 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
96 | 65 | zcnd 12609 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β
β) |
97 | 94, 95, 96 | mulassd 11179 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((-1βπ
) Β· π) Β· (2 Β· π₯)) = ((-1βπ
) Β· (π Β· (2 Β· π₯)))) |
98 | 97 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((((-1βπ
) Β· π) Β· (2 Β· π₯)) mod π) = (((-1βπ
) Β· (π Β· (2 Β· π₯))) mod π)) |
99 | 90, 93, 98 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((((-1βπ
) Β· π
) mod π) mod π) = ((((-1βπ
) Β· π) Β· (2 Β· π₯)) mod π)) |
100 | 10, 68 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
101 | 100 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β) |
102 | 76 | nn0zd 12526 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((-1βπ
) Β· π
) mod π) β β€) |
103 | 74, 59 | zmulcld 12614 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((-1βπ
) Β· π) β β€) |
104 | 103, 65 | zmulcld 12614 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((-1βπ
) Β· π) Β· (2 Β· π₯)) β β€) |
105 | | moddvds 16148 |
. . . . . . . . . . . 12
β’ ((π β β β§
(((-1βπ
) Β·
π
) mod π) β β€ β§ (((-1βπ
) Β· π) Β· (2 Β· π₯)) β β€) β (((((-1βπ
) Β· π
) mod π) mod π) = ((((-1βπ
) Β· π) Β· (2 Β· π₯)) mod π) β π β₯ ((((-1βπ
) Β· π
) mod π) β (((-1βπ
) Β· π) Β· (2 Β· π₯))))) |
106 | 101, 102,
104, 105 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (((((-1βπ
) Β· π
) mod π) mod π) = ((((-1βπ
) Β· π) Β· (2 Β· π₯)) mod π) β π β₯ ((((-1βπ
) Β· π
) mod π) β (((-1βπ
) Β· π) Β· (2 Β· π₯))))) |
107 | 99, 106 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β₯ ((((-1βπ
) Β· π
) mod π) β (((-1βπ
) Β· π) Β· (2 Β· π₯)))) |
108 | 69 | nnnn0d 12474 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β
β0) |
109 | 11, 22 | zndvds 20959 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (((-1βπ
)
Β· π
) mod π) β β€ β§
(((-1βπ
) Β·
π) Β· (2 Β·
π₯)) β β€) β
((πΏβ(((-1βπ
) Β· π
) mod π)) = (πΏβ(((-1βπ
) Β· π) Β· (2 Β· π₯))) β π β₯ ((((-1βπ
) Β· π
) mod π) β (((-1βπ
) Β· π) Β· (2 Β· π₯))))) |
110 | 108, 102,
104, 109 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((πΏβ(((-1βπ
) Β· π
) mod π)) = (πΏβ(((-1βπ
) Β· π) Β· (2 Β· π₯))) β π β₯ ((((-1βπ
) Β· π
) mod π) β (((-1βπ
) Β· π) Β· (2 Β· π₯))))) |
111 | 107, 110 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(((-1βπ
) Β· π
) mod π)) = (πΏβ(((-1βπ
) Β· π) Β· (2 Β· π₯)))) |
112 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β πΏ β (β€ring RingHom
π)) |
113 | | zringmulr 20881 |
. . . . . . . . . . 11
β’ Β·
= (.rββ€ring) |
114 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.rβπ) = (.rβπ) |
115 | 25, 113, 114 | rhmmul 20160 |
. . . . . . . . . 10
β’ ((πΏ β (β€ring
RingHom π) β§
((-1βπ
) Β· π) β β€ β§ (2
Β· π₯) β β€)
β (πΏβ(((-1βπ
) Β· π) Β· (2 Β· π₯))) = ((πΏβ((-1βπ
) Β· π))(.rβπ)(πΏβ(2 Β· π₯)))) |
116 | 112, 103,
65, 115 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(((-1βπ
) Β· π) Β· (2 Β· π₯))) = ((πΏβ((-1βπ
) Β· π))(.rβπ)(πΏβ(2 Β· π₯)))) |
117 | 82, 111, 116 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(2 Β· ((((-1βπ
) Β· π
) mod π) / 2))) = ((πΏβ((-1βπ
) Β· π))(.rβπ)(πΏβ(2 Β· π₯)))) |
118 | 117 | mpteq2dva 5206 |
. . . . . . 7
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· ((((-1βπ
) Β· π
) mod π) / 2)))) = (π₯ β (1...((π β 1) / 2)) β¦ ((πΏβ((-1βπ
) Β· π))(.rβπ)(πΏβ(2 Β· π₯))))) |
119 | 27 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β πΏ:β€βΆ(Baseβπ)) |
120 | 119, 103 | ffvelcdmd 7037 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ((-1βπ
) Β· π)) β (Baseβπ)) |
121 | 119, 65 | ffvelcdmd 7037 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(2 Β· π₯)) β (Baseβπ)) |
122 | | eqidd 2738 |
. . . . . . . 8
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π)))) |
123 | | eqidd 2738 |
. . . . . . . 8
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))) |
124 | 19, 120, 121, 122, 123 | offval2 7638 |
. . . . . . 7
β’ (π β ((π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) βf
(.rβπ)(π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))) = (π₯ β (1...((π β 1) / 2)) β¦ ((πΏβ((-1βπ
) Β· π))(.rβπ)(πΏβ(2 Β· π₯))))) |
125 | 118, 124 | eqtr4d 2780 |
. . . . . 6
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· ((((-1βπ
) Β· π
) mod π) / 2)))) = ((π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) βf
(.rβπ)(π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))))) |
126 | 125 | oveq2d 7374 |
. . . . 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 2781 |
. . . 4
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))) = (πΊ Ξ£g ((π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) βf
(.rβπ)(π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))))) |
128 | 5, 114 | mgpplusg 19901 |
. . . . 5
β’
(.rβπ) = (+gβπΊ) |
129 | | eqid 2737 |
. . . . 5
β’ (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) |
130 | | eqid 2737 |
. . . . 5
β’ (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))) = (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))) |
131 | 7, 128, 18, 19, 120, 121, 129, 130 | gsummptfidmadd2 19704 |
. . . 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 2777 |
. . 3
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))) = ((πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))))(.rβπ)(πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))))) |
133 | 132 | oveq1d 7373 |
. 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 2737 |
. . . . . 6
β’
(Unitβπ) =
(Unitβπ) |
135 | 134, 5 | unitsubm 20100 |
. . . . 5
β’ (π β Ring β
(Unitβπ) β
(SubMndβπΊ)) |
136 | 21, 135 | syl 17 |
. . . 4
β’ (π β (Unitβπ) β (SubMndβπΊ)) |
137 | | elfzle2 13446 |
. . . . . . . . . . 11
β’ (π₯ β (1...((π β 1) / 2)) β π₯ β€ ((π β 1) / 2)) |
138 | 137 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π₯ β€ ((π β 1) / 2)) |
139 | 62 | nnred 12169 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π₯ β β) |
140 | | prmuz2 16573 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β2)) |
141 | | uz2m1nn 12849 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β2) β (π β 1) β β) |
142 | 67, 140, 141 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π β 1) β β) |
143 | 142 | nnred 12169 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π β 1) β β) |
144 | | 2re 12228 |
. . . . . . . . . . . 12
β’ 2 β
β |
145 | 144 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β 2 β
β) |
146 | | 2pos 12257 |
. . . . . . . . . . . 12
β’ 0 <
2 |
147 | 146 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β 0 <
2) |
148 | | lemuldiv2 12037 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ (π β 1) β β β§
(2 β β β§ 0 < 2)) β ((2 Β· π₯) β€ (π β 1) β π₯ β€ ((π β 1) / 2))) |
149 | 139, 143,
145, 147, 148 | syl112anc 1375 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((2 Β· π₯) β€ (π β 1) β π₯ β€ ((π β 1) / 2))) |
150 | 138, 149 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β€ (π β 1)) |
151 | | prmz 16552 |
. . . . . . . . . . . 12
β’ (π β β β π β
β€) |
152 | 67, 151 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β β€) |
153 | | peano2zm 12547 |
. . . . . . . . . . 11
β’ (π β β€ β (π β 1) β
β€) |
154 | 152, 153 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (π β 1) β β€) |
155 | | fznn 13510 |
. . . . . . . . . 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 712 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (2 Β· π₯) β (1...(π β 1))) |
158 | | fzm1ndvds 16205 |
. . . . . . . 8
β’ ((π β β β§ (2
Β· π₯) β
(1...(π β 1))) β
Β¬ π β₯ (2 Β·
π₯)) |
159 | 69, 157, 158 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β Β¬ π β₯ (2 Β· π₯)) |
160 | | eqid 2737 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
161 | 11, 22, 160 | zndvds0 20960 |
. . . . . . . . 9
β’ ((π β β0
β§ (2 Β· π₯) β
β€) β ((πΏβ(2 Β· π₯)) = (0gβπ) β π β₯ (2 Β· π₯))) |
162 | 108, 65, 161 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((πΏβ(2 Β· π₯)) = (0gβπ) β π β₯ (2 Β· π₯))) |
163 | 162 | necon3abid 2981 |
. . . . . . 7
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β ((πΏβ(2 Β· π₯)) β
(0gβπ)
β Β¬ π β₯ (2
Β· π₯))) |
164 | 159, 163 | mpbird 257 |
. . . . . 6
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(2 Β· π₯)) β (0gβπ)) |
165 | 14 | simplbi 499 |
. . . . . . . . 9
β’ (π β Field β π β
DivRing) |
166 | 13, 165 | syl 17 |
. . . . . . . 8
β’ (π β π β DivRing) |
167 | 166 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β π β DivRing) |
168 | 6, 134, 160 | drngunit 20191 |
. . . . . . 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 712 |
. . . . 5
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(2 Β· π₯)) β (Unitβπ)) |
171 | 170 | fmpttd 7064 |
. . . 4
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))):(1...((π β 1) / 2))βΆ(Unitβπ)) |
172 | | fvexd 6858 |
. . . . 5
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ(2 Β· π₯)) β V) |
173 | 130, 19, 172, 37 | fsuppmptdm 9317 |
. . . 4
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))) finSupp (0gβπΊ)) |
174 | 8, 18, 19, 136, 171, 173 | gsumsubmcl 19697 |
. . 3
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯)))) β (Unitβπ)) |
175 | | eqid 2737 |
. . . 4
β’
(/rβπ) = (/rβπ) |
176 | | eqid 2737 |
. . . 4
β’
(1rβπ) = (1rβπ) |
177 | 134, 175,
176 | dvrid 20118 |
. . 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 585 |
. 2
β’ (π β ((πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))))(/rβπ)(πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ(2 Β· π₯))))) = (1rβπ)) |
179 | 120 | fmpttd 7064 |
. . . 4
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))):(1...((π β 1) / 2))βΆ(Baseβπ)) |
180 | | fvexd 6858 |
. . . . 5
β’ ((π β§ π₯ β (1...((π β 1) / 2))) β (πΏβ((-1βπ
) Β· π)) β V) |
181 | 129, 19, 180, 37 | fsuppmptdm 9317 |
. . . 4
β’ (π β (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π))) finSupp (0gβπΊ)) |
182 | 7, 8, 18, 19, 179, 181 | gsumcl 19693 |
. . 3
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π)))) β (Baseβπ)) |
183 | 6, 134, 175, 114 | dvrcan3 20122 |
. . 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 1372 |
. 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 2786 |
1
β’ (π β (πΊ Ξ£g (π₯ β (1...((π β 1) / 2)) β¦ (πΏβ((-1βπ
) Β· π)))) = (1rβπ)) |