Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ค โ (๐ฆ gcd (๐ ยท ๐)) = (๐ค gcd (๐ ยท ๐))) |
2 | 1 | eqeq1d 2739 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ค โ ((๐ฆ gcd (๐ ยท ๐)) = 1 โ (๐ค gcd (๐ ยท ๐)) = 1)) |
3 | | phimul.6 |
. . . . . . . . . . . . 13
โข ๐ = {๐ฆ โ ๐ โฃ (๐ฆ gcd (๐ ยท ๐)) = 1} |
4 | 2, 3 | elrab2 3649 |
. . . . . . . . . . . 12
โข (๐ค โ ๐ โ (๐ค โ ๐ โง (๐ค gcd (๐ ยท ๐)) = 1)) |
5 | 4 | simplbi 499 |
. . . . . . . . . . 11
โข (๐ค โ ๐ โ ๐ค โ ๐) |
6 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ค โ (๐ฅ mod ๐) = (๐ค mod ๐)) |
7 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ค โ (๐ฅ mod ๐) = (๐ค mod ๐)) |
8 | 6, 7 | opeq12d 4839 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ค โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ = โจ(๐ค mod ๐), (๐ค mod ๐)โฉ) |
9 | | crth.3 |
. . . . . . . . . . . 12
โข ๐น = (๐ฅ โ ๐ โฆ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ) |
10 | | opex 5422 |
. . . . . . . . . . . 12
โข
โจ(๐ค mod ๐), (๐ค mod ๐)โฉ โ V |
11 | 8, 9, 10 | fvmpt 6949 |
. . . . . . . . . . 11
โข (๐ค โ ๐ โ (๐นโ๐ค) = โจ(๐ค mod ๐), (๐ค mod ๐)โฉ) |
12 | 5, 11 | syl 17 |
. . . . . . . . . 10
โข (๐ค โ ๐ โ (๐นโ๐ค) = โจ(๐ค mod ๐), (๐ค mod ๐)โฉ) |
13 | 12 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ค โ ๐) โ (๐นโ๐ค) = โจ(๐ค mod ๐), (๐ค mod ๐)โฉ) |
14 | | crth.1 |
. . . . . . . . . . . . . . 15
โข ๐ = (0..^(๐ ยท ๐)) |
15 | 5, 14 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
โข (๐ค โ ๐ โ ๐ค โ (0..^(๐ ยท ๐))) |
16 | 15 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ ๐ค โ (0..^(๐ ยท ๐))) |
17 | | elfzoelz 13573 |
. . . . . . . . . . . . 13
โข (๐ค โ (0..^(๐ ยท ๐)) โ ๐ค โ โค) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ ๐ค โ โค) |
19 | | crth.4 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โ โ โง ๐ โ โ โง (๐ gcd ๐) = 1)) |
20 | 19 | simp1d 1143 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
21 | 20 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ ๐ โ โ) |
22 | | zmodfzo 13800 |
. . . . . . . . . . . 12
โข ((๐ค โ โค โง ๐ โ โ) โ (๐ค mod ๐) โ (0..^๐)) |
23 | 18, 21, 22 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ (๐ค mod ๐) โ (0..^๐)) |
24 | | modgcd 16414 |
. . . . . . . . . . . . 13
โข ((๐ค โ โค โง ๐ โ โ) โ ((๐ค mod ๐) gcd ๐) = (๐ค gcd ๐)) |
25 | 18, 21, 24 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ ((๐ค mod ๐) gcd ๐) = (๐ค gcd ๐)) |
26 | 21 | nnzd 12527 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ ๐ โ โค) |
27 | | gcddvds 16384 |
. . . . . . . . . . . . . . . . 17
โข ((๐ค โ โค โง ๐ โ โค) โ ((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ ๐)) |
28 | 18, 26, 27 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ ((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ ๐)) |
29 | 28 | simpld 496 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โฅ ๐ค) |
30 | | nnne0 12188 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ 0) |
31 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ค = 0 โง ๐ = 0) โ ๐ = 0) |
32 | 31 | necon3ai 2969 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 โ ยฌ (๐ค = 0 โง ๐ = 0)) |
33 | 21, 30, 32 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ค โ ๐) โ ยฌ (๐ค = 0 โง ๐ = 0)) |
34 | | gcdn0cl 16383 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ค โ โค โง ๐ โ โค) โง ยฌ
(๐ค = 0 โง ๐ = 0)) โ (๐ค gcd ๐) โ โ) |
35 | 18, 26, 33, 34 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โ โ) |
36 | 35 | nnzd 12527 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โ โค) |
37 | 19 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ โ) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ ๐ โ โ) |
39 | 38 | nnzd 12527 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ ๐ โ โค) |
40 | 28 | simprd 497 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โฅ ๐) |
41 | 36, 26, 39, 40 | dvdsmultr1d 16180 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โฅ (๐ ยท ๐)) |
42 | 21, 38 | nnmulcld 12207 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ (๐ ยท ๐) โ โ) |
43 | 42 | nnzd 12527 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ (๐ ยท ๐) โ โค) |
44 | | nnne0 12188 |
. . . . . . . . . . . . . . . . 17
โข ((๐ ยท ๐) โ โ โ (๐ ยท ๐) โ 0) |
45 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ค = 0 โง (๐ ยท ๐) = 0) โ (๐ ยท ๐) = 0) |
46 | 45 | necon3ai 2969 |
. . . . . . . . . . . . . . . . 17
โข ((๐ ยท ๐) โ 0 โ ยฌ (๐ค = 0 โง (๐ ยท ๐) = 0)) |
47 | 42, 44, 46 | 3syl 18 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ ยฌ (๐ค = 0 โง (๐ ยท ๐) = 0)) |
48 | | dvdslegcd 16385 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค gcd ๐) โ โค โง ๐ค โ โค โง (๐ ยท ๐) โ โค) โง ยฌ (๐ค = 0 โง (๐ ยท ๐) = 0)) โ (((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ (๐ ยท ๐)) โ (๐ค gcd ๐) โค (๐ค gcd (๐ ยท ๐)))) |
49 | 36, 18, 43, 47, 48 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ (๐ ยท ๐)) โ (๐ค gcd ๐) โค (๐ค gcd (๐ ยท ๐)))) |
50 | 29, 41, 49 | mp2and 698 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โค (๐ค gcd (๐ ยท ๐))) |
51 | 4 | simprbi 498 |
. . . . . . . . . . . . . . 15
โข (๐ค โ ๐ โ (๐ค gcd (๐ ยท ๐)) = 1) |
52 | 51 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd (๐ ยท ๐)) = 1) |
53 | 50, 52 | breqtrd 5132 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โค 1) |
54 | | nnle1eq1 12184 |
. . . . . . . . . . . . . 14
โข ((๐ค gcd ๐) โ โ โ ((๐ค gcd ๐) โค 1 โ (๐ค gcd ๐) = 1)) |
55 | 35, 54 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ ((๐ค gcd ๐) โค 1 โ (๐ค gcd ๐) = 1)) |
56 | 53, 55 | mpbid 231 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) = 1) |
57 | 25, 56 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ((๐ค mod ๐) gcd ๐) = 1) |
58 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ฆ = (๐ค mod ๐) โ (๐ฆ gcd ๐) = ((๐ค mod ๐) gcd ๐)) |
59 | 58 | eqeq1d 2739 |
. . . . . . . . . . . 12
โข (๐ฆ = (๐ค mod ๐) โ ((๐ฆ gcd ๐) = 1 โ ((๐ค mod ๐) gcd ๐) = 1)) |
60 | | phimul.4 |
. . . . . . . . . . . 12
โข ๐ = {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} |
61 | 59, 60 | elrab2 3649 |
. . . . . . . . . . 11
โข ((๐ค mod ๐) โ ๐ โ ((๐ค mod ๐) โ (0..^๐) โง ((๐ค mod ๐) gcd ๐) = 1)) |
62 | 23, 57, 61 | sylanbrc 584 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ (๐ค mod ๐) โ ๐) |
63 | | zmodfzo 13800 |
. . . . . . . . . . . 12
โข ((๐ค โ โค โง ๐ โ โ) โ (๐ค mod ๐) โ (0..^๐)) |
64 | 18, 38, 63 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ (๐ค mod ๐) โ (0..^๐)) |
65 | | modgcd 16414 |
. . . . . . . . . . . . 13
โข ((๐ค โ โค โง ๐ โ โ) โ ((๐ค mod ๐) gcd ๐) = (๐ค gcd ๐)) |
66 | 18, 38, 65 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ ((๐ค mod ๐) gcd ๐) = (๐ค gcd ๐)) |
67 | | gcddvds 16384 |
. . . . . . . . . . . . . . . . 17
โข ((๐ค โ โค โง ๐ โ โค) โ ((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ ๐)) |
68 | 18, 39, 67 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ ((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ ๐)) |
69 | 68 | simpld 496 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โฅ ๐ค) |
70 | | nnne0 12188 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ 0) |
71 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ค = 0 โง ๐ = 0) โ ๐ = 0) |
72 | 71 | necon3ai 2969 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 โ ยฌ (๐ค = 0 โง ๐ = 0)) |
73 | 38, 70, 72 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ค โ ๐) โ ยฌ (๐ค = 0 โง ๐ = 0)) |
74 | | gcdn0cl 16383 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ค โ โค โง ๐ โ โค) โง ยฌ
(๐ค = 0 โง ๐ = 0)) โ (๐ค gcd ๐) โ โ) |
75 | 18, 39, 73, 74 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โ โ) |
76 | 75 | nnzd 12527 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โ โค) |
77 | 68 | simprd 497 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โฅ ๐) |
78 | | dvdsmul2 16162 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) |
79 | 26, 39, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐) โ ๐ โฅ (๐ ยท ๐)) |
80 | 76, 39, 43, 77, 79 | dvdstrd 16178 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โฅ (๐ ยท ๐)) |
81 | | dvdslegcd 16385 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค gcd ๐) โ โค โง ๐ค โ โค โง (๐ ยท ๐) โ โค) โง ยฌ (๐ค = 0 โง (๐ ยท ๐) = 0)) โ (((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ (๐ ยท ๐)) โ (๐ค gcd ๐) โค (๐ค gcd (๐ ยท ๐)))) |
82 | 76, 18, 43, 47, 81 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ (((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ (๐ ยท ๐)) โ (๐ค gcd ๐) โค (๐ค gcd (๐ ยท ๐)))) |
83 | 69, 80, 82 | mp2and 698 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โค (๐ค gcd (๐ ยท ๐))) |
84 | 83, 52 | breqtrd 5132 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) โค 1) |
85 | | nnle1eq1 12184 |
. . . . . . . . . . . . . 14
โข ((๐ค gcd ๐) โ โ โ ((๐ค gcd ๐) โค 1 โ (๐ค gcd ๐) = 1)) |
86 | 75, 85 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค โ ๐) โ ((๐ค gcd ๐) โค 1 โ (๐ค gcd ๐) = 1)) |
87 | 84, 86 | mpbid 231 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค โ ๐) โ (๐ค gcd ๐) = 1) |
88 | 66, 87 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ((๐ค mod ๐) gcd ๐) = 1) |
89 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ฆ = (๐ค mod ๐) โ (๐ฆ gcd ๐) = ((๐ค mod ๐) gcd ๐)) |
90 | 89 | eqeq1d 2739 |
. . . . . . . . . . . 12
โข (๐ฆ = (๐ค mod ๐) โ ((๐ฆ gcd ๐) = 1 โ ((๐ค mod ๐) gcd ๐) = 1)) |
91 | | phimul.5 |
. . . . . . . . . . . 12
โข ๐ = {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} |
92 | 90, 91 | elrab2 3649 |
. . . . . . . . . . 11
โข ((๐ค mod ๐) โ ๐ โ ((๐ค mod ๐) โ (0..^๐) โง ((๐ค mod ๐) gcd ๐) = 1)) |
93 | 64, 88, 92 | sylanbrc 584 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ (๐ค mod ๐) โ ๐) |
94 | 62, 93 | opelxpd 5672 |
. . . . . . . . 9
โข ((๐ โง ๐ค โ ๐) โ โจ(๐ค mod ๐), (๐ค mod ๐)โฉ โ (๐ ร ๐)) |
95 | 13, 94 | eqeltrd 2838 |
. . . . . . . 8
โข ((๐ โง ๐ค โ ๐) โ (๐นโ๐ค) โ (๐ ร ๐)) |
96 | 95 | ralrimiva 3144 |
. . . . . . 7
โข (๐ โ โ๐ค โ ๐ (๐นโ๐ค) โ (๐ ร ๐)) |
97 | | crth.2 |
. . . . . . . . . 10
โข ๐ = ((0..^๐) ร (0..^๐)) |
98 | 14, 97, 9, 19 | crth 16651 |
. . . . . . . . 9
โข (๐ โ ๐น:๐โ1-1-ontoโ๐) |
99 | | f1ofn 6786 |
. . . . . . . . 9
โข (๐น:๐โ1-1-ontoโ๐ โ ๐น Fn ๐) |
100 | | fnfun 6603 |
. . . . . . . . 9
โข (๐น Fn ๐ โ Fun ๐น) |
101 | 98, 99, 100 | 3syl 18 |
. . . . . . . 8
โข (๐ โ Fun ๐น) |
102 | 3 | ssrab3 4041 |
. . . . . . . . 9
โข ๐ โ ๐ |
103 | | fndm 6606 |
. . . . . . . . . 10
โข (๐น Fn ๐ โ dom ๐น = ๐) |
104 | 98, 99, 103 | 3syl 18 |
. . . . . . . . 9
โข (๐ โ dom ๐น = ๐) |
105 | 102, 104 | sseqtrrid 3998 |
. . . . . . . 8
โข (๐ โ ๐ โ dom ๐น) |
106 | | funimass4 6908 |
. . . . . . . 8
โข ((Fun
๐น โง ๐ โ dom ๐น) โ ((๐น โ ๐) โ (๐ ร ๐) โ โ๐ค โ ๐ (๐นโ๐ค) โ (๐ ร ๐))) |
107 | 101, 105,
106 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐น โ ๐) โ (๐ ร ๐) โ โ๐ค โ ๐ (๐นโ๐ค) โ (๐ ร ๐))) |
108 | 96, 107 | mpbird 257 |
. . . . . 6
โข (๐ โ (๐น โ ๐) โ (๐ ร ๐)) |
109 | 60 | ssrab3 4041 |
. . . . . . . . . . 11
โข ๐ โ (0..^๐) |
110 | 91 | ssrab3 4041 |
. . . . . . . . . . 11
โข ๐ โ (0..^๐) |
111 | | xpss12 5649 |
. . . . . . . . . . 11
โข ((๐ โ (0..^๐) โง ๐ โ (0..^๐)) โ (๐ ร ๐) โ ((0..^๐) ร (0..^๐))) |
112 | 109, 110,
111 | mp2an 691 |
. . . . . . . . . 10
โข (๐ ร ๐) โ ((0..^๐) ร (0..^๐)) |
113 | 112, 97 | sseqtrri 3982 |
. . . . . . . . 9
โข (๐ ร ๐) โ ๐ |
114 | 113 | sseli 3941 |
. . . . . . . 8
โข (๐ง โ (๐ ร ๐) โ ๐ง โ ๐) |
115 | | f1ocnvfv2 7224 |
. . . . . . . 8
โข ((๐น:๐โ1-1-ontoโ๐ โง ๐ง โ ๐) โ (๐นโ(โก๐นโ๐ง)) = ๐ง) |
116 | 98, 114, 115 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (๐นโ(โก๐นโ๐ง)) = ๐ง) |
117 | | f1ocnv 6797 |
. . . . . . . . . . 11
โข (๐น:๐โ1-1-ontoโ๐ โ โก๐น:๐โ1-1-ontoโ๐) |
118 | | f1of 6785 |
. . . . . . . . . . 11
โข (โก๐น:๐โ1-1-ontoโ๐ โ โก๐น:๐โถ๐) |
119 | 98, 117, 118 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ โก๐น:๐โถ๐) |
120 | | ffvelcdm 7033 |
. . . . . . . . . 10
โข ((โก๐น:๐โถ๐ โง ๐ง โ ๐) โ (โก๐นโ๐ง) โ ๐) |
121 | 119, 114,
120 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (โก๐นโ๐ง) โ ๐) |
122 | 121, 14 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (โก๐นโ๐ง) โ (0..^(๐ ยท ๐))) |
123 | | elfzoelz 13573 |
. . . . . . . . . . . . 13
โข ((โก๐นโ๐ง) โ (0..^(๐ ยท ๐)) โ (โก๐นโ๐ง) โ โค) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (โก๐นโ๐ง) โ โค) |
125 | 20 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ๐ โ โ) |
126 | | modgcd 16414 |
. . . . . . . . . . . 12
โข (((โก๐นโ๐ง) โ โค โง ๐ โ โ) โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = ((โก๐นโ๐ง) gcd ๐)) |
127 | 124, 125,
126 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = ((โก๐นโ๐ง) gcd ๐)) |
128 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ค = (โก๐นโ๐ง) โ (๐ค mod ๐) = ((โก๐นโ๐ง) mod ๐)) |
129 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ค = (โก๐นโ๐ง) โ (๐ค mod ๐) = ((โก๐นโ๐ง) mod ๐)) |
130 | 128, 129 | opeq12d 4839 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ค = (โก๐นโ๐ง) โ โจ(๐ค mod ๐), (๐ค mod ๐)โฉ = โจ((โก๐นโ๐ง) mod ๐), ((โก๐นโ๐ง) mod ๐)โฉ) |
131 | 8 | cbvmptv 5219 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ ๐ โฆ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ) = (๐ค โ ๐ โฆ โจ(๐ค mod ๐), (๐ค mod ๐)โฉ) |
132 | 9, 131 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
โข ๐น = (๐ค โ ๐ โฆ โจ(๐ค mod ๐), (๐ค mod ๐)โฉ) |
133 | | opex 5422 |
. . . . . . . . . . . . . . . . . . 19
โข
โจ((โก๐นโ๐ง) mod ๐), ((โก๐นโ๐ง) mod ๐)โฉ โ V |
134 | 130, 132,
133 | fvmpt 6949 |
. . . . . . . . . . . . . . . . . 18
โข ((โก๐นโ๐ง) โ ๐ โ (๐นโ(โก๐นโ๐ง)) = โจ((โก๐นโ๐ง) mod ๐), ((โก๐นโ๐ง) mod ๐)โฉ) |
135 | 121, 134 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (๐นโ(โก๐นโ๐ง)) = โจ((โก๐นโ๐ง) mod ๐), ((โก๐นโ๐ง) mod ๐)โฉ) |
136 | 116, 135 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ๐ง = โจ((โก๐นโ๐ง) mod ๐), ((โก๐นโ๐ง) mod ๐)โฉ) |
137 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ๐ง โ (๐ ร ๐)) |
138 | 136, 137 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ โจ((โก๐นโ๐ง) mod ๐), ((โก๐นโ๐ง) mod ๐)โฉ โ (๐ ร ๐)) |
139 | | opelxp 5670 |
. . . . . . . . . . . . . . 15
โข
(โจ((โก๐นโ๐ง) mod ๐), ((โก๐นโ๐ง) mod ๐)โฉ โ (๐ ร ๐) โ (((โก๐นโ๐ง) mod ๐) โ ๐ โง ((โก๐นโ๐ง) mod ๐) โ ๐)) |
140 | 138, 139 | sylib 217 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (((โก๐นโ๐ง) mod ๐) โ ๐ โง ((โก๐นโ๐ง) mod ๐) โ ๐)) |
141 | 140 | simpld 496 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ((โก๐นโ๐ง) mod ๐) โ ๐) |
142 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = ((โก๐นโ๐ง) mod ๐) โ (๐ฆ gcd ๐) = (((โก๐นโ๐ง) mod ๐) gcd ๐)) |
143 | 142 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ((โก๐นโ๐ง) mod ๐) โ ((๐ฆ gcd ๐) = 1 โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1)) |
144 | 143, 60 | elrab2 3649 |
. . . . . . . . . . . . 13
โข (((โก๐นโ๐ง) mod ๐) โ ๐ โ (((โก๐นโ๐ง) mod ๐) โ (0..^๐) โง (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1)) |
145 | 141, 144 | sylib 217 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (((โก๐นโ๐ง) mod ๐) โ (0..^๐) โง (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1)) |
146 | 145 | simprd 497 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1) |
147 | 127, 146 | eqtr3d 2779 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ((โก๐นโ๐ง) gcd ๐) = 1) |
148 | 37 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ๐ โ โ) |
149 | | modgcd 16414 |
. . . . . . . . . . . 12
โข (((โก๐นโ๐ง) โ โค โง ๐ โ โ) โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = ((โก๐นโ๐ง) gcd ๐)) |
150 | 124, 148,
149 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = ((โก๐นโ๐ง) gcd ๐)) |
151 | 140 | simprd 497 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ((โก๐นโ๐ง) mod ๐) โ ๐) |
152 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = ((โก๐นโ๐ง) mod ๐) โ (๐ฆ gcd ๐) = (((โก๐นโ๐ง) mod ๐) gcd ๐)) |
153 | 152 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ((โก๐นโ๐ง) mod ๐) โ ((๐ฆ gcd ๐) = 1 โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1)) |
154 | 153, 91 | elrab2 3649 |
. . . . . . . . . . . . 13
โข (((โก๐นโ๐ง) mod ๐) โ ๐ โ (((โก๐นโ๐ง) mod ๐) โ (0..^๐) โง (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1)) |
155 | 151, 154 | sylib 217 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (((โก๐นโ๐ง) mod ๐) โ (0..^๐) โง (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1)) |
156 | 155 | simprd 497 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (((โก๐นโ๐ง) mod ๐) gcd ๐) = 1) |
157 | 150, 156 | eqtr3d 2779 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ((โก๐นโ๐ง) gcd ๐) = 1) |
158 | 20 | nnzd 12527 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
159 | 158 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ๐ โ โค) |
160 | 37 | nnzd 12527 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
161 | 160 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ๐ โ โค) |
162 | | rpmul 16536 |
. . . . . . . . . . 11
โข (((โก๐นโ๐ง) โ โค โง ๐ โ โค โง ๐ โ โค) โ ((((โก๐นโ๐ง) gcd ๐) = 1 โง ((โก๐นโ๐ง) gcd ๐) = 1) โ ((โก๐นโ๐ง) gcd (๐ ยท ๐)) = 1)) |
163 | 124, 159,
161, 162 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ((((โก๐นโ๐ง) gcd ๐) = 1 โง ((โก๐นโ๐ง) gcd ๐) = 1) โ ((โก๐นโ๐ง) gcd (๐ ยท ๐)) = 1)) |
164 | 147, 157,
163 | mp2and 698 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ((โก๐นโ๐ง) gcd (๐ ยท ๐)) = 1) |
165 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ฆ = (โก๐นโ๐ง) โ (๐ฆ gcd (๐ ยท ๐)) = ((โก๐นโ๐ง) gcd (๐ ยท ๐))) |
166 | 165 | eqeq1d 2739 |
. . . . . . . . . 10
โข (๐ฆ = (โก๐นโ๐ง) โ ((๐ฆ gcd (๐ ยท ๐)) = 1 โ ((โก๐นโ๐ง) gcd (๐ ยท ๐)) = 1)) |
167 | 166, 3 | elrab2 3649 |
. . . . . . . . 9
โข ((โก๐นโ๐ง) โ ๐ โ ((โก๐นโ๐ง) โ ๐ โง ((โก๐นโ๐ง) gcd (๐ ยท ๐)) = 1)) |
168 | 121, 164,
167 | sylanbrc 584 |
. . . . . . . 8
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (โก๐นโ๐ง) โ ๐) |
169 | | funfvima2 7182 |
. . . . . . . . . 10
โข ((Fun
๐น โง ๐ โ dom ๐น) โ ((โก๐นโ๐ง) โ ๐ โ (๐นโ(โก๐นโ๐ง)) โ (๐น โ ๐))) |
170 | 101, 105,
169 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((โก๐นโ๐ง) โ ๐ โ (๐นโ(โก๐นโ๐ง)) โ (๐น โ ๐))) |
171 | 170 | imp 408 |
. . . . . . . 8
โข ((๐ โง (โก๐นโ๐ง) โ ๐) โ (๐นโ(โก๐นโ๐ง)) โ (๐น โ ๐)) |
172 | 168, 171 | syldan 592 |
. . . . . . 7
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ (๐นโ(โก๐นโ๐ง)) โ (๐น โ ๐)) |
173 | 116, 172 | eqeltrrd 2839 |
. . . . . 6
โข ((๐ โง ๐ง โ (๐ ร ๐)) โ ๐ง โ (๐น โ ๐)) |
174 | 108, 173 | eqelssd 3966 |
. . . . 5
โข (๐ โ (๐น โ ๐) = (๐ ร ๐)) |
175 | | f1of1 6784 |
. . . . . . 7
โข (๐น:๐โ1-1-ontoโ๐ โ ๐น:๐โ1-1โ๐) |
176 | 98, 175 | syl 17 |
. . . . . 6
โข (๐ โ ๐น:๐โ1-1โ๐) |
177 | | fzofi 13880 |
. . . . . . . . . 10
โข
(0..^(๐ ยท
๐)) โ
Fin |
178 | 14, 177 | eqeltri 2834 |
. . . . . . . . 9
โข ๐ โ Fin |
179 | | ssfi 9118 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐ โ ๐) โ ๐ โ Fin) |
180 | 178, 102,
179 | mp2an 691 |
. . . . . . . 8
โข ๐ โ Fin |
181 | 180 | elexi 3465 |
. . . . . . 7
โข ๐ โ V |
182 | 181 | f1imaen 8957 |
. . . . . 6
โข ((๐น:๐โ1-1โ๐ โง ๐ โ ๐) โ (๐น โ ๐) โ ๐) |
183 | 176, 102,
182 | sylancl 587 |
. . . . 5
โข (๐ โ (๐น โ ๐) โ ๐) |
184 | 174, 183 | eqbrtrrd 5130 |
. . . 4
โข (๐ โ (๐ ร ๐) โ ๐) |
185 | | fzofi 13880 |
. . . . . . . 8
โข
(0..^๐) โ
Fin |
186 | | ssrab2 4038 |
. . . . . . . 8
โข {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ (0..^๐) |
187 | | ssfi 9118 |
. . . . . . . 8
โข
(((0..^๐) โ Fin
โง {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ (0..^๐)) โ {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ Fin) |
188 | 185, 186,
187 | mp2an 691 |
. . . . . . 7
โข {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ Fin |
189 | 60, 188 | eqeltri 2834 |
. . . . . 6
โข ๐ โ Fin |
190 | | fzofi 13880 |
. . . . . . . 8
โข
(0..^๐) โ
Fin |
191 | | ssrab2 4038 |
. . . . . . . 8
โข {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ (0..^๐) |
192 | | ssfi 9118 |
. . . . . . . 8
โข
(((0..^๐) โ Fin
โง {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ (0..^๐)) โ {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ Fin) |
193 | 190, 191,
192 | mp2an 691 |
. . . . . . 7
โข {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ Fin |
194 | 91, 193 | eqeltri 2834 |
. . . . . 6
โข ๐ โ Fin |
195 | | xpfi 9262 |
. . . . . 6
โข ((๐ โ Fin โง ๐ โ Fin) โ (๐ ร ๐) โ Fin) |
196 | 189, 194,
195 | mp2an 691 |
. . . . 5
โข (๐ ร ๐) โ Fin |
197 | | hashen 14248 |
. . . . 5
โข (((๐ ร ๐) โ Fin โง ๐ โ Fin) โ ((โฏโ(๐ ร ๐)) = (โฏโ๐) โ (๐ ร ๐) โ ๐)) |
198 | 196, 180,
197 | mp2an 691 |
. . . 4
โข
((โฏโ(๐
ร ๐)) =
(โฏโ๐) โ
(๐ ร ๐) โ ๐) |
199 | 184, 198 | sylibr 233 |
. . 3
โข (๐ โ (โฏโ(๐ ร ๐)) = (โฏโ๐)) |
200 | | hashxp 14335 |
. . . 4
โข ((๐ โ Fin โง ๐ โ Fin) โ
(โฏโ(๐ ร
๐)) = ((โฏโ๐) ยท (โฏโ๐))) |
201 | 189, 194,
200 | mp2an 691 |
. . 3
โข
(โฏโ(๐
ร ๐)) =
((โฏโ๐) ยท
(โฏโ๐)) |
202 | 199, 201 | eqtr3di 2792 |
. 2
โข (๐ โ (โฏโ๐) = ((โฏโ๐) ยท (โฏโ๐))) |
203 | 20, 37 | nnmulcld 12207 |
. . 3
โข (๐ โ (๐ ยท ๐) โ โ) |
204 | | dfphi2 16647 |
. . . 4
โข ((๐ ยท ๐) โ โ โ (ฯโ(๐ ยท ๐)) = (โฏโ{๐ฆ โ (0..^(๐ ยท ๐)) โฃ (๐ฆ gcd (๐ ยท ๐)) = 1})) |
205 | 14 | rabeqi 3421 |
. . . . . 6
โข {๐ฆ โ ๐ โฃ (๐ฆ gcd (๐ ยท ๐)) = 1} = {๐ฆ โ (0..^(๐ ยท ๐)) โฃ (๐ฆ gcd (๐ ยท ๐)) = 1} |
206 | 3, 205 | eqtri 2765 |
. . . . 5
โข ๐ = {๐ฆ โ (0..^(๐ ยท ๐)) โฃ (๐ฆ gcd (๐ ยท ๐)) = 1} |
207 | 206 | fveq2i 6846 |
. . . 4
โข
(โฏโ๐) =
(โฏโ{๐ฆ โ
(0..^(๐ ยท ๐)) โฃ (๐ฆ gcd (๐ ยท ๐)) = 1}) |
208 | 204, 207 | eqtr4di 2795 |
. . 3
โข ((๐ ยท ๐) โ โ โ (ฯโ(๐ ยท ๐)) = (โฏโ๐)) |
209 | 203, 208 | syl 17 |
. 2
โข (๐ โ (ฯโ(๐ ยท ๐)) = (โฏโ๐)) |
210 | | dfphi2 16647 |
. . . . 5
โข (๐ โ โ โ
(ฯโ๐) =
(โฏโ{๐ฆ โ
(0..^๐) โฃ (๐ฆ gcd ๐) = 1})) |
211 | 60 | fveq2i 6846 |
. . . . 5
โข
(โฏโ๐) =
(โฏโ{๐ฆ โ
(0..^๐) โฃ (๐ฆ gcd ๐) = 1}) |
212 | 210, 211 | eqtr4di 2795 |
. . . 4
โข (๐ โ โ โ
(ฯโ๐) =
(โฏโ๐)) |
213 | 20, 212 | syl 17 |
. . 3
โข (๐ โ (ฯโ๐) = (โฏโ๐)) |
214 | | dfphi2 16647 |
. . . . 5
โข (๐ โ โ โ
(ฯโ๐) =
(โฏโ{๐ฆ โ
(0..^๐) โฃ (๐ฆ gcd ๐) = 1})) |
215 | 91 | fveq2i 6846 |
. . . . 5
โข
(โฏโ๐) =
(โฏโ{๐ฆ โ
(0..^๐) โฃ (๐ฆ gcd ๐) = 1}) |
216 | 214, 215 | eqtr4di 2795 |
. . . 4
โข (๐ โ โ โ
(ฯโ๐) =
(โฏโ๐)) |
217 | 37, 216 | syl 17 |
. . 3
โข (๐ โ (ฯโ๐) = (โฏโ๐)) |
218 | 213, 217 | oveq12d 7376 |
. 2
โข (๐ โ ((ฯโ๐) ยท (ฯโ๐)) = ((โฏโ๐) ยท (โฏโ๐))) |
219 | 202, 209,
218 | 3eqtr4d 2787 |
1
โข (๐ โ (ฯโ(๐ ยท ๐)) = ((ฯโ๐) ยท (ฯโ๐))) |