Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . 3
โข (๐ โ ๐ โ (โ โ
{2})) |
2 | | gausslemma2d.h |
. . 3
โข ๐ป = ((๐ โ 1) / 2) |
3 | | gausslemma2d.r |
. . 3
โข ๐
= (๐ฅ โ (1...๐ป) โฆ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
4 | | gausslemma2d.m |
. . 3
โข ๐ = (โโ(๐ / 4)) |
5 | 1, 2, 3, 4 | gausslemma2dlem5a 26721 |
. 2
โข (๐ โ (โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) mod ๐) = (โ๐ โ ((๐ + 1)...๐ป)(-1 ยท (๐ ยท 2)) mod ๐)) |
6 | | fzfi 13878 |
. . . . . 6
โข ((๐ + 1)...๐ป) โ Fin |
7 | 6 | a1i 11 |
. . . . 5
โข (๐ โ ((๐ + 1)...๐ป) โ Fin) |
8 | | neg1cn 12268 |
. . . . . 6
โข -1 โ
โ |
9 | 8 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ -1 โ
โ) |
10 | | elfzelz 13442 |
. . . . . . . 8
โข (๐ โ ((๐ + 1)...๐ป) โ ๐ โ โค) |
11 | | 2z 12536 |
. . . . . . . . 9
โข 2 โ
โค |
12 | 11 | a1i 11 |
. . . . . . . 8
โข (๐ โ ((๐ + 1)...๐ป) โ 2 โ โค) |
13 | 10, 12 | zmulcld 12614 |
. . . . . . 7
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ ยท 2) โ โค) |
14 | 13 | zcnd 12609 |
. . . . . 6
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ ยท 2) โ โ) |
15 | 14 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐ ยท 2) โ โ) |
16 | 7, 9, 15 | fprodmul 15844 |
. . . 4
โข (๐ โ โ๐ โ ((๐ + 1)...๐ป)(-1 ยท (๐ ยท 2)) = (โ๐ โ ((๐ + 1)...๐ป)-1 ยท โ๐ โ ((๐ + 1)...๐ป)(๐ ยท 2))) |
17 | 6, 8 | pm3.2i 472 |
. . . . . . 7
โข (((๐ + 1)...๐ป) โ Fin โง -1 โ
โ) |
18 | | fprodconst 15862 |
. . . . . . 7
โข ((((๐ + 1)...๐ป) โ Fin โง -1 โ โ) โ
โ๐ โ ((๐ + 1)...๐ป)-1 = (-1โ(โฏโ((๐ + 1)...๐ป)))) |
19 | 17, 18 | mp1i 13 |
. . . . . 6
โข (๐ โ โ๐ โ ((๐ + 1)...๐ป)-1 = (-1โ(โฏโ((๐ + 1)...๐ป)))) |
20 | | nnoddn2prm 16684 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ยฌ 2 โฅ ๐)) |
21 | | nnre 12161 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ๐ โ
โ) |
23 | 1, 20, 22 | 3syl 18 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
24 | | 4re 12238 |
. . . . . . . . . . . . . . 15
โข 4 โ
โ |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 4 โ
โ) |
26 | | 4ne0 12262 |
. . . . . . . . . . . . . . 15
โข 4 โ
0 |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 4 โ 0) |
28 | 23, 25, 27 | redivcld 11984 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ / 4) โ โ) |
29 | 28 | flcld 13704 |
. . . . . . . . . . . 12
โข (๐ โ (โโ(๐ / 4)) โ
โค) |
30 | 4, 29 | eqeltrid 2842 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
31 | 30 | peano2zd 12611 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โค) |
32 | | nnz 12521 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โค) |
33 | | oddm1d2 16243 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) โ
โค)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) โ
โค)) |
35 | 34 | biimpa 478 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ((๐ โ 1) / 2) โ
โค) |
36 | 1, 20, 35 | 3syl 18 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ 1) / 2) โ
โค) |
37 | 2, 36 | eqeltrid 2842 |
. . . . . . . . . 10
โข (๐ โ ๐ป โ โค) |
38 | 1, 4, 2 | gausslemma2dlem0f 26712 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โค ๐ป) |
39 | | eluz2 12770 |
. . . . . . . . . 10
โข (๐ป โ
(โคโฅโ(๐ + 1)) โ ((๐ + 1) โ โค โง ๐ป โ โค โง (๐ + 1) โค ๐ป)) |
40 | 31, 37, 38, 39 | syl3anbrc 1344 |
. . . . . . . . 9
โข (๐ โ ๐ป โ (โคโฅโ(๐ + 1))) |
41 | | hashfz 14328 |
. . . . . . . . 9
โข (๐ป โ
(โคโฅโ(๐ + 1)) โ (โฏโ((๐ + 1)...๐ป)) = ((๐ป โ (๐ + 1)) + 1)) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
โข (๐ โ (โฏโ((๐ + 1)...๐ป)) = ((๐ป โ (๐ + 1)) + 1)) |
43 | 37 | zcnd 12609 |
. . . . . . . . . 10
โข (๐ โ ๐ป โ โ) |
44 | 30 | zcnd 12609 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
45 | | 1cnd 11151 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
46 | 43, 44, 45 | nppcan2d 11539 |
. . . . . . . . 9
โข (๐ โ ((๐ป โ (๐ + 1)) + 1) = (๐ป โ ๐)) |
47 | | gausslemma2d.n |
. . . . . . . . 9
โข ๐ = (๐ป โ ๐) |
48 | 46, 47 | eqtr4di 2795 |
. . . . . . . 8
โข (๐ โ ((๐ป โ (๐ + 1)) + 1) = ๐) |
49 | 42, 48 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (โฏโ((๐ + 1)...๐ป)) = ๐) |
50 | 49 | oveq2d 7374 |
. . . . . 6
โข (๐ โ
(-1โ(โฏโ((๐
+ 1)...๐ป))) =
(-1โ๐)) |
51 | 19, 50 | eqtrd 2777 |
. . . . 5
โข (๐ โ โ๐ โ ((๐ + 1)...๐ป)-1 = (-1โ๐)) |
52 | 51 | oveq1d 7373 |
. . . 4
โข (๐ โ (โ๐ โ ((๐ + 1)...๐ป)-1 ยท โ๐ โ ((๐ + 1)...๐ป)(๐ ยท 2)) = ((-1โ๐) ยท โ๐ โ ((๐ + 1)...๐ป)(๐ ยท 2))) |
53 | 16, 52 | eqtrd 2777 |
. . 3
โข (๐ โ โ๐ โ ((๐ + 1)...๐ป)(-1 ยท (๐ ยท 2)) = ((-1โ๐) ยท โ๐ โ ((๐ + 1)...๐ป)(๐ ยท 2))) |
54 | 53 | oveq1d 7373 |
. 2
โข (๐ โ (โ๐ โ ((๐ + 1)...๐ป)(-1 ยท (๐ ยท 2)) mod ๐) = (((-1โ๐) ยท โ๐ โ ((๐ + 1)...๐ป)(๐ ยท 2)) mod ๐)) |
55 | 5, 54 | eqtrd 2777 |
1
โข (๐ โ (โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) mod ๐) = (((-1โ๐) ยท โ๐ โ ((๐ + 1)...๐ป)(๐ ยท 2)) mod ๐)) |