Step | Hyp | Ref
| Expression |
1 | | eulerth.4 |
. . . 4
โข (๐ โ ๐น:(1...(ฯโ๐))โ1-1-ontoโ๐) |
2 | | f1ocnv 5466 |
. . . 4
โข (๐น:(1...(ฯโ๐))โ1-1-ontoโ๐ โ โก๐น:๐โ1-1-ontoโ(1...(ฯโ๐))) |
3 | 1, 2 | syl 14 |
. . 3
โข (๐ โ โก๐น:๐โ1-1-ontoโ(1...(ฯโ๐))) |
4 | | eulerth.1 |
. . . . . . 7
โข (๐ โ (๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1)) |
5 | | eulerth.2 |
. . . . . . 7
โข ๐ = {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} |
6 | | eqid 2175 |
. . . . . . 7
โข
(1...(ฯโ๐)) = (1...(ฯโ๐)) |
7 | | fveq2 5507 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
8 | 7 | oveq2d 5881 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ด ยท (๐นโ๐)) = (๐ด ยท (๐นโ๐))) |
9 | 8 | oveq1d 5880 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ด ยท (๐นโ๐)) mod ๐) = ((๐ด ยท (๐นโ๐)) mod ๐)) |
10 | 9 | cbvmptv 4094 |
. . . . . . 7
โข (๐ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐)) mod ๐)) = (๐ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐)) mod ๐)) |
11 | 4, 5, 6, 1, 10 | eulerthlem1 12194 |
. . . . . 6
โข (๐ โ (๐ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐)) mod ๐)):(1...(ฯโ๐))โถ๐) |
12 | | fveq2 5507 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (๐นโ๐) = (๐นโ๐ฆ)) |
13 | 12 | oveq2d 5881 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ (๐ด ยท (๐นโ๐)) = (๐ด ยท (๐นโ๐ฆ))) |
14 | 13 | oveq1d 5880 |
. . . . . . . 8
โข (๐ = ๐ฆ โ ((๐ด ยท (๐นโ๐)) mod ๐) = ((๐ด ยท (๐นโ๐ฆ)) mod ๐)) |
15 | 14 | cbvmptv 4094 |
. . . . . . 7
โข (๐ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐)) mod ๐)) = (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)) |
16 | 15 | feq1i 5350 |
. . . . . 6
โข ((๐ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐)) mod ๐)):(1...(ฯโ๐))โถ๐ โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โถ๐) |
17 | 11, 16 | sylib 122 |
. . . . 5
โข (๐ โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โถ๐) |
18 | 4 | simp1d 1009 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
19 | 18 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐ โ โ) |
20 | 4 | simp2d 1010 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โค) |
21 | 20 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐ด โ โค) |
22 | | ssrab2 3238 |
. . . . . . . . . . . . 13
โข {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ (0..^๐) |
23 | 5, 22 | eqsstri 3185 |
. . . . . . . . . . . 12
โข ๐ โ (0..^๐) |
24 | | fzo0ssnn0 10185 |
. . . . . . . . . . . . 13
โข
(0..^๐) โ
โ0 |
25 | | nn0ssz 9244 |
. . . . . . . . . . . . 13
โข
โ0 โ โค |
26 | 24, 25 | sstri 3162 |
. . . . . . . . . . . 12
โข
(0..^๐) โ
โค |
27 | 23, 26 | sstri 3162 |
. . . . . . . . . . 11
โข ๐ โ
โค |
28 | | f1of 5453 |
. . . . . . . . . . . . . 14
โข (๐น:(1...(ฯโ๐))โ1-1-ontoโ๐ โ ๐น:(1...(ฯโ๐))โถ๐) |
29 | 1, 28 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ ๐น:(1...(ฯโ๐))โถ๐) |
30 | 29 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐น:(1...(ฯโ๐))โถ๐) |
31 | | simprl 529 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐ข โ (1...(ฯโ๐))) |
32 | 30, 31 | ffvelcdmd 5644 |
. . . . . . . . . . 11
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ข) โ ๐) |
33 | 27, 32 | sselid 3151 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ข) โ โค) |
34 | 21, 33 | zmulcld 9354 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐ด ยท (๐นโ๐ข)) โ โค) |
35 | 29 | ffvelcdmda 5643 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฃ โ (1...(ฯโ๐))) โ (๐นโ๐ฃ) โ ๐) |
36 | 35 | adantrl 478 |
. . . . . . . . . . 11
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ฃ) โ ๐) |
37 | 27, 36 | sselid 3151 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ฃ) โ โค) |
38 | 21, 37 | zmulcld 9354 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐ด ยท (๐นโ๐ฃ)) โ โค) |
39 | | moddvds 11774 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ด ยท (๐นโ๐ข)) โ โค โง (๐ด ยท (๐นโ๐ฃ)) โ โค) โ (((๐ด ยท (๐นโ๐ข)) mod ๐) = ((๐ด ยท (๐นโ๐ฃ)) mod ๐) โ ๐ โฅ ((๐ด ยท (๐นโ๐ข)) โ (๐ด ยท (๐นโ๐ฃ))))) |
40 | 19, 34, 38, 39 | syl3anc 1238 |
. . . . . . . 8
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (((๐ด ยท (๐นโ๐ข)) mod ๐) = ((๐ด ยท (๐นโ๐ฃ)) mod ๐) โ ๐ โฅ ((๐ด ยท (๐นโ๐ข)) โ (๐ด ยท (๐นโ๐ฃ))))) |
41 | | eqid 2175 |
. . . . . . . . . 10
โข (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)) = (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)) |
42 | | fveq2 5507 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ข โ (๐นโ๐ฆ) = (๐นโ๐ข)) |
43 | 42 | oveq2d 5881 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ข โ (๐ด ยท (๐นโ๐ฆ)) = (๐ด ยท (๐นโ๐ข))) |
44 | 43 | oveq1d 5880 |
. . . . . . . . . 10
โข (๐ฆ = ๐ข โ ((๐ด ยท (๐นโ๐ฆ)) mod ๐) = ((๐ด ยท (๐นโ๐ข)) mod ๐)) |
45 | | zmodfzo 10317 |
. . . . . . . . . . 11
โข (((๐ด ยท (๐นโ๐ข)) โ โค โง ๐ โ โ) โ ((๐ด ยท (๐นโ๐ข)) mod ๐) โ (0..^๐)) |
46 | 34, 19, 45 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐ด ยท (๐นโ๐ข)) mod ๐) โ (0..^๐)) |
47 | 41, 44, 31, 46 | fvmptd3 5601 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ข) = ((๐ด ยท (๐นโ๐ข)) mod ๐)) |
48 | | fveq2 5507 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ฃ โ (๐นโ๐ฆ) = (๐นโ๐ฃ)) |
49 | 48 | oveq2d 5881 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ฃ โ (๐ด ยท (๐นโ๐ฆ)) = (๐ด ยท (๐นโ๐ฃ))) |
50 | 49 | oveq1d 5880 |
. . . . . . . . . 10
โข (๐ฆ = ๐ฃ โ ((๐ด ยท (๐นโ๐ฆ)) mod ๐) = ((๐ด ยท (๐นโ๐ฃ)) mod ๐)) |
51 | | simprr 531 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐ฃ โ (1...(ฯโ๐))) |
52 | | zmodfzo 10317 |
. . . . . . . . . . 11
โข (((๐ด ยท (๐นโ๐ฃ)) โ โค โง ๐ โ โ) โ ((๐ด ยท (๐นโ๐ฃ)) mod ๐) โ (0..^๐)) |
53 | 38, 19, 52 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐ด ยท (๐นโ๐ฃ)) mod ๐) โ (0..^๐)) |
54 | 41, 50, 51, 53 | fvmptd3 5601 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ฃ) = ((๐ด ยท (๐นโ๐ฃ)) mod ๐)) |
55 | 47, 54 | eqeq12d 2190 |
. . . . . . . 8
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ข) = ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ฃ) โ ((๐ด ยท (๐นโ๐ข)) mod ๐) = ((๐ด ยท (๐นโ๐ฃ)) mod ๐))) |
56 | 21 | zcnd 9349 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐ด โ โ) |
57 | 33 | zcnd 9349 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ข) โ โ) |
58 | 37 | zcnd 9349 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ฃ) โ โ) |
59 | 56, 57, 58 | subdid 8345 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐ด ยท ((๐นโ๐ข) โ (๐นโ๐ฃ))) = ((๐ด ยท (๐นโ๐ข)) โ (๐ด ยท (๐นโ๐ฃ)))) |
60 | 59 | breq2d 4010 |
. . . . . . . 8
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐ โฅ (๐ด ยท ((๐นโ๐ข) โ (๐นโ๐ฃ))) โ ๐ โฅ ((๐ด ยท (๐นโ๐ข)) โ (๐ด ยท (๐นโ๐ฃ))))) |
61 | 40, 55, 60 | 3bitr4d 220 |
. . . . . . 7
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ข) = ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ฃ) โ ๐ โฅ (๐ด ยท ((๐นโ๐ข) โ (๐นโ๐ฃ))))) |
62 | 18 | nnzd 9347 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
63 | 62, 20 | gcdcomd 11942 |
. . . . . . . . . 10
โข (๐ โ (๐ gcd ๐ด) = (๐ด gcd ๐)) |
64 | 4 | simp3d 1011 |
. . . . . . . . . 10
โข (๐ โ (๐ด gcd ๐) = 1) |
65 | 63, 64 | eqtrd 2208 |
. . . . . . . . 9
โข (๐ โ (๐ gcd ๐ด) = 1) |
66 | 65 | adantr 276 |
. . . . . . . 8
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐ gcd ๐ด) = 1) |
67 | 62 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐ โ โค) |
68 | 33, 37 | zsubcld 9353 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐นโ๐ข) โ (๐นโ๐ฃ)) โ โค) |
69 | | coprmdvds 12059 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ด โ โค โง ((๐นโ๐ข) โ (๐นโ๐ฃ)) โ โค) โ ((๐ โฅ (๐ด ยท ((๐นโ๐ข) โ (๐นโ๐ฃ))) โง (๐ gcd ๐ด) = 1) โ ๐ โฅ ((๐นโ๐ข) โ (๐นโ๐ฃ)))) |
70 | 67, 21, 68, 69 | syl3anc 1238 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐ โฅ (๐ด ยท ((๐นโ๐ข) โ (๐นโ๐ฃ))) โง (๐ gcd ๐ด) = 1) โ ๐ โฅ ((๐นโ๐ข) โ (๐นโ๐ฃ)))) |
71 | | zq 9599 |
. . . . . . . . . . . . 13
โข ((๐นโ๐ข) โ โค โ (๐นโ๐ข) โ โ) |
72 | 33, 71 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ข) โ โ) |
73 | | zq 9599 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
74 | 62, 73 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
75 | 74 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ๐ โ โ) |
76 | 23, 32 | sselid 3151 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ข) โ (0..^๐)) |
77 | | elfzole1 10125 |
. . . . . . . . . . . . 13
โข ((๐นโ๐ข) โ (0..^๐) โ 0 โค (๐นโ๐ข)) |
78 | 76, 77 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ 0 โค (๐นโ๐ข)) |
79 | | elfzolt2 10126 |
. . . . . . . . . . . . 13
โข ((๐นโ๐ข) โ (0..^๐) โ (๐นโ๐ข) < ๐) |
80 | 76, 79 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ข) < ๐) |
81 | | modqid 10319 |
. . . . . . . . . . . 12
โข ((((๐นโ๐ข) โ โ โง ๐ โ โ) โง (0 โค (๐นโ๐ข) โง (๐นโ๐ข) < ๐)) โ ((๐นโ๐ข) mod ๐) = (๐นโ๐ข)) |
82 | 72, 75, 78, 80, 81 | syl22anc 1239 |
. . . . . . . . . . 11
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐นโ๐ข) mod ๐) = (๐นโ๐ข)) |
83 | 27, 35 | sselid 3151 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฃ โ (1...(ฯโ๐))) โ (๐นโ๐ฃ) โ โค) |
84 | 83 | adantrl 478 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ฃ) โ โค) |
85 | | zq 9599 |
. . . . . . . . . . . . 13
โข ((๐นโ๐ฃ) โ โค โ (๐นโ๐ฃ) โ โ) |
86 | 84, 85 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ฃ) โ โ) |
87 | 23, 35 | sselid 3151 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฃ โ (1...(ฯโ๐))) โ (๐นโ๐ฃ) โ (0..^๐)) |
88 | | elfzole1 10125 |
. . . . . . . . . . . . . 14
โข ((๐นโ๐ฃ) โ (0..^๐) โ 0 โค (๐นโ๐ฃ)) |
89 | 87, 88 | syl 14 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฃ โ (1...(ฯโ๐))) โ 0 โค (๐นโ๐ฃ)) |
90 | 89 | adantrl 478 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ 0 โค (๐นโ๐ฃ)) |
91 | 87 | adantrl 478 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ฃ) โ (0..^๐)) |
92 | | elfzolt2 10126 |
. . . . . . . . . . . . 13
โข ((๐นโ๐ฃ) โ (0..^๐) โ (๐นโ๐ฃ) < ๐) |
93 | 91, 92 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐นโ๐ฃ) < ๐) |
94 | | modqid 10319 |
. . . . . . . . . . . 12
โข ((((๐นโ๐ฃ) โ โ โง ๐ โ โ) โง (0 โค (๐นโ๐ฃ) โง (๐นโ๐ฃ) < ๐)) โ ((๐นโ๐ฃ) mod ๐) = (๐นโ๐ฃ)) |
95 | 86, 75, 90, 93, 94 | syl22anc 1239 |
. . . . . . . . . . 11
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐นโ๐ฃ) mod ๐) = (๐นโ๐ฃ)) |
96 | 82, 95 | eqeq12d 2190 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (((๐นโ๐ข) mod ๐) = ((๐นโ๐ฃ) mod ๐) โ (๐นโ๐ข) = (๐นโ๐ฃ))) |
97 | | moddvds 11774 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐นโ๐ข) โ โค โง (๐นโ๐ฃ) โ โค) โ (((๐นโ๐ข) mod ๐) = ((๐นโ๐ฃ) mod ๐) โ ๐ โฅ ((๐นโ๐ข) โ (๐นโ๐ฃ)))) |
98 | 19, 33, 37, 97 | syl3anc 1238 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (((๐นโ๐ข) mod ๐) = ((๐นโ๐ฃ) mod ๐) โ ๐ โฅ ((๐นโ๐ข) โ (๐นโ๐ฃ)))) |
99 | | f1of1 5452 |
. . . . . . . . . . . 12
โข (๐น:(1...(ฯโ๐))โ1-1-ontoโ๐ โ ๐น:(1...(ฯโ๐))โ1-1โ๐) |
100 | 1, 99 | syl 14 |
. . . . . . . . . . 11
โข (๐ โ ๐น:(1...(ฯโ๐))โ1-1โ๐) |
101 | | f1fveq 5763 |
. . . . . . . . . . 11
โข ((๐น:(1...(ฯโ๐))โ1-1โ๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐นโ๐ข) = (๐นโ๐ฃ) โ ๐ข = ๐ฃ)) |
102 | 100, 101 | sylan 283 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐นโ๐ข) = (๐นโ๐ฃ) โ ๐ข = ๐ฃ)) |
103 | 96, 98, 102 | 3bitr3d 218 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐ โฅ ((๐นโ๐ข) โ (๐นโ๐ฃ)) โ ๐ข = ๐ฃ)) |
104 | 70, 103 | sylibd 149 |
. . . . . . . 8
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ ((๐ โฅ (๐ด ยท ((๐นโ๐ข) โ (๐นโ๐ฃ))) โง (๐ gcd ๐ด) = 1) โ ๐ข = ๐ฃ)) |
105 | 66, 104 | mpan2d 428 |
. . . . . . 7
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (๐ โฅ (๐ด ยท ((๐นโ๐ข) โ (๐นโ๐ฃ))) โ ๐ข = ๐ฃ)) |
106 | 61, 105 | sylbid 150 |
. . . . . 6
โข ((๐ โง (๐ข โ (1...(ฯโ๐)) โง ๐ฃ โ (1...(ฯโ๐)))) โ (((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ข) = ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ฃ) โ ๐ข = ๐ฃ)) |
107 | 106 | ralrimivva 2557 |
. . . . 5
โข (๐ โ โ๐ข โ (1...(ฯโ๐))โ๐ฃ โ (1...(ฯโ๐))(((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ข) = ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ฃ) โ ๐ข = ๐ฃ)) |
108 | | dff13 5759 |
. . . . 5
โข ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1โ๐ โ ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โถ๐ โง โ๐ข โ (1...(ฯโ๐))โ๐ฃ โ (1...(ฯโ๐))(((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ข) = ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))โ๐ฃ) โ ๐ข = ๐ฃ))) |
109 | 17, 107, 108 | sylanbrc 417 |
. . . 4
โข (๐ โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1โ๐) |
110 | | 1zzd 9253 |
. . . . . . 7
โข (๐ โ 1 โ
โค) |
111 | 18 | phicld 12185 |
. . . . . . . 8
โข (๐ โ (ฯโ๐) โ
โ) |
112 | 111 | nnzd 9347 |
. . . . . . 7
โข (๐ โ (ฯโ๐) โ
โค) |
113 | 110, 112 | fzfigd 10401 |
. . . . . 6
โข (๐ โ (1...(ฯโ๐)) โ Fin) |
114 | | f1oeng 6747 |
. . . . . 6
โข
(((1...(ฯโ๐)) โ Fin โง ๐น:(1...(ฯโ๐))โ1-1-ontoโ๐) โ
(1...(ฯโ๐))
โ ๐) |
115 | 113, 1, 114 | syl2anc 411 |
. . . . 5
โข (๐ โ (1...(ฯโ๐)) โ ๐) |
116 | 4, 5 | eulerthlemfi 12195 |
. . . . 5
โข (๐ โ ๐ โ Fin) |
117 | | f1finf1o 6936 |
. . . . 5
โข
(((1...(ฯโ๐)) โ ๐ โง ๐ โ Fin) โ ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1โ๐ โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1-ontoโ๐)) |
118 | 115, 116,
117 | syl2anc 411 |
. . . 4
โข (๐ โ ((๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1โ๐ โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1-ontoโ๐)) |
119 | 109, 118 | mpbid 147 |
. . 3
โข (๐ โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1-ontoโ๐) |
120 | | f1oco 5476 |
. . 3
โข ((โก๐น:๐โ1-1-ontoโ(1...(ฯโ๐)) โง (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐)):(1...(ฯโ๐))โ1-1-ontoโ๐) โ (โก๐น โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))):(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐))) |
121 | 3, 119, 120 | syl2anc 411 |
. 2
โข (๐ โ (โก๐น โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))):(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐))) |
122 | | eulerth.h |
. . 3
โข ๐ป = (โก๐น โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))) |
123 | | f1oeq1 5441 |
. . 3
โข (๐ป = (โก๐น โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))) โ (๐ป:(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐)) โ (โก๐น โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))):(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐)))) |
124 | 122, 123 | ax-mp 5 |
. 2
โข (๐ป:(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐)) โ (โก๐น โ (๐ฆ โ (1...(ฯโ๐)) โฆ ((๐ด ยท (๐นโ๐ฆ)) mod ๐))):(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐))) |
125 | 121, 124 | sylibr 134 |
1
โข (๐ โ ๐ป:(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐))) |