Step | Hyp | Ref
| Expression |
1 | | fpprbasnn 46011 |
. 2
โข (๐ โ ( FPPr โ๐) โ ๐ โ โ) |
2 | | fpprel 46010 |
. . 3
โข (๐ โ โ โ (๐ โ ( FPPr โ๐) โ (๐ โ (โคโฅโ4)
โง ๐ โ โ
โง ((๐โ(๐ โ 1)) mod ๐) = 1))) |
3 | | nnz 12528 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
4 | | eluz4nn 12819 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ4) โ ๐ โ โ) |
5 | | nnm1nn0 12462 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ4) โ (๐ โ 1) โ
โ0) |
7 | | zexpcl 13991 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง (๐ โ 1) โ
โ0) โ (๐โ(๐ โ 1)) โ
โค) |
8 | 3, 6, 7 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (๐โ(๐ โ 1)) โ
โค) |
9 | 8 | zred 12615 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (๐โ(๐ โ 1)) โ
โ) |
10 | 4 | nnrpd 12963 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ4) โ ๐ โ
โ+) |
11 | 10 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ๐ โ
โ+) |
12 | 9, 11 | modcld 13789 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐โ(๐ โ 1)) mod ๐) โ โ) |
13 | 12 | recnd 11191 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐โ(๐ โ 1)) mod ๐) โ โ) |
14 | | 1cnd 11158 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ 1 โ โ) |
15 | | nncn 12169 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
16 | 15 | adantr 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ๐ โ โ) |
17 | | nnne0 12195 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
18 | 17 | adantr 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ๐ โ 0) |
19 | 13, 14, 16, 18 | mulcand 11796 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) = (๐ ยท 1) โ ((๐โ(๐ โ 1)) mod ๐) = 1)) |
20 | | oveq1 7368 |
. . . . . . . 8
โข ((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) = (๐ ยท 1) โ ((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) mod ๐) = ((๐ ยท 1) mod ๐)) |
21 | 3 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ๐ โ โค) |
22 | | modmulmodr 13851 |
. . . . . . . . . . 11
โข ((๐ โ โค โง (๐โ(๐ โ 1)) โ โ โง ๐ โ โ+)
โ ((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) mod ๐) = ((๐ ยท (๐โ(๐ โ 1))) mod ๐)) |
23 | 21, 9, 11, 22 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) mod ๐) = ((๐ ยท (๐โ(๐ โ 1))) mod ๐)) |
24 | 23 | eqeq1d 2735 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) mod ๐) = ((๐ ยท 1) mod ๐) โ ((๐ ยท (๐โ(๐ โ 1))) mod ๐) = ((๐ ยท 1) mod ๐))) |
25 | 8 | zcnd 12616 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (๐โ(๐ โ 1)) โ
โ) |
26 | 16, 25 | mulcomd 11184 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (๐ ยท (๐โ(๐ โ 1))) = ((๐โ(๐ โ 1)) ยท ๐)) |
27 | | expm1t 14005 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ๐) = ((๐โ(๐ โ 1)) ยท ๐)) |
28 | 27 | eqcomd 2739 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ ((๐โ(๐ โ 1)) ยท ๐) = (๐โ๐)) |
29 | 15, 4, 28 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐โ(๐ โ 1)) ยท ๐) = (๐โ๐)) |
30 | 26, 29 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (๐ ยท (๐โ(๐ โ 1))) = (๐โ๐)) |
31 | 30 | oveq1d 7376 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐ ยท (๐โ(๐ โ 1))) mod ๐) = ((๐โ๐) mod ๐)) |
32 | 15 | mulid1d 11180 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
33 | 32 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (๐ ยท 1) = ๐) |
34 | 33 | oveq1d 7376 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐ ยท 1) mod ๐) = (๐ mod ๐)) |
35 | 31, 34 | eqeq12d 2749 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (((๐ ยท (๐โ(๐ โ 1))) mod ๐) = ((๐ ยท 1) mod ๐) โ ((๐โ๐) mod ๐) = (๐ mod ๐))) |
36 | 35 | biimpd 228 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (((๐ ยท (๐โ(๐ โ 1))) mod ๐) = ((๐ ยท 1) mod ๐) โ ((๐โ๐) mod ๐) = (๐ mod ๐))) |
37 | 24, 36 | sylbid 239 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) mod ๐) = ((๐ ยท 1) mod ๐) โ ((๐โ๐) mod ๐) = (๐ mod ๐))) |
38 | 20, 37 | syl5 34 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ ((๐ ยท ((๐โ(๐ โ 1)) mod ๐)) = (๐ ยท 1) โ ((๐โ๐) mod ๐) = (๐ mod ๐))) |
39 | 19, 38 | sylbird 260 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (((๐โ(๐ โ 1)) mod ๐) = 1 โ ((๐โ๐) mod ๐) = (๐ mod ๐))) |
40 | 39 | a1d 25 |
. . . . 5
โข ((๐ โ โ โง ๐ โ
(โคโฅโ4)) โ (๐ โ โ โ (((๐โ(๐ โ 1)) mod ๐) = 1 โ ((๐โ๐) mod ๐) = (๐ mod ๐)))) |
41 | 40 | ex 414 |
. . . 4
โข (๐ โ โ โ (๐ โ
(โคโฅโ4) โ (๐ โ โ โ (((๐โ(๐ โ 1)) mod ๐) = 1 โ ((๐โ๐) mod ๐) = (๐ mod ๐))))) |
42 | 41 | 3impd 1349 |
. . 3
โข (๐ โ โ โ ((๐ โ
(โคโฅโ4) โง ๐ โ โ โง ((๐โ(๐ โ 1)) mod ๐) = 1) โ ((๐โ๐) mod ๐) = (๐ mod ๐))) |
43 | 2, 42 | sylbid 239 |
. 2
โข (๐ โ โ โ (๐ โ ( FPPr โ๐) โ ((๐โ๐) mod ๐) = (๐ mod ๐))) |
44 | 1, 43 | mpcom 38 |
1
โข (๐ โ ( FPPr โ๐) โ ((๐โ๐) mod ๐) = (๐ mod ๐)) |