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 | | gausslemma2d.n |
. . 3
โข ๐ = (๐ป โ ๐) |
6 | 1, 2, 3, 4, 5 | gausslemma2dlem6 26723 |
. 2
โข (๐ โ ((!โ๐ป) mod ๐) = ((((-1โ๐) ยท (2โ๐ป)) ยท (!โ๐ป)) mod ๐)) |
7 | 1, 2 | gausslemma2dlem0b 26708 |
. . . . . . . . . . 11
โข (๐ โ ๐ป โ โ) |
8 | 7 | nnnn0d 12474 |
. . . . . . . . . 10
โข (๐ โ ๐ป โ
โ0) |
9 | 8 | faccld 14185 |
. . . . . . . . 9
โข (๐ โ (!โ๐ป) โ โ) |
10 | 9 | nncnd 12170 |
. . . . . . . 8
โข (๐ โ (!โ๐ป) โ โ) |
11 | 10 | mulid2d 11174 |
. . . . . . 7
โข (๐ โ (1 ยท (!โ๐ป)) = (!โ๐ป)) |
12 | 11 | eqcomd 2743 |
. . . . . 6
โข (๐ โ (!โ๐ป) = (1 ยท (!โ๐ป))) |
13 | 12 | oveq1d 7373 |
. . . . 5
โข (๐ โ ((!โ๐ป) mod ๐) = ((1 ยท (!โ๐ป)) mod ๐)) |
14 | 13 | eqeq1d 2739 |
. . . 4
โข (๐ โ (((!โ๐ป) mod ๐) = ((((-1โ๐) ยท (2โ๐ป)) ยท (!โ๐ป)) mod ๐) โ ((1 ยท (!โ๐ป)) mod ๐) = ((((-1โ๐) ยท (2โ๐ป)) ยท (!โ๐ป)) mod ๐))) |
15 | | 1zzd 12535 |
. . . . 5
โข (๐ โ 1 โ
โค) |
16 | | neg1z 12540 |
. . . . . . 7
โข -1 โ
โค |
17 | 1, 4, 2, 5 | gausslemma2dlem0h 26714 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
18 | | zexpcl 13983 |
. . . . . . 7
โข ((-1
โ โค โง ๐
โ โ0) โ (-1โ๐) โ โค) |
19 | 16, 17, 18 | sylancr 588 |
. . . . . 6
โข (๐ โ (-1โ๐) โ โค) |
20 | | 2z 12536 |
. . . . . . 7
โข 2 โ
โค |
21 | | zexpcl 13983 |
. . . . . . 7
โข ((2
โ โค โง ๐ป
โ โ0) โ (2โ๐ป) โ โค) |
22 | 20, 8, 21 | sylancr 588 |
. . . . . 6
โข (๐ โ (2โ๐ป) โ โค) |
23 | 19, 22 | zmulcld 12614 |
. . . . 5
โข (๐ โ ((-1โ๐) ยท (2โ๐ป)) โ
โค) |
24 | 9 | nnzd 12527 |
. . . . 5
โข (๐ โ (!โ๐ป) โ โค) |
25 | | eldifi 4087 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
26 | | prmnn 16551 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
27 | 1, 25, 26 | 3syl 18 |
. . . . 5
โข (๐ โ ๐ โ โ) |
28 | 1, 2 | gausslemma2dlem0c 26709 |
. . . . 5
โข (๐ โ ((!โ๐ป) gcd ๐) = 1) |
29 | | cncongrcoprm 16547 |
. . . . 5
โข (((1
โ โค โง ((-1โ๐) ยท (2โ๐ป)) โ โค โง (!โ๐ป) โ โค) โง (๐ โ โ โง
((!โ๐ป) gcd ๐) = 1)) โ (((1 ยท
(!โ๐ป)) mod ๐) = ((((-1โ๐) ยท (2โ๐ป)) ยท (!โ๐ป)) mod ๐) โ (1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐))) |
30 | 15, 23, 24, 27, 28, 29 | syl32anc 1379 |
. . . 4
โข (๐ โ (((1 ยท
(!โ๐ป)) mod ๐) = ((((-1โ๐) ยท (2โ๐ป)) ยท (!โ๐ป)) mod ๐) โ (1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐))) |
31 | 14, 30 | bitrd 279 |
. . 3
โข (๐ โ (((!โ๐ป) mod ๐) = ((((-1โ๐) ยท (2โ๐ป)) ยท (!โ๐ป)) mod ๐) โ (1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐))) |
32 | | simpr 486 |
. . . . 5
โข ((๐ โง (1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐)) โ (1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐)) |
33 | 26 | nnred 12169 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
34 | | prmgt1 16574 |
. . . . . . . . 9
โข (๐ โ โ โ 1 <
๐) |
35 | 33, 34 | jca 513 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ โ โง 1 <
๐)) |
36 | 25, 35 | syl 17 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง 1 < ๐)) |
37 | | 1mod 13809 |
. . . . . . 7
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
38 | 1, 36, 37 | 3syl 18 |
. . . . . 6
โข (๐ โ (1 mod ๐) = 1) |
39 | 38 | adantr 482 |
. . . . 5
โข ((๐ โง (1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐)) โ (1 mod ๐) = 1) |
40 | 32, 39 | eqtr3d 2779 |
. . . 4
โข ((๐ โง (1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐)) โ (((-1โ๐) ยท (2โ๐ป)) mod ๐) = 1) |
41 | 40 | ex 414 |
. . 3
โข (๐ โ ((1 mod ๐) = (((-1โ๐) ยท (2โ๐ป)) mod ๐) โ (((-1โ๐) ยท (2โ๐ป)) mod ๐) = 1)) |
42 | 31, 41 | sylbid 239 |
. 2
โข (๐ โ (((!โ๐ป) mod ๐) = ((((-1โ๐) ยท (2โ๐ป)) ยท (!โ๐ป)) mod ๐) โ (((-1โ๐) ยท (2โ๐ป)) mod ๐) = 1)) |
43 | 6, 42 | mpd 15 |
1
โข (๐ โ (((-1โ๐) ยท (2โ๐ป)) mod ๐) = 1) |