Step | Hyp | Ref
| Expression |
1 | | prmnn 16557 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ) |
2 | | dvdsmodexp 16151 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐ด) โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)) |
3 | 2 | 3exp 1120 |
. . . 4
โข (๐ โ โ โ (๐ โ โ โ (๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)))) |
4 | 1, 1, 3 | sylc 65 |
. . 3
โข (๐ โ โ โ (๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
5 | 4 | adantr 482 |
. 2
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
6 | | coprm 16594 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค) โ (ยฌ
๐ โฅ ๐ด โ (๐ gcd ๐ด) = 1)) |
7 | | prmz 16558 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
8 | | gcdcom 16400 |
. . . . . 6
โข ((๐ โ โค โง ๐ด โ โค) โ (๐ gcd ๐ด) = (๐ด gcd ๐)) |
9 | 7, 8 | sylan 581 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ gcd ๐ด) = (๐ด gcd ๐)) |
10 | 9 | eqeq1d 2739 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค) โ ((๐ gcd ๐ด) = 1 โ (๐ด gcd ๐) = 1)) |
11 | 6, 10 | bitrd 279 |
. . 3
โข ((๐ โ โ โง ๐ด โ โค) โ (ยฌ
๐ โฅ ๐ด โ (๐ด gcd ๐) = 1)) |
12 | | simp2 1138 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ด โ โค) |
13 | 1 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ โ โ) |
14 | 13 | phicld 16651 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (ฯโ๐) โ
โ) |
15 | 14 | nnnn0d 12480 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (ฯโ๐) โ
โ0) |
16 | | zexpcl 13989 |
. . . . . . . 8
โข ((๐ด โ โค โง
(ฯโ๐) โ
โ0) โ (๐ดโ(ฯโ๐)) โ โค) |
17 | 12, 15, 16 | syl2anc 585 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ(ฯโ๐)) โ โค) |
18 | 17 | zred 12614 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ(ฯโ๐)) โ โ) |
19 | | 1red 11163 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ 1 โ
โ) |
20 | 13 | nnrpd 12962 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ โ
โ+) |
21 | | eulerth 16662 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐)) |
22 | 1, 21 | syl3an1 1164 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐)) |
23 | | modmul1 13836 |
. . . . . 6
โข ((((๐ดโ(ฯโ๐)) โ โ โง 1 โ
โ) โง (๐ด โ
โค โง ๐ โ
โ+) โง ((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐)) โ (((๐ดโ(ฯโ๐)) ยท ๐ด) mod ๐) = ((1 ยท ๐ด) mod ๐)) |
24 | 18, 19, 12, 20, 22, 23 | syl221anc 1382 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (((๐ดโ(ฯโ๐)) ยท ๐ด) mod ๐) = ((1 ยท ๐ด) mod ๐)) |
25 | | phiprm 16656 |
. . . . . . . . . 10
โข (๐ โ โ โ
(ฯโ๐) = (๐ โ 1)) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (ฯโ๐) = (๐ โ 1)) |
27 | 26 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ(ฯโ๐)) = (๐ดโ(๐ โ 1))) |
28 | 27 | oveq1d 7377 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) ยท ๐ด) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
29 | 12 | zcnd 12615 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ด โ โ) |
30 | | expm1t 14003 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ๐) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
31 | 29, 13, 30 | syl2anc 585 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ๐) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
32 | 28, 31 | eqtr4d 2780 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) ยท ๐ด) = (๐ดโ๐)) |
33 | 32 | oveq1d 7377 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (((๐ดโ(ฯโ๐)) ยท ๐ด) mod ๐) = ((๐ดโ๐) mod ๐)) |
34 | 29 | mulid2d 11180 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (1 ยท ๐ด) = ๐ด) |
35 | 34 | oveq1d 7377 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((1 ยท ๐ด) mod ๐) = (๐ด mod ๐)) |
36 | 24, 33, 35 | 3eqtr3d 2785 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)) |
37 | 36 | 3expia 1122 |
. . 3
โข ((๐ โ โ โง ๐ด โ โค) โ ((๐ด gcd ๐) = 1 โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
38 | 11, 37 | sylbid 239 |
. 2
โข ((๐ โ โ โง ๐ด โ โค) โ (ยฌ
๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
39 | 5, 38 | pm2.61d 179 |
1
โข ((๐ โ โ โง ๐ด โ โค) โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)) |