Step | Hyp | Ref
| Expression |
1 | | lgseisen.2 |
. . . . 5
โข (๐ โ ๐ โ (โ โ
{2})) |
2 | 1 | eldifad 3961 |
. . . 4
โข (๐ โ ๐ โ โ) |
3 | | prmz 16612 |
. . . 4
โข (๐ โ โ โ ๐ โ
โค) |
4 | 2, 3 | syl 17 |
. . 3
โข (๐ โ ๐ โ โค) |
5 | | lgseisen.1 |
. . 3
โข (๐ โ ๐ โ (โ โ
{2})) |
6 | | lgsval3 26818 |
. . 3
โข ((๐ โ โค โง ๐ โ (โ โ {2}))
โ (๐
/L ๐) =
((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) |
7 | 4, 5, 6 | syl2anc 585 |
. 2
โข (๐ โ (๐ /L ๐) = ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) |
8 | 1 | gausslemma2dlem0a 26859 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
9 | | oddprm 16743 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
10 | 5, 9 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((๐ โ 1) / 2) โ
โ) |
11 | 10 | nnnn0d 12532 |
. . . . . . . 8
โข (๐ โ ((๐ โ 1) / 2) โ
โ0) |
12 | 8, 11 | nnexpcld 14208 |
. . . . . . 7
โข (๐ โ (๐โ((๐ โ 1) / 2)) โ
โ) |
13 | 12 | nnred 12227 |
. . . . . 6
โข (๐ โ (๐โ((๐ โ 1) / 2)) โ
โ) |
14 | | neg1rr 12327 |
. . . . . . . 8
โข -1 โ
โ |
15 | 14 | a1i 11 |
. . . . . . 7
โข (๐ โ -1 โ
โ) |
16 | | neg1ne0 12328 |
. . . . . . . 8
โข -1 โ
0 |
17 | 16 | a1i 11 |
. . . . . . 7
โข (๐ โ -1 โ
0) |
18 | | fzfid 13938 |
. . . . . . . 8
โข (๐ โ (1...((๐ โ 1) / 2)) โ
Fin) |
19 | 8 | nnred 12227 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
20 | 5 | gausslemma2dlem0a 26859 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
21 | 19, 20 | nndivred 12266 |
. . . . . . . . . . 11
โข (๐ โ (๐ / ๐) โ โ) |
22 | 21 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ / ๐) โ โ) |
23 | | 2re 12286 |
. . . . . . . . . . 11
โข 2 โ
โ |
24 | | elfznn 13530 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ ๐ฅ โ โ) |
25 | 24 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ฅ โ โ) |
26 | 25 | nnred 12227 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ฅ โ โ) |
27 | | remulcl 11195 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐ฅ
โ โ) โ (2 ยท ๐ฅ) โ โ) |
28 | 23, 26, 27 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (2 ยท ๐ฅ) โ
โ) |
29 | 22, 28 | remulcld 11244 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ / ๐) ยท (2 ยท ๐ฅ)) โ โ) |
30 | 29 | flcld 13763 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ
(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))) โ
โค) |
31 | 18, 30 | fsumzcl 15681 |
. . . . . . 7
โข (๐ โ ฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))) โ โค) |
32 | 15, 17, 31 | reexpclzd 14212 |
. . . . . 6
โข (๐ โ (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) โ โ) |
33 | | 1re 11214 |
. . . . . . 7
โข 1 โ
โ |
34 | 33 | a1i 11 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
35 | 20 | nnrpd 13014 |
. . . . . 6
โข (๐ โ ๐ โ
โ+) |
36 | | lgseisen.3 |
. . . . . . 7
โข (๐ โ ๐ โ ๐) |
37 | | eqid 2733 |
. . . . . . 7
โข ((๐ ยท (2 ยท ๐ฅ)) mod ๐) = ((๐ ยท (2 ยท ๐ฅ)) mod ๐) |
38 | | eqid 2733 |
. . . . . . 7
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โฆ
((((-1โ((๐ ยท (2
ยท ๐ฅ)) mod ๐)) ยท ((๐ ยท (2 ยท ๐ฅ)) mod ๐)) mod ๐) / 2)) = (๐ฅ โ (1...((๐ โ 1) / 2)) โฆ
((((-1โ((๐ ยท (2
ยท ๐ฅ)) mod ๐)) ยท ((๐ ยท (2 ยท ๐ฅ)) mod ๐)) mod ๐) / 2)) |
39 | | eqid 2733 |
. . . . . . 7
โข ((๐ ยท (2 ยท ๐ฆ)) mod ๐) = ((๐ ยท (2 ยท ๐ฆ)) mod ๐) |
40 | | eqid 2733 |
. . . . . . 7
โข
(โค/nโคโ๐) = (โค/nโคโ๐) |
41 | | eqid 2733 |
. . . . . . 7
โข
(mulGrpโ(โค/nโคโ๐)) =
(mulGrpโ(โค/nโคโ๐)) |
42 | | eqid 2733 |
. . . . . . 7
โข
(โคRHomโ(โค/nโคโ๐)) =
(โคRHomโ(โค/nโคโ๐)) |
43 | 5, 1, 36, 37, 38, 39, 40, 41, 42 | lgseisenlem4 26881 |
. . . . . 6
โข (๐ โ ((๐โ((๐ โ 1) / 2)) mod ๐) = ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) mod ๐)) |
44 | | modadd1 13873 |
. . . . . 6
โข ((((๐โ((๐ โ 1) / 2)) โ โ โง
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โ โ) โง
(1 โ โ โง ๐
โ โ+) โง ((๐โ((๐ โ 1) / 2)) mod ๐) = ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) mod ๐)) โ (((๐โ((๐ โ 1) / 2)) + 1) mod ๐) = (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) mod ๐)) |
45 | 13, 32, 34, 35, 43, 44 | syl221anc 1382 |
. . . . 5
โข (๐ โ (((๐โ((๐ โ 1) / 2)) + 1) mod ๐) = (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) mod ๐)) |
46 | | peano2re 11387 |
. . . . . . 7
โข
((-1โฮฃ๐ฅ
โ (1...((๐ โ 1)
/ 2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โ โ โ
((-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) + 1) โ
โ) |
47 | 32, 46 | syl 17 |
. . . . . 6
โข (๐ โ ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) โ โ) |
48 | | df-neg 11447 |
. . . . . . . 8
โข -1 = (0
โ 1) |
49 | | neg1cn 12326 |
. . . . . . . . . . . . 13
โข -1 โ
โ |
50 | | absexpz 15252 |
. . . . . . . . . . . . 13
โข ((-1
โ โ โง -1 โ 0 โง ฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))) โ โค) โ
(absโ(-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) = ((absโ-1)โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) |
51 | 49, 16, 31, 50 | mp3an12i 1466 |
. . . . . . . . . . . 12
โข (๐ โ
(absโ(-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) = ((absโ-1)โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) |
52 | | ax-1cn 11168 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ |
53 | 52 | absnegi 15347 |
. . . . . . . . . . . . . . 15
โข
(absโ-1) = (absโ1) |
54 | | abs1 15244 |
. . . . . . . . . . . . . . 15
โข
(absโ1) = 1 |
55 | 53, 54 | eqtri 2761 |
. . . . . . . . . . . . . 14
โข
(absโ-1) = 1 |
56 | 55 | oveq1i 7419 |
. . . . . . . . . . . . 13
โข
((absโ-1)โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) = (1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) |
57 | | 1exp 14057 |
. . . . . . . . . . . . . 14
โข
(ฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ))) โ โค โ
(1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) = 1) |
58 | 31, 57 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) = 1) |
59 | 56, 58 | eqtrid 2785 |
. . . . . . . . . . . 12
โข (๐ โ
((absโ-1)โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) = 1) |
60 | 51, 59 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ
(absโ(-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) = 1) |
61 | | 1le1 11842 |
. . . . . . . . . . 11
โข 1 โค
1 |
62 | 60, 61 | eqbrtrdi 5188 |
. . . . . . . . . 10
โข (๐ โ
(absโ(-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) โค 1) |
63 | | absle 15262 |
. . . . . . . . . . 11
โข
(((-1โฮฃ๐ฅ
โ (1...((๐ โ 1)
/ 2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โ โ โง
1 โ โ) โ ((absโ(-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) โค 1 โ (-1 โค
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โง
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โค
1))) |
64 | 32, 33, 63 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ
((absโ(-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) โค 1 โ (-1 โค
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โง
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โค
1))) |
65 | 62, 64 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (-1 โค
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โง
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โค
1)) |
66 | 65 | simpld 496 |
. . . . . . . 8
โข (๐ โ -1 โค
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ))))) |
67 | 48, 66 | eqbrtrrid 5185 |
. . . . . . 7
โข (๐ โ (0 โ 1) โค
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ))))) |
68 | | 0red 11217 |
. . . . . . . 8
โข (๐ โ 0 โ
โ) |
69 | 68, 34, 32 | lesubaddd 11811 |
. . . . . . 7
โข (๐ โ ((0 โ 1) โค
(-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โ 0 โค
((-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) +
1))) |
70 | 67, 69 | mpbid 231 |
. . . . . 6
โข (๐ โ 0 โค
((-1โฮฃ๐ฅ โ
(1...((๐ โ 1) /
2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) +
1)) |
71 | 20 | nnred 12227 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
72 | | peano2rem 11527 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
73 | 71, 72 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) โ โ) |
74 | 65 | simprd 497 |
. . . . . . . 8
โข (๐ โ (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) โค 1) |
75 | | df-2 12275 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
76 | 23 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
77 | 5 | eldifad 3961 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
78 | | prmuz2 16633 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
79 | | eluzle 12835 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ2) โ 2 โค ๐) |
80 | 77, 78, 79 | 3syl 18 |
. . . . . . . . . . 11
โข (๐ โ 2 โค ๐) |
81 | | eldifsni 4794 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ ๐ โ
2) |
82 | 5, 81 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ 2) |
83 | 76, 71, 80, 82 | leneltd 11368 |
. . . . . . . . . 10
โข (๐ โ 2 < ๐) |
84 | 75, 83 | eqbrtrrid 5185 |
. . . . . . . . 9
โข (๐ โ (1 + 1) < ๐) |
85 | 34, 34, 71 | ltaddsubd 11814 |
. . . . . . . . 9
โข (๐ โ ((1 + 1) < ๐ โ 1 < (๐ โ 1))) |
86 | 84, 85 | mpbid 231 |
. . . . . . . 8
โข (๐ โ 1 < (๐ โ 1)) |
87 | 32, 34, 73, 74, 86 | lelttrd 11372 |
. . . . . . 7
โข (๐ โ (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) < (๐ โ 1)) |
88 | 32, 34, 71 | ltaddsubd 11814 |
. . . . . . 7
โข (๐ โ (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) < ๐ โ (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) < (๐ โ 1))) |
89 | 87, 88 | mpbird 257 |
. . . . . 6
โข (๐ โ ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) < ๐) |
90 | | modid 13861 |
. . . . . 6
โข
(((((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) โ โ โง ๐ โ โ+)
โง (0 โค ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) โง ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) < ๐)) โ (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) mod ๐) = ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1)) |
91 | 47, 35, 70, 89, 90 | syl22anc 838 |
. . . . 5
โข (๐ โ (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) mod ๐) = ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1)) |
92 | 45, 91 | eqtrd 2773 |
. . . 4
โข (๐ โ (((๐โ((๐ โ 1) / 2)) + 1) mod ๐) = ((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1)) |
93 | 92 | oveq1d 7424 |
. . 3
โข (๐ โ ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) = (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) โ 1)) |
94 | 32 | recnd 11242 |
. . . 4
โข (๐ โ (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) โ โ) |
95 | | pncan 11466 |
. . . 4
โข
(((-1โฮฃ๐ฅ
โ (1...((๐ โ 1)
/ 2))(โโ((๐ /
๐) ยท (2 ยท
๐ฅ)))) โ โ โง
1 โ โ) โ (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) โ 1) = (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) |
96 | 94, 52, 95 | sylancl 587 |
. . 3
โข (๐ โ (((-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ)))) + 1) โ 1) = (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) |
97 | 93, 96 | eqtrd 2773 |
. 2
โข (๐ โ ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) = (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) |
98 | 7, 97 | eqtrd 2773 |
1
โข (๐ โ (๐ /L ๐) = (-1โฮฃ๐ฅ โ (1...((๐ โ 1) / 2))(โโ((๐ / ๐) ยท (2 ยท ๐ฅ))))) |