Step | Hyp | Ref
| Expression |
1 | | 41prothprm.p |
. . . . 5
โข ๐ = ;41 |
2 | 1 | 41prothprmlem1 45883 |
. . . 4
โข ((๐ โ 1) / 2) = ;20 |
3 | 2 | oveq2i 7373 |
. . 3
โข
(3โ((๐ โ
1) / 2)) = (3โ;20) |
4 | 3 | oveq1i 7372 |
. 2
โข
((3โ((๐ โ
1) / 2)) mod ๐) =
((3โ;20) mod ๐) |
5 | | 5cn 12248 |
. . . . . . . . 9
โข 5 โ
โ |
6 | | 4cn 12245 |
. . . . . . . . 9
โข 4 โ
โ |
7 | | 5t4e20 12727 |
. . . . . . . . 9
โข (5
ยท 4) = ;20 |
8 | 5, 6, 7 | mulcomli 11171 |
. . . . . . . 8
โข (4
ยท 5) = ;20 |
9 | 8 | eqcomi 2746 |
. . . . . . 7
โข ;20 = (4 ยท 5) |
10 | 9 | oveq2i 7373 |
. . . . . 6
โข
(3โ;20) = (3โ(4
ยท 5)) |
11 | | 3cn 12241 |
. . . . . . 7
โข 3 โ
โ |
12 | | 4nn0 12439 |
. . . . . . 7
โข 4 โ
โ0 |
13 | | 5nn0 12440 |
. . . . . . 7
โข 5 โ
โ0 |
14 | | expmul 14020 |
. . . . . . 7
โข ((3
โ โ โง 4 โ โ0 โง 5 โ
โ0) โ (3โ(4 ยท 5)) =
((3โ4)โ5)) |
15 | 11, 12, 13, 14 | mp3an 1462 |
. . . . . 6
โข
(3โ(4 ยท 5)) = ((3โ4)โ5) |
16 | 10, 15 | eqtri 2765 |
. . . . 5
โข
(3โ;20) =
((3โ4)โ5) |
17 | 16 | oveq1i 7372 |
. . . 4
โข
((3โ;20) mod ;41) = (((3โ4)โ5) mod ;41) |
18 | | 3z 12543 |
. . . . . . 7
โข 3 โ
โค |
19 | | zexpcl 13989 |
. . . . . . 7
โข ((3
โ โค โง 4 โ โ0) โ (3โ4) โ
โค) |
20 | 18, 12, 19 | mp2an 691 |
. . . . . 6
โข
(3โ4) โ โค |
21 | | neg1z 12546 |
. . . . . 6
โข -1 โ
โค |
22 | 20, 21 | pm3.2i 472 |
. . . . 5
โข
((3โ4) โ โค โง -1 โ โค) |
23 | | 1nn 12171 |
. . . . . . . 8
โข 1 โ
โ |
24 | 12, 23 | decnncl 12645 |
. . . . . . 7
โข ;41 โ โ |
25 | | nnrp 12933 |
. . . . . . 7
โข (;41 โ โ โ ;41 โ
โ+) |
26 | 24, 25 | ax-mp 5 |
. . . . . 6
โข ;41 โ
โ+ |
27 | 13, 26 | pm3.2i 472 |
. . . . 5
โข (5 โ
โ0 โง ;41
โ โ+) |
28 | | 3exp4mod41 45882 |
. . . . 5
โข
((3โ4) mod ;41) = (-1
mod ;41) |
29 | | modexp 14148 |
. . . . 5
โข
((((3โ4) โ โค โง -1 โ โค) โง (5 โ
โ0 โง ;41
โ โ+) โง ((3โ4) mod ;41) = (-1 mod ;41)) โ (((3โ4)โ5) mod ;41) = ((-1โ5) mod ;41)) |
30 | 22, 27, 28, 29 | mp3an 1462 |
. . . 4
โข
(((3โ4)โ5) mod ;41) = ((-1โ5) mod ;41) |
31 | | 3p2e5 12311 |
. . . . . . . 8
โข (3 + 2) =
5 |
32 | 31 | eqcomi 2746 |
. . . . . . 7
โข 5 = (3 +
2) |
33 | 32 | oveq2i 7373 |
. . . . . 6
โข
(-1โ5) = (-1โ(3 + 2)) |
34 | | 2z 12542 |
. . . . . . . 8
โข 2 โ
โค |
35 | | m1expaddsub 19287 |
. . . . . . . 8
โข ((3
โ โค โง 2 โ โค) โ (-1โ(3 โ 2)) =
(-1โ(3 + 2))) |
36 | 18, 34, 35 | mp2an 691 |
. . . . . . 7
โข
(-1โ(3 โ 2)) = (-1โ(3 + 2)) |
37 | 36 | eqcomi 2746 |
. . . . . 6
โข
(-1โ(3 + 2)) = (-1โ(3 โ 2)) |
38 | | 2cn 12235 |
. . . . . . . . 9
โข 2 โ
โ |
39 | | ax-1cn 11116 |
. . . . . . . . 9
โข 1 โ
โ |
40 | | 2p1e3 12302 |
. . . . . . . . 9
โข (2 + 1) =
3 |
41 | 11, 38, 39, 40 | subaddrii 11497 |
. . . . . . . 8
โข (3
โ 2) = 1 |
42 | 41 | oveq2i 7373 |
. . . . . . 7
โข
(-1โ(3 โ 2)) = (-1โ1) |
43 | | neg1cn 12274 |
. . . . . . . 8
โข -1 โ
โ |
44 | | exp1 13980 |
. . . . . . . 8
โข (-1
โ โ โ (-1โ1) = -1) |
45 | 43, 44 | ax-mp 5 |
. . . . . . 7
โข
(-1โ1) = -1 |
46 | 42, 45 | eqtri 2765 |
. . . . . 6
โข
(-1โ(3 โ 2)) = -1 |
47 | 33, 37, 46 | 3eqtri 2769 |
. . . . 5
โข
(-1โ5) = -1 |
48 | 47 | oveq1i 7372 |
. . . 4
โข
((-1โ5) mod ;41) = (-1
mod ;41) |
49 | 17, 30, 48 | 3eqtri 2769 |
. . 3
โข
((3โ;20) mod ;41) = (-1 mod ;41) |
50 | 1 | oveq2i 7373 |
. . 3
โข
((3โ;20) mod ๐) = ((3โ;20) mod ;41) |
51 | 1 | oveq2i 7373 |
. . 3
โข (-1 mod
๐) = (-1 mod ;41) |
52 | 49, 50, 51 | 3eqtr4i 2775 |
. 2
โข
((3โ;20) mod ๐) = (-1 mod ๐) |
53 | 4, 52 | eqtri 2765 |
1
โข
((3โ((๐ โ
1) / 2)) mod ๐) = (-1 mod
๐) |