Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . . 7
โข (๐ โ (๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1)) |
2 | 1 | simp2d 1144 |
. . . . . 6
โข (๐ โ ๐ด โ โค) |
3 | 2 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โค) |
4 | | eulerth.4 |
. . . . . . . . . 10
โข (๐ โ ๐น:๐โ1-1-ontoโ๐) |
5 | | f1of 6789 |
. . . . . . . . . 10
โข (๐น:๐โ1-1-ontoโ๐ โ ๐น:๐โถ๐) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐น:๐โถ๐) |
7 | 6 | ffvelcdmda 7040 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ๐ฅ) โ ๐) |
8 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ฆ = (๐นโ๐ฅ) โ (๐ฆ gcd ๐) = ((๐นโ๐ฅ) gcd ๐)) |
9 | 8 | eqeq1d 2739 |
. . . . . . . . 9
โข (๐ฆ = (๐นโ๐ฅ) โ ((๐ฆ gcd ๐) = 1 โ ((๐นโ๐ฅ) gcd ๐) = 1)) |
10 | | eulerth.2 |
. . . . . . . . 9
โข ๐ = {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} |
11 | 9, 10 | elrab2 3653 |
. . . . . . . 8
โข ((๐นโ๐ฅ) โ ๐ โ ((๐นโ๐ฅ) โ (0..^๐) โง ((๐นโ๐ฅ) gcd ๐) = 1)) |
12 | 7, 11 | sylib 217 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ๐ฅ) โ (0..^๐) โง ((๐นโ๐ฅ) gcd ๐) = 1)) |
13 | 12 | simpld 496 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ๐ฅ) โ (0..^๐)) |
14 | | elfzoelz 13579 |
. . . . . 6
โข ((๐นโ๐ฅ) โ (0..^๐) โ (๐นโ๐ฅ) โ โค) |
15 | 13, 14 | syl 17 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ๐ฅ) โ โค) |
16 | 3, 15 | zmulcld 12620 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ (๐ด ยท (๐นโ๐ฅ)) โ โค) |
17 | 1 | simp1d 1143 |
. . . . 5
โข (๐ โ ๐ โ โ) |
18 | 17 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ๐ โ โ) |
19 | | zmodfzo 13806 |
. . . 4
โข (((๐ด ยท (๐นโ๐ฅ)) โ โค โง ๐ โ โ) โ ((๐ด ยท (๐นโ๐ฅ)) mod ๐) โ (0..^๐)) |
20 | 16, 18, 19 | syl2anc 585 |
. . 3
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ด ยท (๐นโ๐ฅ)) mod ๐) โ (0..^๐)) |
21 | | modgcd 16420 |
. . . . 5
โข (((๐ด ยท (๐นโ๐ฅ)) โ โค โง ๐ โ โ) โ (((๐ด ยท (๐นโ๐ฅ)) mod ๐) gcd ๐) = ((๐ด ยท (๐นโ๐ฅ)) gcd ๐)) |
22 | 16, 18, 21 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ (((๐ด ยท (๐นโ๐ฅ)) mod ๐) gcd ๐) = ((๐ด ยท (๐นโ๐ฅ)) gcd ๐)) |
23 | 17 | nnzd 12533 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
24 | 23 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ ๐ โ โค) |
25 | 16, 24 | gcdcomd 16401 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ด ยท (๐นโ๐ฅ)) gcd ๐) = (๐ gcd (๐ด ยท (๐นโ๐ฅ)))) |
26 | 23, 2 | gcdcomd 16401 |
. . . . . . 7
โข (๐ โ (๐ gcd ๐ด) = (๐ด gcd ๐)) |
27 | 1 | simp3d 1145 |
. . . . . . 7
โข (๐ โ (๐ด gcd ๐) = 1) |
28 | 26, 27 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (๐ gcd ๐ด) = 1) |
29 | 28 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (๐ gcd ๐ด) = 1) |
30 | 24, 15 | gcdcomd 16401 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (๐ gcd (๐นโ๐ฅ)) = ((๐นโ๐ฅ) gcd ๐)) |
31 | 12 | simprd 497 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ๐ฅ) gcd ๐) = 1) |
32 | 30, 31 | eqtrd 2777 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (๐ gcd (๐นโ๐ฅ)) = 1) |
33 | | rpmul 16542 |
. . . . . 6
โข ((๐ โ โค โง ๐ด โ โค โง (๐นโ๐ฅ) โ โค) โ (((๐ gcd ๐ด) = 1 โง (๐ gcd (๐นโ๐ฅ)) = 1) โ (๐ gcd (๐ด ยท (๐นโ๐ฅ))) = 1)) |
34 | 24, 3, 15, 33 | syl3anc 1372 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (((๐ gcd ๐ด) = 1 โง (๐ gcd (๐นโ๐ฅ)) = 1) โ (๐ gcd (๐ด ยท (๐นโ๐ฅ))) = 1)) |
35 | 29, 32, 34 | mp2and 698 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ (๐ gcd (๐ด ยท (๐นโ๐ฅ))) = 1) |
36 | 22, 25, 35 | 3eqtrd 2781 |
. . 3
โข ((๐ โง ๐ฅ โ ๐) โ (((๐ด ยท (๐นโ๐ฅ)) mod ๐) gcd ๐) = 1) |
37 | | oveq1 7369 |
. . . . 5
โข (๐ฆ = ((๐ด ยท (๐นโ๐ฅ)) mod ๐) โ (๐ฆ gcd ๐) = (((๐ด ยท (๐นโ๐ฅ)) mod ๐) gcd ๐)) |
38 | 37 | eqeq1d 2739 |
. . . 4
โข (๐ฆ = ((๐ด ยท (๐นโ๐ฅ)) mod ๐) โ ((๐ฆ gcd ๐) = 1 โ (((๐ด ยท (๐นโ๐ฅ)) mod ๐) gcd ๐) = 1)) |
39 | 38, 10 | elrab2 3653 |
. . 3
โข (((๐ด ยท (๐นโ๐ฅ)) mod ๐) โ ๐ โ (((๐ด ยท (๐นโ๐ฅ)) mod ๐) โ (0..^๐) โง (((๐ด ยท (๐นโ๐ฅ)) mod ๐) gcd ๐) = 1)) |
40 | 20, 36, 39 | sylanbrc 584 |
. 2
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ด ยท (๐นโ๐ฅ)) mod ๐) โ ๐) |
41 | | eulerth.5 |
. 2
โข ๐บ = (๐ฅ โ ๐ โฆ ((๐ด ยท (๐นโ๐ฅ)) mod ๐)) |
42 | 40, 41 | fmptd 7067 |
1
โข (๐ โ ๐บ:๐โถ๐) |