Step | Hyp | Ref
| Expression |
1 | | ablfacrp.2 |
. . . . . . 7
โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) |
2 | | ablfacrp.m |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
3 | 2 | nnnn0d 12474 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ0) |
4 | | ablfacrp.n |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
5 | 4 | nnnn0d 12474 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ0) |
6 | 3, 5 | nn0mulcld 12479 |
. . . . . . 7
โข (๐ โ (๐ ยท ๐) โ
โ0) |
7 | 1, 6 | eqeltrd 2838 |
. . . . . 6
โข (๐ โ (โฏโ๐ต) โ
โ0) |
8 | | ablfacrp.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐บ) |
9 | 8 | fvexi 6857 |
. . . . . . 7
โข ๐ต โ V |
10 | | hashclb 14259 |
. . . . . . 7
โข (๐ต โ V โ (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0)) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0) |
12 | 7, 11 | sylibr 233 |
. . . . 5
โข (๐ โ ๐ต โ Fin) |
13 | | ablfacrp.k |
. . . . . 6
โข ๐พ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} |
14 | 13 | ssrab3 4041 |
. . . . 5
โข ๐พ โ ๐ต |
15 | | ssfi 9118 |
. . . . 5
โข ((๐ต โ Fin โง ๐พ โ ๐ต) โ ๐พ โ Fin) |
16 | 12, 14, 15 | sylancl 587 |
. . . 4
โข (๐ โ ๐พ โ Fin) |
17 | | hashcl 14257 |
. . . 4
โข (๐พ โ Fin โ
(โฏโ๐พ) โ
โ0) |
18 | 16, 17 | syl 17 |
. . 3
โข (๐ โ (โฏโ๐พ) โ
โ0) |
19 | | ablfacrp.g |
. . . . . . . 8
โข (๐ โ ๐บ โ Abel) |
20 | 2 | nnzd 12527 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
21 | | ablfacrp.o |
. . . . . . . . 9
โข ๐ = (odโ๐บ) |
22 | 21, 8 | oddvdssubg 19634 |
. . . . . . . 8
โข ((๐บ โ Abel โง ๐ โ โค) โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
23 | 19, 20, 22 | syl2anc 585 |
. . . . . . 7
โข (๐ โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
24 | 13, 23 | eqeltrid 2842 |
. . . . . 6
โข (๐ โ ๐พ โ (SubGrpโ๐บ)) |
25 | 8 | lagsubg 18993 |
. . . . . 6
โข ((๐พ โ (SubGrpโ๐บ) โง ๐ต โ Fin) โ (โฏโ๐พ) โฅ (โฏโ๐ต)) |
26 | 24, 12, 25 | syl2anc 585 |
. . . . 5
โข (๐ โ (โฏโ๐พ) โฅ (โฏโ๐ต)) |
27 | 2 | nncnd 12170 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
28 | 4 | nncnd 12170 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
29 | 27, 28 | mulcomd 11177 |
. . . . . 6
โข (๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
30 | 1, 29 | eqtrd 2777 |
. . . . 5
โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) |
31 | 26, 30 | breqtrd 5132 |
. . . 4
โข (๐ โ (โฏโ๐พ) โฅ (๐ ยท ๐)) |
32 | | ablfacrp.l |
. . . . 5
โข ๐ฟ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} |
33 | | ablfacrp.1 |
. . . . 5
โข (๐ โ (๐ gcd ๐) = 1) |
34 | 8, 21, 13, 32, 19, 2, 4, 33, 1 | ablfacrplem 19845 |
. . . 4
โข (๐ โ ((โฏโ๐พ) gcd ๐) = 1) |
35 | 18 | nn0zd 12526 |
. . . . 5
โข (๐ โ (โฏโ๐พ) โ
โค) |
36 | 4 | nnzd 12527 |
. . . . 5
โข (๐ โ ๐ โ โค) |
37 | | coprmdvds 16530 |
. . . . 5
โข
(((โฏโ๐พ)
โ โค โง ๐
โ โค โง ๐
โ โค) โ (((โฏโ๐พ) โฅ (๐ ยท ๐) โง ((โฏโ๐พ) gcd ๐) = 1) โ (โฏโ๐พ) โฅ ๐)) |
38 | 35, 36, 20, 37 | syl3anc 1372 |
. . . 4
โข (๐ โ (((โฏโ๐พ) โฅ (๐ ยท ๐) โง ((โฏโ๐พ) gcd ๐) = 1) โ (โฏโ๐พ) โฅ ๐)) |
39 | 31, 34, 38 | mp2and 698 |
. . 3
โข (๐ โ (โฏโ๐พ) โฅ ๐) |
40 | 21, 8 | oddvdssubg 19634 |
. . . . . . . . . . 11
โข ((๐บ โ Abel โง ๐ โ โค) โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
41 | 19, 36, 40 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
42 | 32, 41 | eqeltrid 2842 |
. . . . . . . . 9
โข (๐ โ ๐ฟ โ (SubGrpโ๐บ)) |
43 | 8 | lagsubg 18993 |
. . . . . . . . 9
โข ((๐ฟ โ (SubGrpโ๐บ) โง ๐ต โ Fin) โ (โฏโ๐ฟ) โฅ (โฏโ๐ต)) |
44 | 42, 12, 43 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (โฏโ๐ฟ) โฅ (โฏโ๐ต)) |
45 | 44, 1 | breqtrd 5132 |
. . . . . . 7
โข (๐ โ (โฏโ๐ฟ) โฅ (๐ ยท ๐)) |
46 | 20, 36 | gcdcomd 16395 |
. . . . . . . . 9
โข (๐ โ (๐ gcd ๐) = (๐ gcd ๐)) |
47 | 46, 33 | eqtr3d 2779 |
. . . . . . . 8
โข (๐ โ (๐ gcd ๐) = 1) |
48 | 8, 21, 32, 13, 19, 4, 2, 47, 30 | ablfacrplem 19845 |
. . . . . . 7
โข (๐ โ ((โฏโ๐ฟ) gcd ๐) = 1) |
49 | 32 | ssrab3 4041 |
. . . . . . . . . . 11
โข ๐ฟ โ ๐ต |
50 | | ssfi 9118 |
. . . . . . . . . . 11
โข ((๐ต โ Fin โง ๐ฟ โ ๐ต) โ ๐ฟ โ Fin) |
51 | 12, 49, 50 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ ๐ฟ โ Fin) |
52 | | hashcl 14257 |
. . . . . . . . . 10
โข (๐ฟ โ Fin โ
(โฏโ๐ฟ) โ
โ0) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โฏโ๐ฟ) โ
โ0) |
54 | 53 | nn0zd 12526 |
. . . . . . . 8
โข (๐ โ (โฏโ๐ฟ) โ
โค) |
55 | | coprmdvds 16530 |
. . . . . . . 8
โข
(((โฏโ๐ฟ)
โ โค โง ๐
โ โค โง ๐
โ โค) โ (((โฏโ๐ฟ) โฅ (๐ ยท ๐) โง ((โฏโ๐ฟ) gcd ๐) = 1) โ (โฏโ๐ฟ) โฅ ๐)) |
56 | 54, 20, 36, 55 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ (((โฏโ๐ฟ) โฅ (๐ ยท ๐) โง ((โฏโ๐ฟ) gcd ๐) = 1) โ (โฏโ๐ฟ) โฅ ๐)) |
57 | 45, 48, 56 | mp2and 698 |
. . . . . 6
โข (๐ โ (โฏโ๐ฟ) โฅ ๐) |
58 | | dvdscmul 16166 |
. . . . . . 7
โข
(((โฏโ๐ฟ)
โ โค โง ๐
โ โค โง ๐
โ โค) โ ((โฏโ๐ฟ) โฅ ๐ โ (๐ ยท (โฏโ๐ฟ)) โฅ (๐ ยท ๐))) |
59 | 54, 36, 20, 58 | syl3anc 1372 |
. . . . . 6
โข (๐ โ ((โฏโ๐ฟ) โฅ ๐ โ (๐ ยท (โฏโ๐ฟ)) โฅ (๐ ยท ๐))) |
60 | 57, 59 | mpd 15 |
. . . . 5
โข (๐ โ (๐ ยท (โฏโ๐ฟ)) โฅ (๐ ยท ๐)) |
61 | | eqid 2737 |
. . . . . . . . . 10
โข
(0gโ๐บ) = (0gโ๐บ) |
62 | | eqid 2737 |
. . . . . . . . . 10
โข
(LSSumโ๐บ) =
(LSSumโ๐บ) |
63 | 8, 21, 13, 32, 19, 2, 4, 33, 1,
61, 62 | ablfacrp 19846 |
. . . . . . . . 9
โข (๐ โ ((๐พ โฉ ๐ฟ) = {(0gโ๐บ)} โง (๐พ(LSSumโ๐บ)๐ฟ) = ๐ต)) |
64 | 63 | simprd 497 |
. . . . . . . 8
โข (๐ โ (๐พ(LSSumโ๐บ)๐ฟ) = ๐ต) |
65 | 64 | fveq2d 6847 |
. . . . . . 7
โข (๐ โ (โฏโ(๐พ(LSSumโ๐บ)๐ฟ)) = (โฏโ๐ต)) |
66 | | eqid 2737 |
. . . . . . . 8
โข
(Cntzโ๐บ) =
(Cntzโ๐บ) |
67 | 63 | simpld 496 |
. . . . . . . 8
โข (๐ โ (๐พ โฉ ๐ฟ) = {(0gโ๐บ)}) |
68 | 66, 19, 24, 42 | ablcntzd 19636 |
. . . . . . . 8
โข (๐ โ ๐พ โ ((Cntzโ๐บ)โ๐ฟ)) |
69 | 62, 61, 66, 24, 42, 67, 68, 16, 51 | lsmhash 19488 |
. . . . . . 7
โข (๐ โ (โฏโ(๐พ(LSSumโ๐บ)๐ฟ)) = ((โฏโ๐พ) ยท (โฏโ๐ฟ))) |
70 | 65, 69 | eqtr3d 2779 |
. . . . . 6
โข (๐ โ (โฏโ๐ต) = ((โฏโ๐พ) ยท (โฏโ๐ฟ))) |
71 | 70, 1 | eqtr3d 2779 |
. . . . 5
โข (๐ โ ((โฏโ๐พ) ยท (โฏโ๐ฟ)) = (๐ ยท ๐)) |
72 | 60, 71 | breqtrrd 5134 |
. . . 4
โข (๐ โ (๐ ยท (โฏโ๐ฟ)) โฅ ((โฏโ๐พ) ยท (โฏโ๐ฟ))) |
73 | 61 | subg0cl 18937 |
. . . . . . . 8
โข (๐ฟ โ (SubGrpโ๐บ) โ
(0gโ๐บ)
โ ๐ฟ) |
74 | | ne0i 4295 |
. . . . . . . 8
โข
((0gโ๐บ) โ ๐ฟ โ ๐ฟ โ โ
) |
75 | 42, 73, 74 | 3syl 18 |
. . . . . . 7
โข (๐ โ ๐ฟ โ โ
) |
76 | | hashnncl 14267 |
. . . . . . . 8
โข (๐ฟ โ Fin โ
((โฏโ๐ฟ) โ
โ โ ๐ฟ โ
โ
)) |
77 | 51, 76 | syl 17 |
. . . . . . 7
โข (๐ โ ((โฏโ๐ฟ) โ โ โ ๐ฟ โ โ
)) |
78 | 75, 77 | mpbird 257 |
. . . . . 6
โข (๐ โ (โฏโ๐ฟ) โ
โ) |
79 | 78 | nnne0d 12204 |
. . . . 5
โข (๐ โ (โฏโ๐ฟ) โ 0) |
80 | | dvdsmulcr 16169 |
. . . . 5
โข ((๐ โ โค โง
(โฏโ๐พ) โ
โค โง ((โฏโ๐ฟ) โ โค โง (โฏโ๐ฟ) โ 0)) โ ((๐ ยท (โฏโ๐ฟ)) โฅ ((โฏโ๐พ) ยท (โฏโ๐ฟ)) โ ๐ โฅ (โฏโ๐พ))) |
81 | 20, 35, 54, 79, 80 | syl112anc 1375 |
. . . 4
โข (๐ โ ((๐ ยท (โฏโ๐ฟ)) โฅ ((โฏโ๐พ) ยท (โฏโ๐ฟ)) โ ๐ โฅ (โฏโ๐พ))) |
82 | 72, 81 | mpbid 231 |
. . 3
โข (๐ โ ๐ โฅ (โฏโ๐พ)) |
83 | | dvdseq 16197 |
. . 3
โข
((((โฏโ๐พ)
โ โ0 โง ๐ โ โ0) โง
((โฏโ๐พ) โฅ
๐ โง ๐ โฅ (โฏโ๐พ))) โ (โฏโ๐พ) = ๐) |
84 | 18, 3, 39, 82, 83 | syl22anc 838 |
. 2
โข (๐ โ (โฏโ๐พ) = ๐) |
85 | | dvdsmulc 16167 |
. . . . . . 7
โข
(((โฏโ๐พ)
โ โค โง ๐
โ โค โง ๐
โ โค) โ ((โฏโ๐พ) โฅ ๐ โ ((โฏโ๐พ) ยท ๐) โฅ (๐ ยท ๐))) |
86 | 35, 20, 36, 85 | syl3anc 1372 |
. . . . . 6
โข (๐ โ ((โฏโ๐พ) โฅ ๐ โ ((โฏโ๐พ) ยท ๐) โฅ (๐ ยท ๐))) |
87 | 39, 86 | mpd 15 |
. . . . 5
โข (๐ โ ((โฏโ๐พ) ยท ๐) โฅ (๐ ยท ๐)) |
88 | 87, 71 | breqtrrd 5134 |
. . . 4
โข (๐ โ ((โฏโ๐พ) ยท ๐) โฅ ((โฏโ๐พ) ยท (โฏโ๐ฟ))) |
89 | 84, 2 | eqeltrd 2838 |
. . . . . 6
โข (๐ โ (โฏโ๐พ) โ
โ) |
90 | 89 | nnne0d 12204 |
. . . . 5
โข (๐ โ (โฏโ๐พ) โ 0) |
91 | | dvdscmulr 16168 |
. . . . 5
โข ((๐ โ โค โง
(โฏโ๐ฟ) โ
โค โง ((โฏโ๐พ) โ โค โง (โฏโ๐พ) โ 0)) โ
(((โฏโ๐พ)
ยท ๐) โฅ
((โฏโ๐พ) ยท
(โฏโ๐ฟ)) โ
๐ โฅ
(โฏโ๐ฟ))) |
92 | 36, 54, 35, 90, 91 | syl112anc 1375 |
. . . 4
โข (๐ โ (((โฏโ๐พ) ยท ๐) โฅ ((โฏโ๐พ) ยท (โฏโ๐ฟ)) โ ๐ โฅ (โฏโ๐ฟ))) |
93 | 88, 92 | mpbid 231 |
. . 3
โข (๐ โ ๐ โฅ (โฏโ๐ฟ)) |
94 | | dvdseq 16197 |
. . 3
โข
((((โฏโ๐ฟ)
โ โ0 โง ๐ โ โ0) โง
((โฏโ๐ฟ) โฅ
๐ โง ๐ โฅ (โฏโ๐ฟ))) โ (โฏโ๐ฟ) = ๐) |
95 | 53, 5, 57, 93, 94 | syl22anc 838 |
. 2
โข (๐ โ (โฏโ๐ฟ) = ๐) |
96 | 84, 95 | jca 513 |
1
โข (๐ โ ((โฏโ๐พ) = ๐ โง (โฏโ๐ฟ) = ๐)) |