Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . . 4
โข (๐ โ ๐ โ (โ โ
{2})) |
2 | | gausslemma2d.h |
. . . 4
โข ๐ป = ((๐ โ 1) / 2) |
3 | | gausslemma2d.r |
. . . 4
โข ๐
= (๐ฅ โ (1...๐ป) โฆ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
4 | | gausslemma2d.m |
. . . 4
โข ๐ = (โโ(๐ / 4)) |
5 | 1, 2, 3, 4 | gausslemma2dlem3 26719 |
. . 3
โข (๐ โ โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) = (๐ โ (๐ ยท 2))) |
6 | | prodeq2 15798 |
. . . 4
โข
(โ๐ โ
((๐ + 1)...๐ป)(๐
โ๐) = (๐ โ (๐ ยท 2)) โ โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) = โ๐ โ ((๐ + 1)...๐ป)(๐ โ (๐ ยท 2))) |
7 | 6 | oveq1d 7373 |
. . 3
โข
(โ๐ โ
((๐ + 1)...๐ป)(๐
โ๐) = (๐ โ (๐ ยท 2)) โ (โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) mod ๐) = (โ๐ โ ((๐ + 1)...๐ป)(๐ โ (๐ ยท 2)) mod ๐)) |
8 | 5, 7 | syl 17 |
. 2
โข (๐ โ (โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) mod ๐) = (โ๐ โ ((๐ + 1)...๐ป)(๐ โ (๐ ยท 2)) mod ๐)) |
9 | | eldifi 4087 |
. . 3
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
10 | | fzfid 13879 |
. . . 4
โข (๐ โ โ โ ((๐ + 1)...๐ป) โ Fin) |
11 | | prmz 16552 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
12 | 11 | adantr 482 |
. . . . 5
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ ๐ โ โค) |
13 | | elfzelz 13442 |
. . . . . . 7
โข (๐ โ ((๐ + 1)...๐ป) โ ๐ โ โค) |
14 | | 2z 12536 |
. . . . . . . 8
โข 2 โ
โค |
15 | 14 | a1i 11 |
. . . . . . 7
โข (๐ โ ((๐ + 1)...๐ป) โ 2 โ โค) |
16 | 13, 15 | zmulcld 12614 |
. . . . . 6
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ ยท 2) โ โค) |
17 | 16 | adantl 483 |
. . . . 5
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐ ยท 2) โ โค) |
18 | 12, 17 | zsubcld 12613 |
. . . 4
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐ โ (๐ ยท 2)) โ
โค) |
19 | | neg1z 12540 |
. . . . . . 7
โข -1 โ
โค |
20 | 19 | a1i 11 |
. . . . . 6
โข (๐ โ ((๐ + 1)...๐ป) โ -1 โ โค) |
21 | 20, 16 | zmulcld 12614 |
. . . . 5
โข (๐ โ ((๐ + 1)...๐ป) โ (-1 ยท (๐ ยท 2)) โ
โค) |
22 | 21 | adantl 483 |
. . . 4
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ (-1 ยท (๐ ยท 2)) โ
โค) |
23 | | prmnn 16551 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ) |
24 | 16 | zcnd 12609 |
. . . . . . . 8
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ ยท 2) โ โ) |
25 | 24 | mulm1d 11608 |
. . . . . . 7
โข (๐ โ ((๐ + 1)...๐ป) โ (-1 ยท (๐ ยท 2)) = -(๐ ยท 2)) |
26 | 25 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ (-1 ยท (๐ ยท 2)) = -(๐ ยท 2)) |
27 | 26 | oveq1d 7373 |
. . . . 5
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ ((-1 ยท (๐ ยท 2)) mod ๐) = (-(๐ ยท 2) mod ๐)) |
28 | 16 | zred 12608 |
. . . . . 6
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ ยท 2) โ โ) |
29 | 23 | nnrpd 12956 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ+) |
30 | | negmod 13822 |
. . . . . 6
โข (((๐ ยท 2) โ โ
โง ๐ โ
โ+) โ (-(๐ ยท 2) mod ๐) = ((๐ โ (๐ ยท 2)) mod ๐)) |
31 | 28, 29, 30 | syl2anr 598 |
. . . . 5
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ (-(๐ ยท 2) mod ๐) = ((๐ โ (๐ ยท 2)) mod ๐)) |
32 | 27, 31 | eqtr2d 2778 |
. . . 4
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ ((๐ โ (๐ ยท 2)) mod ๐) = ((-1 ยท (๐ ยท 2)) mod ๐)) |
33 | 10, 18, 22, 23, 32 | fprodmodd 15881 |
. . 3
โข (๐ โ โ โ
(โ๐ โ ((๐ + 1)...๐ป)(๐ โ (๐ ยท 2)) mod ๐) = (โ๐ โ ((๐ + 1)...๐ป)(-1 ยท (๐ ยท 2)) mod ๐)) |
34 | 1, 9, 33 | 3syl 18 |
. 2
โข (๐ โ (โ๐ โ ((๐ + 1)...๐ป)(๐ โ (๐ ยท 2)) mod ๐) = (โ๐ โ ((๐ + 1)...๐ป)(-1 ยท (๐ ยท 2)) mod ๐)) |
35 | 8, 34 | eqtrd 2777 |
1
โข (๐ โ (โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) mod ๐) = (โ๐ โ ((๐ + 1)...๐ป)(-1 ยท (๐ ยท 2)) mod ๐)) |