Step | Hyp | Ref
| Expression |
1 | | prmnn 12109 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ) |
2 | | dvdsmodexp 11801 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐ด) โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)) |
3 | 2 | 3exp 1202 |
. . . 4
โข (๐ โ โ โ (๐ โ โ โ (๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)))) |
4 | 1, 1, 3 | sylc 62 |
. . 3
โข (๐ โ โ โ (๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
5 | 4 | adantr 276 |
. 2
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
6 | | coprm 12143 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค) โ (ยฌ
๐ โฅ ๐ด โ (๐ gcd ๐ด) = 1)) |
7 | | prmz 12110 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
8 | | gcdcom 11973 |
. . . . . 6
โข ((๐ โ โค โง ๐ด โ โค) โ (๐ gcd ๐ด) = (๐ด gcd ๐)) |
9 | 7, 8 | sylan 283 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ gcd ๐ด) = (๐ด gcd ๐)) |
10 | 9 | eqeq1d 2186 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค) โ ((๐ gcd ๐ด) = 1 โ (๐ด gcd ๐) = 1)) |
11 | 6, 10 | bitrd 188 |
. . 3
โข ((๐ โ โ โง ๐ด โ โค) โ (ยฌ
๐ โฅ ๐ด โ (๐ด gcd ๐) = 1)) |
12 | | simp2 998 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ด โ โค) |
13 | 1 | 3ad2ant1 1018 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ โ โ) |
14 | 13 | phicld 12217 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (ฯโ๐) โ
โ) |
15 | 14 | nnnn0d 9228 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (ฯโ๐) โ
โ0) |
16 | | zexpcl 10534 |
. . . . . . . 8
โข ((๐ด โ โค โง
(ฯโ๐) โ
โ0) โ (๐ดโ(ฯโ๐)) โ โค) |
17 | 12, 15, 16 | syl2anc 411 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ(ฯโ๐)) โ โค) |
18 | | zq 9625 |
. . . . . . 7
โข ((๐ดโ(ฯโ๐)) โ โค โ (๐ดโ(ฯโ๐)) โ
โ) |
19 | 17, 18 | syl 14 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ(ฯโ๐)) โ โ) |
20 | | 1z 9278 |
. . . . . . 7
โข 1 โ
โค |
21 | | zq 9625 |
. . . . . . 7
โข (1 โ
โค โ 1 โ โ) |
22 | 20, 21 | mp1i 10 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ 1 โ
โ) |
23 | | nnq 9632 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
24 | 13, 23 | syl 14 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ โ โ) |
25 | 13 | nngt0d 8962 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ 0 < ๐) |
26 | | eulerth 12232 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐)) |
27 | 1, 26 | syl3an1 1271 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐)) |
28 | 19, 22, 12, 24, 25, 27 | modqmul1 10376 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (((๐ดโ(ฯโ๐)) ยท ๐ด) mod ๐) = ((1 ยท ๐ด) mod ๐)) |
29 | | phiprm 12222 |
. . . . . . . . . 10
โข (๐ โ โ โ
(ฯโ๐) = (๐ โ 1)) |
30 | 29 | 3ad2ant1 1018 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (ฯโ๐) = (๐ โ 1)) |
31 | 30 | oveq2d 5890 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ(ฯโ๐)) = (๐ดโ(๐ โ 1))) |
32 | 31 | oveq1d 5889 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) ยท ๐ด) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
33 | 12 | zcnd 9375 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ๐ด โ โ) |
34 | | expm1t 10547 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ๐) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
35 | 33, 13, 34 | syl2anc 411 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (๐ดโ๐) = ((๐ดโ(๐ โ 1)) ยท ๐ด)) |
36 | 32, 35 | eqtr4d 2213 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ(ฯโ๐)) ยท ๐ด) = (๐ดโ๐)) |
37 | 36 | oveq1d 5889 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (((๐ดโ(ฯโ๐)) ยท ๐ด) mod ๐) = ((๐ดโ๐) mod ๐)) |
38 | 33 | mulid2d 7975 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ (1 ยท ๐ด) = ๐ด) |
39 | 38 | oveq1d 5889 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((1 ยท ๐ด) mod ๐) = (๐ด mod ๐)) |
40 | 28, 37, 39 | 3eqtr3d 2218 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)) |
41 | 40 | 3expia 1205 |
. . 3
โข ((๐ โ โ โง ๐ด โ โค) โ ((๐ด gcd ๐) = 1 โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
42 | 11, 41 | sylbid 150 |
. 2
โข ((๐ โ โ โง ๐ด โ โค) โ (ยฌ
๐ โฅ ๐ด โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐))) |
43 | | dvdsdc 11804 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค) โ
DECID ๐
โฅ ๐ด) |
44 | 1, 43 | sylan 283 |
. . 3
โข ((๐ โ โ โง ๐ด โ โค) โ
DECID ๐
โฅ ๐ด) |
45 | | exmiddc 836 |
. . 3
โข
(DECID ๐ โฅ ๐ด โ (๐ โฅ ๐ด โจ ยฌ ๐ โฅ ๐ด)) |
46 | 44, 45 | syl 14 |
. 2
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ ๐ด โจ ยฌ ๐ โฅ ๐ด)) |
47 | 5, 42, 46 | mpjaod 718 |
1
โข ((๐ โ โ โง ๐ด โ โค) โ ((๐ดโ๐) mod ๐) = (๐ด mod ๐)) |