Step | Hyp | Ref
| Expression |
1 | | fz1ssfz0 13544 |
. . 3
โข
(1...(๐ โ 1))
โ (0...(๐ โ
1)) |
2 | | simpr 486 |
. . 3
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ด โ (1...(๐ โ 1))) |
3 | 1, 2 | sselid 3947 |
. 2
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ด โ (0...(๐ โ 1))) |
4 | | simpl 484 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ โ โ) |
5 | | elfznn 13477 |
. . . . . . 7
โข (๐ด โ (1...(๐ โ 1)) โ ๐ด โ โ) |
6 | 5 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ด โ โ) |
7 | 6 | nnzd 12533 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ด โ โค) |
8 | | prmnn 16557 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
9 | | fzm1ndvds 16211 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐ด) |
10 | 8, 9 | sylan 581 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐ด) |
11 | | prmdiv.1 |
. . . . . 6
โข ๐
= ((๐ดโ(๐ โ 2)) mod ๐) |
12 | 11 | prmdiv 16664 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โ (๐
โ (1...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐
) โ 1))) |
13 | 4, 7, 10, 12 | syl3anc 1372 |
. . . 4
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ (๐
โ (1...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐
) โ 1))) |
14 | 13 | simprd 497 |
. . 3
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ โฅ ((๐ด ยท ๐
) โ 1)) |
15 | 6 | nncnd 12176 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ด โ โ) |
16 | 13 | simpld 496 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐
โ (1...(๐ โ 1))) |
17 | | elfznn 13477 |
. . . . . . 7
โข (๐
โ (1...(๐ โ 1)) โ ๐
โ โ) |
18 | 16, 17 | syl 17 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐
โ โ) |
19 | 18 | nncnd 12176 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐
โ โ) |
20 | 15, 19 | mulcomd 11183 |
. . . 4
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ (๐ด ยท ๐
) = (๐
ยท ๐ด)) |
21 | 20 | oveq1d 7377 |
. . 3
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ((๐ด ยท ๐
) โ 1) = ((๐
ยท ๐ด) โ 1)) |
22 | 14, 21 | breqtrd 5136 |
. 2
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ โฅ ((๐
ยท ๐ด) โ 1)) |
23 | 16 | elfzelzd 13449 |
. . 3
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐
โ โค) |
24 | | fzm1ndvds 16211 |
. . . 4
โข ((๐ โ โ โง ๐
โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐
) |
25 | 8, 16, 24 | syl2an2r 684 |
. . 3
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐
) |
26 | | eqid 2737 |
. . . 4
โข ((๐
โ(๐ โ 2)) mod ๐) = ((๐
โ(๐ โ 2)) mod ๐) |
27 | 26 | prmdiveq 16665 |
. . 3
โข ((๐ โ โ โง ๐
โ โค โง ยฌ
๐ โฅ ๐
) โ ((๐ด โ (0...(๐ โ 1)) โง ๐ โฅ ((๐
ยท ๐ด) โ 1)) โ ๐ด = ((๐
โ(๐ โ 2)) mod ๐))) |
28 | 4, 23, 25, 27 | syl3anc 1372 |
. 2
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ((๐ด โ (0...(๐ โ 1)) โง ๐ โฅ ((๐
ยท ๐ด) โ 1)) โ ๐ด = ((๐
โ(๐ โ 2)) mod ๐))) |
29 | 3, 22, 28 | mpbi2and 711 |
1
โข ((๐ โ โ โง ๐ด โ (1...(๐ โ 1))) โ ๐ด = ((๐
โ(๐ โ 2)) mod ๐)) |