Step | Hyp | Ref
| Expression |
1 | | nprmdvds1 16590 |
. . . . . . 7
โข (๐ โ โ โ ยฌ
๐ โฅ
1) |
2 | 1 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ยฌ ๐ โฅ 1) |
3 | | ablfacrp.1 |
. . . . . . . 8
โข (๐ โ (๐ gcd ๐) = 1) |
4 | 3 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐ gcd ๐) = 1) |
5 | 4 | breq2d 5121 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (๐ โฅ (๐ gcd ๐) โ ๐ โฅ 1)) |
6 | 2, 5 | mtbird 325 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ยฌ ๐ โฅ (๐ gcd ๐)) |
7 | | ablfacrp.k |
. . . . . . . . . . . . . 14
โข ๐พ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} |
8 | | ablfacrp.g |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐บ โ Abel) |
9 | | ablfacrp.m |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โ) |
10 | 9 | nnzd 12534 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โค) |
11 | | ablfacrp.o |
. . . . . . . . . . . . . . . 16
โข ๐ = (odโ๐บ) |
12 | | ablfacrp.b |
. . . . . . . . . . . . . . . 16
โข ๐ต = (Baseโ๐บ) |
13 | 11, 12 | oddvdssubg 19641 |
. . . . . . . . . . . . . . 15
โข ((๐บ โ Abel โง ๐ โ โค) โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
14 | 8, 10, 13 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} โ (SubGrpโ๐บ)) |
15 | 7, 14 | eqeltrid 2838 |
. . . . . . . . . . . . 13
โข (๐ โ ๐พ โ (SubGrpโ๐บ)) |
16 | 15 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ ๐พ โ (SubGrpโ๐บ)) |
17 | | eqid 2733 |
. . . . . . . . . . . . 13
โข (๐บ โพs ๐พ) = (๐บ โพs ๐พ) |
18 | 17 | subggrp 18939 |
. . . . . . . . . . . 12
โข (๐พ โ (SubGrpโ๐บ) โ (๐บ โพs ๐พ) โ Grp) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ (๐บ โพs ๐พ) โ Grp) |
20 | 17 | subgbas 18940 |
. . . . . . . . . . . . 13
โข (๐พ โ (SubGrpโ๐บ) โ ๐พ = (Baseโ(๐บ โพs ๐พ))) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ ๐พ = (Baseโ(๐บ โพs ๐พ))) |
22 | | ablfacrp.2 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) |
23 | 9 | nnnn0d 12481 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ
โ0) |
24 | | ablfacrp.n |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ โ) |
25 | 24 | nnnn0d 12481 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ
โ0) |
26 | 23, 25 | nn0mulcld 12486 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ ยท ๐) โ
โ0) |
27 | 22, 26 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โฏโ๐ต) โ
โ0) |
28 | 12 | fvexi 6860 |
. . . . . . . . . . . . . . . 16
โข ๐ต โ V |
29 | | hashclb 14267 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ V โ (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0) |
31 | 27, 30 | sylibr 233 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ต โ Fin) |
32 | 7 | ssrab3 4044 |
. . . . . . . . . . . . . 14
โข ๐พ โ ๐ต |
33 | | ssfi 9123 |
. . . . . . . . . . . . . 14
โข ((๐ต โ Fin โง ๐พ โ ๐ต) โ ๐พ โ Fin) |
34 | 31, 32, 33 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ ๐พ โ Fin) |
35 | 34 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ ๐พ โ Fin) |
36 | 21, 35 | eqeltrrd 2835 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ (Baseโ(๐บ โพs ๐พ)) โ Fin) |
37 | | simplr 768 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ ๐ โ โ) |
38 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ ๐ โฅ (โฏโ๐พ)) |
39 | 21 | fveq2d 6850 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ (โฏโ๐พ) = (โฏโ(Baseโ(๐บ โพs ๐พ)))) |
40 | 38, 39 | breqtrd 5135 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ ๐ โฅ (โฏโ(Baseโ(๐บ โพs ๐พ)))) |
41 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(Baseโ(๐บ
โพs ๐พ)) =
(Baseโ(๐บ
โพs ๐พ)) |
42 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(odโ(๐บ
โพs ๐พ)) =
(odโ(๐บ
โพs ๐พ)) |
43 | 41, 42 | odcau 19394 |
. . . . . . . . . . 11
โข ((((๐บ โพs ๐พ) โ Grp โง
(Baseโ(๐บ
โพs ๐พ))
โ Fin โง ๐ โ
โ) โง ๐ โฅ
(โฏโ(Baseโ(๐บ โพs ๐พ)))) โ โ๐ โ (Baseโ(๐บ โพs ๐พ))((odโ(๐บ โพs ๐พ))โ๐) = ๐) |
44 | 19, 36, 37, 40, 43 | syl31anc 1374 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ โ๐ โ (Baseโ(๐บ โพs ๐พ))((odโ(๐บ โพs ๐พ))โ๐) = ๐) |
45 | 21 | rexeqdv 3313 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ (โ๐ โ ๐พ ((odโ(๐บ โพs ๐พ))โ๐) = ๐ โ โ๐ โ (Baseโ(๐บ โพs ๐พ))((odโ(๐บ โพs ๐พ))โ๐) = ๐)) |
46 | 44, 45 | mpbird 257 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ โ๐ โ ๐พ ((odโ(๐บ โพs ๐พ))โ๐) = ๐) |
47 | 17, 11, 42 | subgod 19360 |
. . . . . . . . . . . . 13
โข ((๐พ โ (SubGrpโ๐บ) โง ๐ โ ๐พ) โ (๐โ๐) = ((odโ(๐บ โพs ๐พ))โ๐)) |
48 | 16, 47 | sylan 581 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โง ๐ โ ๐พ) โ (๐โ๐) = ((odโ(๐บ โพs ๐พ))โ๐)) |
49 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ (๐โ๐ฅ) = (๐โ๐)) |
50 | 49 | breq1d 5119 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ ((๐โ๐ฅ) โฅ ๐ โ (๐โ๐) โฅ ๐)) |
51 | 50, 7 | elrab2 3652 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐พ โ (๐ โ ๐ต โง (๐โ๐) โฅ ๐)) |
52 | 51 | simprbi 498 |
. . . . . . . . . . . . 13
โข (๐ โ ๐พ โ (๐โ๐) โฅ ๐) |
53 | 52 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โง ๐ โ ๐พ) โ (๐โ๐) โฅ ๐) |
54 | 48, 53 | eqbrtrrd 5133 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โง ๐ โ ๐พ) โ ((odโ(๐บ โพs ๐พ))โ๐) โฅ ๐) |
55 | | breq1 5112 |
. . . . . . . . . . 11
โข
(((odโ(๐บ
โพs ๐พ))โ๐) = ๐ โ (((odโ(๐บ โพs ๐พ))โ๐) โฅ ๐ โ ๐ โฅ ๐)) |
56 | 54, 55 | syl5ibcom 244 |
. . . . . . . . . 10
โข ((((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โง ๐ โ ๐พ) โ (((odโ(๐บ โพs ๐พ))โ๐) = ๐ โ ๐ โฅ ๐)) |
57 | 56 | rexlimdva 3149 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ (โ๐ โ ๐พ ((odโ(๐บ โพs ๐พ))โ๐) = ๐ โ ๐ โฅ ๐)) |
58 | 46, 57 | mpd 15 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ) โง ๐ โฅ (โฏโ๐พ)) โ ๐ โฅ ๐) |
59 | 58 | ex 414 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐ โฅ (โฏโ๐พ) โ ๐ โฅ ๐)) |
60 | 59 | anim1d 612 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โฅ (โฏโ๐พ) โง ๐ โฅ ๐) โ (๐ โฅ ๐ โง ๐ โฅ ๐))) |
61 | | prmz 16559 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
62 | 61 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐ โ โค) |
63 | | hashcl 14265 |
. . . . . . . . . 10
โข (๐พ โ Fin โ
(โฏโ๐พ) โ
โ0) |
64 | 34, 63 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โฏโ๐พ) โ
โ0) |
65 | 64 | nn0zd 12533 |
. . . . . . . 8
โข (๐ โ (โฏโ๐พ) โ
โค) |
66 | 65 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (โฏโ๐พ) โ
โค) |
67 | 24 | nnzd 12534 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
68 | 67 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐ โ โค) |
69 | | dvdsgcdb 16434 |
. . . . . . 7
โข ((๐ โ โค โง
(โฏโ๐พ) โ
โค โง ๐ โ
โค) โ ((๐ โฅ
(โฏโ๐พ) โง
๐ โฅ ๐) โ ๐ โฅ ((โฏโ๐พ) gcd ๐))) |
70 | 62, 66, 68, 69 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โฅ (โฏโ๐พ) โง ๐ โฅ ๐) โ ๐ โฅ ((โฏโ๐พ) gcd ๐))) |
71 | 10 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐ โ โค) |
72 | | dvdsgcdb 16434 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ โฅ (๐ gcd ๐))) |
73 | 62, 71, 68, 72 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ โฅ (๐ gcd ๐))) |
74 | 60, 70, 73 | 3imtr3d 293 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐ โฅ ((โฏโ๐พ) gcd ๐) โ ๐ โฅ (๐ gcd ๐))) |
75 | 6, 74 | mtod 197 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ยฌ ๐ โฅ ((โฏโ๐พ) gcd ๐)) |
76 | 75 | nrexdv 3143 |
. . 3
โข (๐ โ ยฌ โ๐ โ โ ๐ โฅ ((โฏโ๐พ) gcd ๐)) |
77 | | exprmfct 16588 |
. . 3
โข
(((โฏโ๐พ)
gcd ๐) โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ((โฏโ๐พ) gcd ๐)) |
78 | 76, 77 | nsyl 140 |
. 2
โข (๐ โ ยฌ
((โฏโ๐พ) gcd
๐) โ
(โคโฅโ2)) |
79 | 24 | nnne0d 12211 |
. . . . . 6
โข (๐ โ ๐ โ 0) |
80 | | simpr 486 |
. . . . . . 7
โข
(((โฏโ๐พ)
= 0 โง ๐ = 0) โ
๐ = 0) |
81 | 80 | necon3ai 2965 |
. . . . . 6
โข (๐ โ 0 โ ยฌ
((โฏโ๐พ) = 0
โง ๐ =
0)) |
82 | 79, 81 | syl 17 |
. . . . 5
โข (๐ โ ยฌ
((โฏโ๐พ) = 0
โง ๐ =
0)) |
83 | | gcdn0cl 16390 |
. . . . 5
โข
((((โฏโ๐พ)
โ โค โง ๐
โ โค) โง ยฌ ((โฏโ๐พ) = 0 โง ๐ = 0)) โ ((โฏโ๐พ) gcd ๐) โ โ) |
84 | 65, 67, 82, 83 | syl21anc 837 |
. . . 4
โข (๐ โ ((โฏโ๐พ) gcd ๐) โ โ) |
85 | | elnn1uz2 12858 |
. . . 4
โข
(((โฏโ๐พ)
gcd ๐) โ โ
โ (((โฏโ๐พ)
gcd ๐) = 1 โจ
((โฏโ๐พ) gcd
๐) โ
(โคโฅโ2))) |
86 | 84, 85 | sylib 217 |
. . 3
โข (๐ โ (((โฏโ๐พ) gcd ๐) = 1 โจ ((โฏโ๐พ) gcd ๐) โ
(โคโฅโ2))) |
87 | 86 | ord 863 |
. 2
โข (๐ โ (ยฌ
((โฏโ๐พ) gcd
๐) = 1 โ
((โฏโ๐พ) gcd
๐) โ
(โคโฅโ2))) |
88 | 78, 87 | mt3d 148 |
1
โข (๐ โ ((โฏโ๐พ) gcd ๐) = 1) |