Step | Hyp | Ref
| Expression |
1 | | lgsqr.t |
. . . . 5
β’ π = ((((π β 1) / 2) β π) β 1 ) |
2 | 1 | fveq2i 6846 |
. . . 4
β’ (πβπ) = (πβ((((π β 1) / 2) β π) β 1 )) |
3 | 2 | fveq1i 6844 |
. . 3
β’ ((πβπ)β(πΏβπ΄)) = ((πβ((((π β 1) / 2) β π) β 1 ))β(πΏβπ΄)) |
4 | | lgsqr.o |
. . . . 5
β’ π = (eval1βπ) |
5 | | lgsqr.s |
. . . . 5
β’ π = (Poly1βπ) |
6 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
7 | | lgsqr.b |
. . . . 5
β’ π΅ = (Baseβπ) |
8 | | lgsqr.1 |
. . . . . . . . 9
β’ (π β π β (β β
{2})) |
9 | 8 | eldifad 3923 |
. . . . . . . 8
β’ (π β π β β) |
10 | | lgsqr.y |
. . . . . . . . 9
β’ π =
(β€/nβ€βπ) |
11 | 10 | znfld 20970 |
. . . . . . . 8
β’ (π β β β π β Field) |
12 | 9, 11 | syl 17 |
. . . . . . 7
β’ (π β π β Field) |
13 | | fldidom 20778 |
. . . . . . 7
β’ (π β Field β π β IDomn) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π β π β IDomn) |
15 | | isidom 20777 |
. . . . . . 7
β’ (π β IDomn β (π β CRing β§ π β Domn)) |
16 | 15 | simplbi 499 |
. . . . . 6
β’ (π β IDomn β π β CRing) |
17 | 14, 16 | syl 17 |
. . . . 5
β’ (π β π β CRing) |
18 | | crngring 19977 |
. . . . . . . . 9
β’ (π β CRing β π β Ring) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
β’ (π β π β Ring) |
20 | | lgsqr.l |
. . . . . . . . 9
β’ πΏ = (β€RHomβπ) |
21 | 20 | zrhrhm 20915 |
. . . . . . . 8
β’ (π β Ring β πΏ β (β€ring
RingHom π)) |
22 | 19, 21 | syl 17 |
. . . . . . 7
β’ (π β πΏ β (β€ring RingHom
π)) |
23 | | zringbas 20878 |
. . . . . . . 8
β’ β€ =
(Baseββ€ring) |
24 | 23, 6 | rhmf 20159 |
. . . . . . 7
β’ (πΏ β (β€ring
RingHom π) β πΏ:β€βΆ(Baseβπ)) |
25 | 22, 24 | syl 17 |
. . . . . 6
β’ (π β πΏ:β€βΆ(Baseβπ)) |
26 | | lgsqrlem1.3 |
. . . . . 6
β’ (π β π΄ β β€) |
27 | 25, 26 | ffvelcdmd 7037 |
. . . . 5
β’ (π β (πΏβπ΄) β (Baseβπ)) |
28 | | lgsqr.x |
. . . . . . . 8
β’ π = (var1βπ) |
29 | 4, 28, 6, 5, 7, 17,
27 | evl1vard 21706 |
. . . . . . 7
β’ (π β (π β π΅ β§ ((πβπ)β(πΏβπ΄)) = (πΏβπ΄))) |
30 | | lgsqr.e |
. . . . . . 7
β’ β =
(.gβ(mulGrpβπ)) |
31 | | eqid 2737 |
. . . . . . 7
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
32 | | oddprm 16683 |
. . . . . . . . 9
β’ (π β (β β {2})
β ((π β 1) / 2)
β β) |
33 | 8, 32 | syl 17 |
. . . . . . . 8
β’ (π β ((π β 1) / 2) β
β) |
34 | 33 | nnnn0d 12474 |
. . . . . . 7
β’ (π β ((π β 1) / 2) β
β0) |
35 | 4, 5, 6, 7, 17, 27, 29, 30, 31, 34 | evl1expd 21714 |
. . . . . 6
β’ (π β ((((π β 1) / 2) β π) β π΅ β§ ((πβ(((π β 1) / 2) β π))β(πΏβπ΄)) = (((π β 1) /
2)(.gβ(mulGrpβπ))(πΏβπ΄)))) |
36 | | zringmpg 20895 |
. . . . . . . . . . . 12
β’
((mulGrpββfld) βΎs β€) =
(mulGrpββ€ring) |
37 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(mulGrpβπ) =
(mulGrpβπ) |
38 | 36, 37 | rhmmhm 20154 |
. . . . . . . . . . 11
β’ (πΏ β (β€ring
RingHom π) β πΏ β
(((mulGrpββfld) βΎs β€) MndHom
(mulGrpβπ))) |
39 | 22, 38 | syl 17 |
. . . . . . . . . 10
β’ (π β πΏ β
(((mulGrpββfld) βΎs β€) MndHom
(mulGrpβπ))) |
40 | 36, 23 | mgpbas 19903 |
. . . . . . . . . . 11
β’ β€ =
(Baseβ((mulGrpββfld) βΎs
β€)) |
41 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.gβ((mulGrpββfld)
βΎs β€)) =
(.gβ((mulGrpββfld) βΎs
β€)) |
42 | 40, 41, 31 | mhmmulg 18918 |
. . . . . . . . . 10
β’ ((πΏ β
(((mulGrpββfld) βΎs β€) MndHom
(mulGrpβπ)) β§
((π β 1) / 2) β
β0 β§ π΄
β β€) β (πΏβ(((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π΄)) = (((π β 1) /
2)(.gβ(mulGrpβπ))(πΏβπ΄))) |
43 | 39, 34, 26, 42 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (πΏβ(((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π΄)) = (((π β 1) /
2)(.gβ(mulGrpβπ))(πΏβπ΄))) |
44 | | zsubrg 20853 |
. . . . . . . . . . . . . 14
β’ β€
β (SubRingββfld) |
45 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(mulGrpββfld) =
(mulGrpββfld) |
46 | 45 | subrgsubm 20238 |
. . . . . . . . . . . . . 14
β’ (β€
β (SubRingββfld) β β€ β
(SubMndβ(mulGrpββfld))) |
47 | 44, 46 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (π β β€ β
(SubMndβ(mulGrpββfld))) |
48 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(.gβ(mulGrpββfld)) =
(.gβ(mulGrpββfld)) |
49 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
((mulGrpββfld) βΎs β€) =
((mulGrpββfld) βΎs
β€) |
50 | 48, 49, 41 | submmulg 18921 |
. . . . . . . . . . . . 13
β’ ((β€
β (SubMndβ(mulGrpββfld)) β§ ((π β 1) / 2) β
β0 β§ π΄
β β€) β (((π
β 1) / 2)(.gβ(mulGrpββfld))π΄) = (((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π΄)) |
51 | 47, 34, 26, 50 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β (((π β 1) /
2)(.gβ(mulGrpββfld))π΄) = (((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π΄)) |
52 | 26 | zcnd 12609 |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
53 | | cnfldexp 20833 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β 1) / 2) β
β0) β (((π β 1) /
2)(.gβ(mulGrpββfld))π΄) = (π΄β((π β 1) / 2))) |
54 | 52, 34, 53 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (((π β 1) /
2)(.gβ(mulGrpββfld))π΄) = (π΄β((π β 1) / 2))) |
55 | 51, 54 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ (π β (((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π΄) = (π΄β((π β 1) / 2))) |
56 | 55 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π β (πΏβ(((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π΄)) = (πΏβ(π΄β((π β 1) / 2)))) |
57 | | lgsqrlem1.4 |
. . . . . . . . . . . 12
β’ (π β ((π΄β((π β 1) / 2)) mod π) = (1 mod π)) |
58 | | prmnn 16551 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
59 | 9, 58 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
60 | | zexpcl 13983 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β€ β§ ((π β 1) / 2) β
β0) β (π΄β((π β 1) / 2)) β
β€) |
61 | 26, 34, 60 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (π΄β((π β 1) / 2)) β
β€) |
62 | | 1zzd 12535 |
. . . . . . . . . . . . 13
β’ (π β 1 β
β€) |
63 | | moddvds 16148 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π΄β((π β 1) / 2)) β β€ β§ 1
β β€) β (((π΄β((π β 1) / 2)) mod π) = (1 mod π) β π β₯ ((π΄β((π β 1) / 2)) β
1))) |
64 | 59, 61, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β (((π΄β((π β 1) / 2)) mod π) = (1 mod π) β π β₯ ((π΄β((π β 1) / 2)) β
1))) |
65 | 57, 64 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β π β₯ ((π΄β((π β 1) / 2)) β
1)) |
66 | 59 | nnnn0d 12474 |
. . . . . . . . . . . 12
β’ (π β π β
β0) |
67 | 10, 20 | zndvds 20959 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π΄β((π β 1) / 2)) β β€
β§ 1 β β€) β ((πΏβ(π΄β((π β 1) / 2))) = (πΏβ1) β π β₯ ((π΄β((π β 1) / 2)) β
1))) |
68 | 66, 61, 62, 67 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β ((πΏβ(π΄β((π β 1) / 2))) = (πΏβ1) β π β₯ ((π΄β((π β 1) / 2)) β
1))) |
69 | 65, 68 | mpbird 257 |
. . . . . . . . . 10
β’ (π β (πΏβ(π΄β((π β 1) / 2))) = (πΏβ1)) |
70 | | zring1 20883 |
. . . . . . . . . . . 12
β’ 1 =
(1rββ€ring) |
71 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(1rβπ) = (1rβπ) |
72 | 70, 71 | rhm1 20163 |
. . . . . . . . . . 11
β’ (πΏ β (β€ring
RingHom π) β (πΏβ1) =
(1rβπ)) |
73 | 22, 72 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΏβ1) = (1rβπ)) |
74 | 56, 69, 73 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (π β (πΏβ(((π β 1) /
2)(.gβ((mulGrpββfld)
βΎs β€))π΄)) = (1rβπ)) |
75 | 43, 74 | eqtr3d 2779 |
. . . . . . . 8
β’ (π β (((π β 1) /
2)(.gβ(mulGrpβπ))(πΏβπ΄)) = (1rβπ)) |
76 | 75 | eqeq2d 2748 |
. . . . . . 7
β’ (π β (((πβ(((π β 1) / 2) β π))β(πΏβπ΄)) = (((π β 1) /
2)(.gβ(mulGrpβπ))(πΏβπ΄)) β ((πβ(((π β 1) / 2) β π))β(πΏβπ΄)) = (1rβπ))) |
77 | 76 | anbi2d 630 |
. . . . . 6
β’ (π β (((((π β 1) / 2) β π) β π΅ β§ ((πβ(((π β 1) / 2) β π))β(πΏβπ΄)) = (((π β 1) /
2)(.gβ(mulGrpβπ))(πΏβπ΄))) β ((((π β 1) / 2) β π) β π΅ β§ ((πβ(((π β 1) / 2) β π))β(πΏβπ΄)) = (1rβπ)))) |
78 | 35, 77 | mpbid 231 |
. . . . 5
β’ (π β ((((π β 1) / 2) β π) β π΅ β§ ((πβ(((π β 1) / 2) β π))β(πΏβπ΄)) = (1rβπ))) |
79 | | eqid 2737 |
. . . . . . 7
β’
(algScβπ) =
(algScβπ) |
80 | 6, 71 | ringidcl 19990 |
. . . . . . . 8
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
81 | 19, 80 | syl 17 |
. . . . . . 7
β’ (π β (1rβπ) β (Baseβπ)) |
82 | 4, 5, 6, 79, 7, 17, 81, 27 | evl1scad 21704 |
. . . . . 6
β’ (π β (((algScβπ)β(1rβπ)) β π΅ β§ ((πβ((algScβπ)β(1rβπ)))β(πΏβπ΄)) = (1rβπ))) |
83 | | lgsqr.u |
. . . . . . . . . 10
β’ 1 =
(1rβπ) |
84 | 5, 79, 71, 83 | ply1scl1 21666 |
. . . . . . . . 9
β’ (π β Ring β
((algScβπ)β(1rβπ)) = 1 ) |
85 | 19, 84 | syl 17 |
. . . . . . . 8
β’ (π β ((algScβπ)β(1rβπ)) = 1 ) |
86 | 85 | eleq1d 2823 |
. . . . . . 7
β’ (π β (((algScβπ)β(1rβπ)) β π΅ β 1 β π΅)) |
87 | 85 | fveq2d 6847 |
. . . . . . . . 9
β’ (π β (πβ((algScβπ)β(1rβπ))) = (πβ 1 )) |
88 | 87 | fveq1d 6845 |
. . . . . . . 8
β’ (π β ((πβ((algScβπ)β(1rβπ)))β(πΏβπ΄)) = ((πβ 1 )β(πΏβπ΄))) |
89 | 88 | eqeq1d 2739 |
. . . . . . 7
β’ (π β (((πβ((algScβπ)β(1rβπ)))β(πΏβπ΄)) = (1rβπ) β ((πβ 1 )β(πΏβπ΄)) = (1rβπ))) |
90 | 86, 89 | anbi12d 632 |
. . . . . 6
β’ (π β ((((algScβπ)β(1rβπ)) β π΅ β§ ((πβ((algScβπ)β(1rβπ)))β(πΏβπ΄)) = (1rβπ)) β ( 1 β π΅ β§ ((πβ 1 )β(πΏβπ΄)) = (1rβπ)))) |
91 | 82, 90 | mpbid 231 |
. . . . 5
β’ (π β ( 1 β π΅ β§ ((πβ 1 )β(πΏβπ΄)) = (1rβπ))) |
92 | | lgsqr.m |
. . . . 5
β’ β =
(-gβπ) |
93 | | eqid 2737 |
. . . . 5
β’
(-gβπ) = (-gβπ) |
94 | 4, 5, 6, 7, 17, 27, 78, 91, 92, 93 | evl1subd 21711 |
. . . 4
β’ (π β (((((π β 1) / 2) β π) β 1 ) β π΅ β§ ((πβ((((π β 1) / 2) β π) β 1 ))β(πΏβπ΄)) = ((1rβπ)(-gβπ)(1rβπ)))) |
95 | 94 | simprd 497 |
. . 3
β’ (π β ((πβ((((π β 1) / 2) β π) β 1 ))β(πΏβπ΄)) = ((1rβπ)(-gβπ)(1rβπ))) |
96 | 3, 95 | eqtrid 2789 |
. 2
β’ (π β ((πβπ)β(πΏβπ΄)) = ((1rβπ)(-gβπ)(1rβπ))) |
97 | | ringgrp 19970 |
. . . 4
β’ (π β Ring β π β Grp) |
98 | 19, 97 | syl 17 |
. . 3
β’ (π β π β Grp) |
99 | | eqid 2737 |
. . . 4
β’
(0gβπ) = (0gβπ) |
100 | 6, 99, 93 | grpsubid 18832 |
. . 3
β’ ((π β Grp β§
(1rβπ)
β (Baseβπ))
β ((1rβπ)(-gβπ)(1rβπ)) = (0gβπ)) |
101 | 98, 81, 100 | syl2anc 585 |
. 2
β’ (π β
((1rβπ)(-gβπ)(1rβπ)) = (0gβπ)) |
102 | 96, 101 | eqtrd 2777 |
1
β’ (π β ((πβπ)β(πΏβπ΄)) = (0gβπ)) |