Step | Hyp | Ref
| Expression |
1 | | elfzoelz 13579 |
. . . . . 6
โข (๐ฅ โ (0..^(๐ ยท ๐)) โ ๐ฅ โ โค) |
2 | | crth.1 |
. . . . . 6
โข ๐ = (0..^(๐ ยท ๐)) |
3 | 1, 2 | eleq2s 2856 |
. . . . 5
โข (๐ฅ โ ๐ โ ๐ฅ โ โค) |
4 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โค) โ ๐ฅ โ โค) |
5 | | crth.4 |
. . . . . . . . . 10
โข (๐ โ (๐ โ โ โง ๐ โ โ โง (๐ gcd ๐) = 1)) |
6 | 5 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
7 | 6 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โค) โ ๐ โ โ) |
8 | | zmodfzo 13806 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โ) โ (๐ฅ mod ๐) โ (0..^๐)) |
9 | 4, 7, 8 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โค) โ (๐ฅ mod ๐) โ (0..^๐)) |
10 | 5 | simp2d 1144 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
11 | 10 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โค) โ ๐ โ โ) |
12 | | zmodfzo 13806 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โ) โ (๐ฅ mod ๐) โ (0..^๐)) |
13 | 4, 11, 12 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โค) โ (๐ฅ mod ๐) โ (0..^๐)) |
14 | 9, 13 | opelxpd 5676 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โค) โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ โ ((0..^๐) ร (0..^๐))) |
15 | | crth.2 |
. . . . . 6
โข ๐ = ((0..^๐) ร (0..^๐)) |
16 | 14, 15 | eleqtrrdi 2849 |
. . . . 5
โข ((๐ โง ๐ฅ โ โค) โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ โ ๐) |
17 | 3, 16 | sylan2 594 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ โ ๐) |
18 | | crth.3 |
. . . 4
โข ๐น = (๐ฅ โ ๐ โฆ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ) |
19 | 17, 18 | fmptd 7067 |
. . 3
โข (๐ โ ๐น:๐โถ๐) |
20 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ฅ mod ๐) = (๐ฆ mod ๐)) |
21 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ฅ mod ๐) = (๐ฆ mod ๐)) |
22 | 20, 21 | opeq12d 4843 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ = โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ) |
23 | | opex 5426 |
. . . . . . . . 9
โข
โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ โ V |
24 | 22, 18, 23 | fvmpt 6953 |
. . . . . . . 8
โข (๐ฆ โ ๐ โ (๐นโ๐ฆ) = โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ) |
25 | 24 | ad2antrl 727 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) = โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ) |
26 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ฅ = ๐ง โ (๐ฅ mod ๐) = (๐ง mod ๐)) |
27 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ฅ = ๐ง โ (๐ฅ mod ๐) = (๐ง mod ๐)) |
28 | 26, 27 | opeq12d 4843 |
. . . . . . . . 9
โข (๐ฅ = ๐ง โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ) |
29 | | opex 5426 |
. . . . . . . . 9
โข
โจ(๐ง mod ๐), (๐ง mod ๐)โฉ โ V |
30 | 28, 18, 29 | fvmpt 6953 |
. . . . . . . 8
โข (๐ง โ ๐ โ (๐นโ๐ง) = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ) |
31 | 30 | ad2antll 728 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ) |
32 | 25, 31 | eqeq12d 2753 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ)) |
33 | | ovex 7395 |
. . . . . . 7
โข (๐ฆ mod ๐) โ V |
34 | | ovex 7395 |
. . . . . . 7
โข (๐ฆ mod ๐) โ V |
35 | 33, 34 | opth 5438 |
. . . . . 6
โข
(โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ โ ((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐))) |
36 | 32, 35 | bitrdi 287 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)))) |
37 | 6 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โ) |
38 | 37 | nnzd 12533 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โค) |
39 | 10 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โ) |
40 | 39 | nnzd 12533 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โค) |
41 | | simprl 770 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ ๐) |
42 | 41, 2 | eleqtrdi 2848 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ (0..^(๐ ยท ๐))) |
43 | | elfzoelz 13579 |
. . . . . . . . 9
โข (๐ฆ โ (0..^(๐ ยท ๐)) โ ๐ฆ โ โค) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ โค) |
45 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ ๐) |
46 | 45, 2 | eleqtrdi 2848 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ (0..^(๐ ยท ๐))) |
47 | | elfzoelz 13579 |
. . . . . . . . 9
โข (๐ง โ (0..^(๐ ยท ๐)) โ ๐ง โ โค) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ โค) |
49 | 44, 48 | zsubcld 12619 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ โ ๐ง) โ โค) |
50 | 5 | simp3d 1145 |
. . . . . . . 8
โข (๐ โ (๐ gcd ๐) = 1) |
51 | 50 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ gcd ๐) = 1) |
52 | | coprmdvds2 16537 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค โง (๐ฆ โ ๐ง) โ โค) โง (๐ gcd ๐) = 1) โ ((๐ โฅ (๐ฆ โ ๐ง) โง ๐ โฅ (๐ฆ โ ๐ง)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
53 | 38, 40, 49, 51, 52 | syl31anc 1374 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ โฅ (๐ฆ โ ๐ง) โง ๐ โฅ (๐ฆ โ ๐ง)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
54 | | moddvds 16154 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ฆ โ โค โง ๐ง โ โค) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
55 | 37, 44, 48, 54 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
56 | | moddvds 16154 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ฆ โ โค โง ๐ง โ โค) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
57 | 39, 44, 48, 56 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
58 | 55, 57 | anbi12d 632 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)) โ (๐ โฅ (๐ฆ โ ๐ง) โง ๐ โฅ (๐ฆ โ ๐ง)))) |
59 | 44 | zred 12614 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ โ) |
60 | 37, 39 | nnmulcld 12213 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ ยท ๐) โ โ) |
61 | 60 | nnrpd 12962 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ ยท ๐) โ
โ+) |
62 | | elfzole1 13587 |
. . . . . . . . . 10
โข (๐ฆ โ (0..^(๐ ยท ๐)) โ 0 โค ๐ฆ) |
63 | 42, 62 | syl 17 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 โค ๐ฆ) |
64 | | elfzolt2 13588 |
. . . . . . . . . 10
โข (๐ฆ โ (0..^(๐ ยท ๐)) โ ๐ฆ < (๐ ยท ๐)) |
65 | 42, 64 | syl 17 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ < (๐ ยท ๐)) |
66 | | modid 13808 |
. . . . . . . . 9
โข (((๐ฆ โ โ โง (๐ ยท ๐) โ โ+) โง (0 โค
๐ฆ โง ๐ฆ < (๐ ยท ๐))) โ (๐ฆ mod (๐ ยท ๐)) = ๐ฆ) |
67 | 59, 61, 63, 65, 66 | syl22anc 838 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ mod (๐ ยท ๐)) = ๐ฆ) |
68 | 48 | zred 12614 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ โ) |
69 | | elfzole1 13587 |
. . . . . . . . . 10
โข (๐ง โ (0..^(๐ ยท ๐)) โ 0 โค ๐ง) |
70 | 46, 69 | syl 17 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 โค ๐ง) |
71 | | elfzolt2 13588 |
. . . . . . . . . 10
โข (๐ง โ (0..^(๐ ยท ๐)) โ ๐ง < (๐ ยท ๐)) |
72 | 46, 71 | syl 17 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง < (๐ ยท ๐)) |
73 | | modid 13808 |
. . . . . . . . 9
โข (((๐ง โ โ โง (๐ ยท ๐) โ โ+) โง (0 โค
๐ง โง ๐ง < (๐ ยท ๐))) โ (๐ง mod (๐ ยท ๐)) = ๐ง) |
74 | 68, 61, 70, 72, 73 | syl22anc 838 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ง mod (๐ ยท ๐)) = ๐ง) |
75 | 67, 74 | eqeq12d 2753 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod (๐ ยท ๐)) = (๐ง mod (๐ ยท ๐)) โ ๐ฆ = ๐ง)) |
76 | | moddvds 16154 |
. . . . . . . 8
โข (((๐ ยท ๐) โ โ โง ๐ฆ โ โค โง ๐ง โ โค) โ ((๐ฆ mod (๐ ยท ๐)) = (๐ง mod (๐ ยท ๐)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
77 | 60, 44, 48, 76 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod (๐ ยท ๐)) = (๐ง mod (๐ ยท ๐)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
78 | 75, 77 | bitr3d 281 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ = ๐ง โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
79 | 53, 58, 78 | 3imtr4d 294 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)) โ ๐ฆ = ๐ง)) |
80 | 36, 79 | sylbid 239 |
. . . 4
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
81 | 80 | ralrimivva 3198 |
. . 3
โข (๐ โ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
82 | | dff13 7207 |
. . 3
โข (๐น:๐โ1-1โ๐ โ (๐น:๐โถ๐ โง โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง))) |
83 | 19, 81, 82 | sylanbrc 584 |
. 2
โข (๐ โ ๐น:๐โ1-1โ๐) |
84 | | nnnn0 12427 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
85 | | nnnn0 12427 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
86 | | nn0mulcl 12456 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท ๐) โ
โ0) |
87 | | hashfzo0 14337 |
. . . . . . . . 9
โข ((๐ ยท ๐) โ โ0 โ
(โฏโ(0..^(๐
ยท ๐))) = (๐ ยท ๐)) |
88 | 86, 87 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โฏโ(0..^(๐ ยท ๐))) = (๐ ยท ๐)) |
89 | | fzofi 13886 |
. . . . . . . . . 10
โข
(0..^๐) โ
Fin |
90 | | fzofi 13886 |
. . . . . . . . . 10
โข
(0..^๐) โ
Fin |
91 | | hashxp 14341 |
. . . . . . . . . 10
โข
(((0..^๐) โ Fin
โง (0..^๐) โ Fin)
โ (โฏโ((0..^๐) ร (0..^๐))) = ((โฏโ(0..^๐)) ยท (โฏโ(0..^๐)))) |
92 | 89, 90, 91 | mp2an 691 |
. . . . . . . . 9
โข
(โฏโ((0..^๐) ร (0..^๐))) = ((โฏโ(0..^๐)) ยท (โฏโ(0..^๐))) |
93 | | hashfzo0 14337 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (โฏโ(0..^๐)) = ๐) |
94 | | hashfzo0 14337 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (โฏโ(0..^๐)) = ๐) |
95 | 93, 94 | oveqan12d 7381 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โฏโ(0..^๐)) ยท (โฏโ(0..^๐))) = (๐ ยท ๐)) |
96 | 92, 95 | eqtrid 2789 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โฏโ((0..^๐) ร (0..^๐))) = (๐ ยท ๐)) |
97 | 88, 96 | eqtr4d 2780 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โฏโ(0..^(๐ ยท ๐))) = (โฏโ((0..^๐) ร (0..^๐)))) |
98 | | fzofi 13886 |
. . . . . . . 8
โข
(0..^(๐ ยท
๐)) โ
Fin |
99 | | xpfi 9268 |
. . . . . . . . 9
โข
(((0..^๐) โ Fin
โง (0..^๐) โ Fin)
โ ((0..^๐) ร
(0..^๐)) โ
Fin) |
100 | 89, 90, 99 | mp2an 691 |
. . . . . . . 8
โข
((0..^๐) ร
(0..^๐)) โ
Fin |
101 | | hashen 14254 |
. . . . . . . 8
โข
(((0..^(๐ ยท
๐)) โ Fin โง
((0..^๐) ร (0..^๐)) โ Fin) โ
((โฏโ(0..^(๐
ยท ๐))) =
(โฏโ((0..^๐)
ร (0..^๐))) โ
(0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐)))) |
102 | 98, 100, 101 | mp2an 691 |
. . . . . . 7
โข
((โฏโ(0..^(๐ ยท ๐))) = (โฏโ((0..^๐) ร (0..^๐))) โ (0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐))) |
103 | 97, 102 | sylib 217 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐))) |
104 | 84, 85, 103 | syl2an 597 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
(0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐))) |
105 | 6, 10, 104 | syl2anc 585 |
. . . 4
โข (๐ โ (0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐))) |
106 | 105, 2, 15 | 3brtr4g 5144 |
. . 3
โข (๐ โ ๐ โ ๐) |
107 | 15, 100 | eqeltri 2834 |
. . 3
โข ๐ โ Fin |
108 | | f1finf1o 9222 |
. . 3
โข ((๐ โ ๐ โง ๐ โ Fin) โ (๐น:๐โ1-1โ๐ โ ๐น:๐โ1-1-ontoโ๐)) |
109 | 106, 107,
108 | sylancl 587 |
. 2
โข (๐ โ (๐น:๐โ1-1โ๐ โ ๐น:๐โ1-1-ontoโ๐)) |
110 | 83, 109 | mpbid 231 |
1
โข (๐ โ ๐น:๐โ1-1-ontoโ๐) |