Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
Cntz Cntz |
2 | | eqid 2622 |
. 2
|
3 | | eqid 2622 |
. 2
mrClsSubGrp mrClsSubGrp |
4 | | ablfac1.g |
. . 3
|
5 | | ablgrp 18198 |
. . 3
|
6 | 4, 5 | syl 17 |
. 2
|
7 | | ablfac1.1 |
. . 3
|
8 | | nnex 11026 |
. . . . 5
|
9 | | prmnn 15388 |
. . . . . 6
|
10 | 9 | ssriv 3607 |
. . . . 5
|
11 | 8, 10 | ssexi 4803 |
. . . 4
|
12 | 11 | ssex 4802 |
. . 3
|
13 | 7, 12 | syl 17 |
. 2
|
14 | 4 | adantr 481 |
. . . 4
|
15 | 7 | sselda 3603 |
. . . . . . 7
|
16 | 15, 9 | syl 17 |
. . . . . 6
|
17 | | ablfac1.b |
. . . . . . . . . . 11
|
18 | 17 | grpbn0 17451 |
. . . . . . . . . 10
|
19 | 6, 18 | syl 17 |
. . . . . . . . 9
|
20 | | ablfac1.f |
. . . . . . . . . 10
|
21 | | hashnncl 13157 |
. . . . . . . . . 10
|
22 | 20, 21 | syl 17 |
. . . . . . . . 9
|
23 | 19, 22 | mpbird 247 |
. . . . . . . 8
|
24 | 23 | adantr 481 |
. . . . . . 7
|
25 | 15, 24 | pccld 15555 |
. . . . . 6
|
26 | 16, 25 | nnexpcld 13030 |
. . . . 5
|
27 | 26 | nnzd 11481 |
. . . 4
|
28 | | ablfac1.o |
. . . . 5
|
29 | 28, 17 | oddvdssubg 18258 |
. . . 4
SubGrp |
30 | 14, 27, 29 | syl2anc 693 |
. . 3
SubGrp |
31 | | ablfac1.s |
. . 3
|
32 | 30, 31 | fmptd 6385 |
. 2
SubGrp |
33 | 4 | adantr 481 |
. . 3
|
34 | 32 | adantr 481 |
. . . 4
SubGrp |
35 | | simpr1 1067 |
. . . 4
|
36 | 34, 35 | ffvelrnd 6360 |
. . 3
SubGrp |
37 | | simpr2 1068 |
. . . 4
|
38 | 34, 37 | ffvelrnd 6360 |
. . 3
SubGrp |
39 | 1, 33, 36, 38 | ablcntzd 18260 |
. 2
Cntz |
40 | | id 22 |
. . . . . . . . . 10
|
41 | | oveq1 6657 |
. . . . . . . . . 10
|
42 | 40, 41 | oveq12d 6668 |
. . . . . . . . 9
|
43 | 42 | breq2d 4665 |
. . . . . . . 8
|
44 | 43 | rabbidv 3189 |
. . . . . . 7
|
45 | | fvex 6201 |
. . . . . . . . 9
|
46 | 17, 45 | eqeltri 2697 |
. . . . . . . 8
|
47 | 46 | rabex 4813 |
. . . . . . 7
|
48 | 44, 31, 47 | fvmpt3i 6287 |
. . . . . 6
|
49 | 48 | adantl 482 |
. . . . 5
|
50 | | eqimss 3657 |
. . . . 5
|
51 | 49, 50 | syl 17 |
. . . 4
|
52 | 4 | adantr 481 |
. . . . . 6
|
53 | | eqid 2622 |
. . . . . . 7
|
54 | 53 | subgacs 17629 |
. . . . . 6
SubGrp ACS |
55 | | acsmre 16313 |
. . . . . 6
SubGrp ACS SubGrp Moore |
56 | 52, 5, 54, 55 | 4syl 19 |
. . . . 5
SubGrp Moore |
57 | | df-ima 5127 |
. . . . . . 7
|
58 | 7 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
60 | 23 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
|
61 | | pcdvds 15568 |
. . . . . . . . . . . . . . . 16
|
62 | 59, 60, 61 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
63 | 7 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
|
64 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
|
66 | 63, 65 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
|
67 | | pcdvds 15568 |
. . . . . . . . . . . . . . . 16
|
68 | 66, 60, 67 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
69 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 17, 28, 31, 4, 20, 7, 69, 70 | ablfac1lem 18467 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 72 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
|
74 | 73 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
76 | 66, 9 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
77 | 66, 60 | pccld 15555 |
. . . . . . . . . . . . . . . . . 18
|
78 | 76, 77 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . 17
|
79 | 78 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
80 | 60 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
81 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 81 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 82 | necomd 2849 |
. . . . . . . . . . . . . . . . . 18
|
84 | | prmrp 15424 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 59, 66, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
86 | 83, 85 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
87 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 59, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
89 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 66, 89 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
91 | 59, 60 | pccld 15555 |
. . . . . . . . . . . . . . . . . 18
|
92 | | rpexp12i 15434 |
. . . . . . . . . . . . . . . . . 18
|
93 | 88, 90, 91, 77, 92 | syl112anc 1330 |
. . . . . . . . . . . . . . . . 17
|
94 | 86, 93 | mpd 15 |
. . . . . . . . . . . . . . . 16
|
95 | | coprmdvds2 15368 |
. . . . . . . . . . . . . . . 16
|
96 | 75, 79, 80, 94, 95 | syl31anc 1329 |
. . . . . . . . . . . . . . 15
|
97 | 62, 68, 96 | mp2and 715 |
. . . . . . . . . . . . . 14
|
98 | 71 | simp3d 1075 |
. . . . . . . . . . . . . . 15
|
99 | 98 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
100 | 97, 99 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
101 | 72 | simprd 479 |
. . . . . . . . . . . . . . . 16
|
102 | 101 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
103 | 102 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
104 | 74 | nnne0d 11065 |
. . . . . . . . . . . . . 14
|
105 | | dvdscmulr 15010 |
. . . . . . . . . . . . . 14
|
106 | 79, 103, 75, 104, 105 | syl112anc 1330 |
. . . . . . . . . . . . 13
|
107 | 100, 106 | mpbid 222 |
. . . . . . . . . . . 12
|
108 | 17, 28 | odcl 17955 |
. . . . . . . . . . . . . . 15
|
109 | 108 | adantl 482 |
. . . . . . . . . . . . . 14
|
110 | 109 | nn0zd 11480 |
. . . . . . . . . . . . 13
|
111 | | dvdstr 15018 |
. . . . . . . . . . . . 13
|
112 | 110, 79, 103, 111 | syl3anc 1326 |
. . . . . . . . . . . 12
|
113 | 107, 112 | mpan2d 710 |
. . . . . . . . . . 11
|
114 | 113 | ss2rabdv 3683 |
. . . . . . . . . 10
|
115 | 47 | elpw 4164 |
. . . . . . . . . 10
|
116 | 114, 115 | sylibr 224 |
. . . . . . . . 9
|
117 | 31 | reseq1i 5392 |
. . . . . . . . . 10
|
118 | | difss 3737 |
. . . . . . . . . . 11
|
119 | | resmpt 5449 |
. . . . . . . . . . 11
|
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . 10
|
121 | 117, 120 | eqtri 2644 |
. . . . . . . . 9
|
122 | 116, 121 | fmptd 6385 |
. . . . . . . 8
|
123 | | frn 6053 |
. . . . . . . 8
|
124 | 122, 123 | syl 17 |
. . . . . . 7
|
125 | 57, 124 | syl5eqss 3649 |
. . . . . 6
|
126 | | sspwuni 4611 |
. . . . . 6
|
127 | 125, 126 | sylib 208 |
. . . . 5
|
128 | 101 | nnzd 11481 |
. . . . . 6
|
129 | 28, 17 | oddvdssubg 18258 |
. . . . . 6
SubGrp |
130 | 52, 128, 129 | syl2anc 693 |
. . . . 5
SubGrp |
131 | 3 | mrcsscl 16280 |
. . . . 5
SubGrp Moore
SubGrp mrClsSubGrp
|
132 | 56, 127, 130, 131 | syl3anc 1326 |
. . . 4
mrClsSubGrp
|
133 | | ss2in 3840 |
. . . 4
mrClsSubGrp
mrClsSubGrp
|
134 | 51, 132, 133 | syl2anc 693 |
. . 3
mrClsSubGrp |
135 | | eqid 2622 |
. . . . 5
|
136 | | eqid 2622 |
. . . . 5
|
137 | 71 | simp2d 1074 |
. . . . 5
|
138 | | eqid 2622 |
. . . . 5
|
139 | 17, 28, 135, 136, 52, 73, 101, 137, 98, 2, 138 | ablfacrp 18465 |
. . . 4
|
140 | 139 | simpld 475 |
. . 3
|
141 | 134, 140 | sseqtrd 3641 |
. 2
mrClsSubGrp |
142 | 1, 2, 3, 6, 13, 32, 39, 141 | dmdprdd 18398 |
1
DProd
|