Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ โ) |
2 | | prmz 16558 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โค) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ โค) |
4 | | simpl2 1193 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ด โ โค) |
5 | | elfzelz 13448 |
. . . . . . . . . . 11
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โค) |
6 | 5 | ad2antrl 727 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ โค) |
7 | 4, 6 | zmulcld 12620 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ด ยท ๐) โ โค) |
8 | | 1z 12540 |
. . . . . . . . 9
โข 1 โ
โค |
9 | | zsubcl 12552 |
. . . . . . . . 9
โข (((๐ด ยท ๐) โ โค โง 1 โ โค)
โ ((๐ด ยท ๐) โ 1) โ
โค) |
10 | 7, 8, 9 | sylancl 587 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ((๐ด ยท ๐) โ 1) โ
โค) |
11 | | prmdiv.1 |
. . . . . . . . . . . . . 14
โข ๐
= ((๐ดโ(๐ โ 2)) mod ๐) |
12 | 11 | prmdiv 16664 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โ (๐
โ (1...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐
) โ 1))) |
13 | 12 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐
โ (1...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐
) โ 1))) |
14 | 13 | simpld 496 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐
โ (1...(๐ โ 1))) |
15 | | elfzelz 13448 |
. . . . . . . . . . 11
โข (๐
โ (1...(๐ โ 1)) โ ๐
โ โค) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐
โ โค) |
17 | 4, 16 | zmulcld 12620 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ด ยท ๐
) โ โค) |
18 | | zsubcl 12552 |
. . . . . . . . 9
โข (((๐ด ยท ๐
) โ โค โง 1 โ โค)
โ ((๐ด ยท ๐
) โ 1) โ
โค) |
19 | 17, 8, 18 | sylancl 587 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ((๐ด ยท ๐
) โ 1) โ
โค) |
20 | | simprr 772 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โฅ ((๐ด ยท ๐) โ 1)) |
21 | 13 | simprd 497 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โฅ ((๐ด ยท ๐
) โ 1)) |
22 | 3, 10, 19, 20, 21 | dvds2subd 16182 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โฅ (((๐ด ยท ๐) โ 1) โ ((๐ด ยท ๐
) โ 1))) |
23 | 7 | zcnd 12615 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ด ยท ๐) โ โ) |
24 | 17 | zcnd 12615 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ด ยท ๐
) โ โ) |
25 | | 1cnd 11157 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ 1 โ
โ) |
26 | 23, 24, 25 | nnncan2d 11554 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (((๐ด ยท ๐) โ 1) โ ((๐ด ยท ๐
) โ 1)) = ((๐ด ยท ๐) โ (๐ด ยท ๐
))) |
27 | 4 | zcnd 12615 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ด โ โ) |
28 | | elfznn0 13541 |
. . . . . . . . . . . 12
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ
โ0) |
29 | 28 | ad2antrl 727 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ
โ0) |
30 | 29 | nn0red 12481 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ โ) |
31 | 30 | recnd 11190 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ โ) |
32 | 16 | zcnd 12615 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐
โ โ) |
33 | 27, 31, 32 | subdid 11618 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ด ยท (๐ โ ๐
)) = ((๐ด ยท ๐) โ (๐ด ยท ๐
))) |
34 | 26, 33 | eqtr4d 2780 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (((๐ด ยท ๐) โ 1) โ ((๐ด ยท ๐
) โ 1)) = (๐ด ยท (๐ โ ๐
))) |
35 | 22, 34 | breqtrd 5136 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โฅ (๐ด ยท (๐ โ ๐
))) |
36 | | simpl3 1194 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ยฌ ๐ โฅ ๐ด) |
37 | | coprm 16594 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค) โ (ยฌ
๐ โฅ ๐ด โ (๐ gcd ๐ด) = 1)) |
38 | 1, 4, 37 | syl2anc 585 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (ยฌ ๐ โฅ ๐ด โ (๐ gcd ๐ด) = 1)) |
39 | 36, 38 | mpbid 231 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ gcd ๐ด) = 1) |
40 | 6, 16 | zsubcld 12619 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ โ ๐
) โ โค) |
41 | | coprmdvds 16536 |
. . . . . . 7
โข ((๐ โ โค โง ๐ด โ โค โง (๐ โ ๐
) โ โค) โ ((๐ โฅ (๐ด ยท (๐ โ ๐
)) โง (๐ gcd ๐ด) = 1) โ ๐ โฅ (๐ โ ๐
))) |
42 | 3, 4, 40, 41 | syl3anc 1372 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ((๐ โฅ (๐ด ยท (๐ โ ๐
)) โง (๐ gcd ๐ด) = 1) โ ๐ โฅ (๐ โ ๐
))) |
43 | 35, 39, 42 | mp2and 698 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โฅ (๐ โ ๐
)) |
44 | | prmnn 16557 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
45 | 1, 44 | syl 17 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ โ) |
46 | | moddvds 16154 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โค โง ๐
โ โค) โ ((๐ mod ๐) = (๐
mod ๐) โ ๐ โฅ (๐ โ ๐
))) |
47 | 45, 6, 16, 46 | syl3anc 1372 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ((๐ mod ๐) = (๐
mod ๐) โ ๐ โฅ (๐ โ ๐
))) |
48 | 43, 47 | mpbird 257 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ mod ๐) = (๐
mod ๐)) |
49 | 45 | nnrpd 12962 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โ
โ+) |
50 | | elfzle1 13451 |
. . . . . 6
โข (๐ โ (0...(๐ โ 1)) โ 0 โค ๐) |
51 | 50 | ad2antrl 727 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ 0 โค ๐) |
52 | | elfzle2 13452 |
. . . . . . 7
โข (๐ โ (0...(๐ โ 1)) โ ๐ โค (๐ โ 1)) |
53 | 52 | ad2antrl 727 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ โค (๐ โ 1)) |
54 | | zltlem1 12563 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < ๐ โ ๐ โค (๐ โ 1))) |
55 | 6, 3, 54 | syl2anc 585 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ < ๐ โ ๐ โค (๐ โ 1))) |
56 | 53, 55 | mpbird 257 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ < ๐) |
57 | | modid 13808 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ+)
โง (0 โค ๐ โง ๐ < ๐)) โ (๐ mod ๐) = ๐) |
58 | 30, 49, 51, 56, 57 | syl22anc 838 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ mod ๐) = ๐) |
59 | | prmuz2 16579 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
60 | | uznn0sub 12809 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ (๐ โ 2) โ
โ0) |
61 | 1, 59, 60 | 3syl 18 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ โ 2) โ
โ0) |
62 | | zexpcl 13989 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ โ 2) โ
โ0) โ (๐ดโ(๐ โ 2)) โ
โค) |
63 | 4, 61, 62 | syl2anc 585 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ดโ(๐ โ 2)) โ
โค) |
64 | 63 | zred 12614 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐ดโ(๐ โ 2)) โ
โ) |
65 | | modabs2 13817 |
. . . . . 6
โข (((๐ดโ(๐ โ 2)) โ โ โง ๐ โ โ+)
โ (((๐ดโ(๐ โ 2)) mod ๐) mod ๐) = ((๐ดโ(๐ โ 2)) mod ๐)) |
66 | 64, 49, 65 | syl2anc 585 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (((๐ดโ(๐ โ 2)) mod ๐) mod ๐) = ((๐ดโ(๐ โ 2)) mod ๐)) |
67 | 11 | oveq1i 7372 |
. . . . 5
โข (๐
mod ๐) = (((๐ดโ(๐ โ 2)) mod ๐) mod ๐) |
68 | 66, 67, 11 | 3eqtr4g 2802 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ (๐
mod ๐) = ๐
) |
69 | 48, 58, 68 | 3eqtr3d 2785 |
. . 3
โข (((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โง (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1))) โ ๐ = ๐
) |
70 | 69 | ex 414 |
. 2
โข ((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โ ((๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1)) โ ๐ = ๐
)) |
71 | | fz1ssfz0 13544 |
. . . . . 6
โข
(1...(๐ โ 1))
โ (0...(๐ โ
1)) |
72 | 71 | sseli 3945 |
. . . . 5
โข (๐
โ (1...(๐ โ 1)) โ ๐
โ (0...(๐ โ 1))) |
73 | | eleq1 2826 |
. . . . 5
โข (๐ = ๐
โ (๐ โ (0...(๐ โ 1)) โ ๐
โ (0...(๐ โ 1)))) |
74 | 72, 73 | syl5ibr 246 |
. . . 4
โข (๐ = ๐
โ (๐
โ (1...(๐ โ 1)) โ ๐ โ (0...(๐ โ 1)))) |
75 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐
โ (๐ด ยท ๐) = (๐ด ยท ๐
)) |
76 | 75 | oveq1d 7377 |
. . . . . 6
โข (๐ = ๐
โ ((๐ด ยท ๐) โ 1) = ((๐ด ยท ๐
) โ 1)) |
77 | 76 | breq2d 5122 |
. . . . 5
โข (๐ = ๐
โ (๐ โฅ ((๐ด ยท ๐) โ 1) โ ๐ โฅ ((๐ด ยท ๐
) โ 1))) |
78 | 77 | biimprd 248 |
. . . 4
โข (๐ = ๐
โ (๐ โฅ ((๐ด ยท ๐
) โ 1) โ ๐ โฅ ((๐ด ยท ๐) โ 1))) |
79 | 74, 78 | anim12d 610 |
. . 3
โข (๐ = ๐
โ ((๐
โ (1...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐
) โ 1)) โ (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1)))) |
80 | 12, 79 | syl5com 31 |
. 2
โข ((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โ (๐ = ๐
โ (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1)))) |
81 | 70, 80 | impbid 211 |
1
โข ((๐ โ โ โง ๐ด โ โค โง ยฌ
๐ โฅ ๐ด) โ ((๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ด ยท ๐) โ 1)) โ ๐ = ๐
)) |