Step | Hyp | Ref
| Expression |
1 | | pgpfac1.c |
. . . 4
β’ (π β πΆ β (π β (π β π))) |
2 | 1 | eldifbd 3928 |
. . 3
β’ (π β Β¬ πΆ β (π β π)) |
3 | | pgpfac1.p |
. . . . . . . 8
β’ (π β π pGrp πΊ) |
4 | | pgpprm 19382 |
. . . . . . . 8
β’ (π pGrp πΊ β π β β) |
5 | 3, 4 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
6 | | pgpfac1.g |
. . . . . . . . 9
β’ (π β πΊ β Abel) |
7 | | ablgrp 19574 |
. . . . . . . . 9
β’ (πΊ β Abel β πΊ β Grp) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (π β πΊ β Grp) |
9 | | pgpfac1.n |
. . . . . . . 8
β’ (π β π΅ β Fin) |
10 | | pgpfac1.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΊ) |
11 | | pgpfac1.e |
. . . . . . . . 9
β’ πΈ = (gExβπΊ) |
12 | 10, 11 | gexcl2 19378 |
. . . . . . . 8
β’ ((πΊ β Grp β§ π΅ β Fin) β πΈ β
β) |
13 | 8, 9, 12 | syl2anc 585 |
. . . . . . 7
β’ (π β πΈ β β) |
14 | | pceq0 16750 |
. . . . . . 7
β’ ((π β β β§ πΈ β β) β ((π pCnt πΈ) = 0 β Β¬ π β₯ πΈ)) |
15 | 5, 13, 14 | syl2anc 585 |
. . . . . 6
β’ (π β ((π pCnt πΈ) = 0 β Β¬ π β₯ πΈ)) |
16 | | oveq2 7370 |
. . . . . 6
β’ ((π pCnt πΈ) = 0 β (πβ(π pCnt πΈ)) = (πβ0)) |
17 | 15, 16 | syl6bir 254 |
. . . . 5
β’ (π β (Β¬ π β₯ πΈ β (πβ(π pCnt πΈ)) = (πβ0))) |
18 | 10 | grpbn0 18786 |
. . . . . . . . . . . . 13
β’ (πΊ β Grp β π΅ β β
) |
19 | 8, 18 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π΅ β β
) |
20 | | hashnncl 14273 |
. . . . . . . . . . . . 13
β’ (π΅ β Fin β
((β―βπ΅) β
β β π΅ β
β
)) |
21 | 9, 20 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ΅) β β β π΅ β β
)) |
22 | 19, 21 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β (β―βπ΅) β
β) |
23 | 5, 22 | pccld 16729 |
. . . . . . . . . 10
β’ (π β (π pCnt (β―βπ΅)) β
β0) |
24 | 10, 11 | gexdvds3 19379 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ π΅ β Fin) β πΈ β₯ (β―βπ΅)) |
25 | 8, 9, 24 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β πΈ β₯ (β―βπ΅)) |
26 | 10 | pgphash 19396 |
. . . . . . . . . . . 12
β’ ((π pGrp πΊ β§ π΅ β Fin) β (β―βπ΅) = (πβ(π pCnt (β―βπ΅)))) |
27 | 3, 9, 26 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (β―βπ΅) = (πβ(π pCnt (β―βπ΅)))) |
28 | 25, 27 | breqtrd 5136 |
. . . . . . . . . 10
β’ (π β πΈ β₯ (πβ(π pCnt (β―βπ΅)))) |
29 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = (π pCnt (β―βπ΅)) β (πβπ) = (πβ(π pCnt (β―βπ΅)))) |
30 | 29 | breq2d 5122 |
. . . . . . . . . . 11
β’ (π = (π pCnt (β―βπ΅)) β (πΈ β₯ (πβπ) β πΈ β₯ (πβ(π pCnt (β―βπ΅))))) |
31 | 30 | rspcev 3584 |
. . . . . . . . . 10
β’ (((π pCnt (β―βπ΅)) β β0
β§ πΈ β₯ (πβ(π pCnt (β―βπ΅)))) β βπ β β0 πΈ β₯ (πβπ)) |
32 | 23, 28, 31 | syl2anc 585 |
. . . . . . . . 9
β’ (π β βπ β β0 πΈ β₯ (πβπ)) |
33 | | pcprmpw2 16761 |
. . . . . . . . . 10
β’ ((π β β β§ πΈ β β) β
(βπ β
β0 πΈ
β₯ (πβπ) β πΈ = (πβ(π pCnt πΈ)))) |
34 | 5, 13, 33 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (βπ β β0 πΈ β₯ (πβπ) β πΈ = (πβ(π pCnt πΈ)))) |
35 | 32, 34 | mpbid 231 |
. . . . . . . 8
β’ (π β πΈ = (πβ(π pCnt πΈ))) |
36 | 35 | eqcomd 2743 |
. . . . . . 7
β’ (π β (πβ(π pCnt πΈ)) = πΈ) |
37 | | prmnn 16557 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
38 | 5, 37 | syl 17 |
. . . . . . . . 9
β’ (π β π β β) |
39 | 38 | nncnd 12176 |
. . . . . . . 8
β’ (π β π β β) |
40 | 39 | exp0d 14052 |
. . . . . . 7
β’ (π β (πβ0) = 1) |
41 | 36, 40 | eqeq12d 2753 |
. . . . . 6
β’ (π β ((πβ(π pCnt πΈ)) = (πβ0) β πΈ = 1)) |
42 | 8 | grpmndd 18767 |
. . . . . . 7
β’ (π β πΊ β Mnd) |
43 | 10, 11 | gex1 19380 |
. . . . . . 7
β’ (πΊ β Mnd β (πΈ = 1 β π΅ β 1o)) |
44 | 42, 43 | syl 17 |
. . . . . 6
β’ (π β (πΈ = 1 β π΅ β 1o)) |
45 | 41, 44 | bitrd 279 |
. . . . 5
β’ (π β ((πβ(π pCnt πΈ)) = (πβ0) β π΅ β 1o)) |
46 | 17, 45 | sylibd 238 |
. . . 4
β’ (π β (Β¬ π β₯ πΈ β π΅ β 1o)) |
47 | | pgpfac1.s |
. . . . . . . . . . 11
β’ π = (πΎβ{π΄}) |
48 | 10 | subgacs 18970 |
. . . . . . . . . . . . . 14
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβπ΅)) |
49 | 8, 48 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (SubGrpβπΊ) β (ACSβπ΅)) |
50 | 49 | acsmred 17543 |
. . . . . . . . . . . 12
β’ (π β (SubGrpβπΊ) β (Mooreβπ΅)) |
51 | | pgpfac1.u |
. . . . . . . . . . . . . 14
β’ (π β π β (SubGrpβπΊ)) |
52 | 10 | subgss 18936 |
. . . . . . . . . . . . . 14
β’ (π β (SubGrpβπΊ) β π β π΅) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β π΅) |
54 | | pgpfac1.au |
. . . . . . . . . . . . 13
β’ (π β π΄ β π) |
55 | 53, 54 | sseldd 3950 |
. . . . . . . . . . . 12
β’ (π β π΄ β π΅) |
56 | | pgpfac1.k |
. . . . . . . . . . . . 13
β’ πΎ =
(mrClsβ(SubGrpβπΊ)) |
57 | 56 | mrcsncl 17499 |
. . . . . . . . . . . 12
β’
(((SubGrpβπΊ)
β (Mooreβπ΅)
β§ π΄ β π΅) β (πΎβ{π΄}) β (SubGrpβπΊ)) |
58 | 50, 55, 57 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πΎβ{π΄}) β (SubGrpβπΊ)) |
59 | 47, 58 | eqeltrid 2842 |
. . . . . . . . . 10
β’ (π β π β (SubGrpβπΊ)) |
60 | | pgpfac1.w |
. . . . . . . . . 10
β’ (π β π β (SubGrpβπΊ)) |
61 | | pgpfac1.l |
. . . . . . . . . . 11
β’ β =
(LSSumβπΊ) |
62 | 61 | lsmsubg2 19644 |
. . . . . . . . . 10
β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β (π β π) β (SubGrpβπΊ)) |
63 | 6, 59, 60, 62 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π β π) β (SubGrpβπΊ)) |
64 | | pgpfac1.z |
. . . . . . . . . 10
β’ 0 =
(0gβπΊ) |
65 | 64 | subg0cl 18943 |
. . . . . . . . 9
β’ ((π β π) β (SubGrpβπΊ) β 0 β (π β π)) |
66 | 63, 65 | syl 17 |
. . . . . . . 8
β’ (π β 0 β (π β π)) |
67 | 66 | snssd 4774 |
. . . . . . 7
β’ (π β { 0 } β (π β π)) |
68 | 67 | adantr 482 |
. . . . . 6
β’ ((π β§ π΅ β 1o) β { 0 } β
(π β π)) |
69 | 1 | eldifad 3927 |
. . . . . . . . 9
β’ (π β πΆ β π) |
70 | 53, 69 | sseldd 3950 |
. . . . . . . 8
β’ (π β πΆ β π΅) |
71 | 70 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΅ β 1o) β πΆ β π΅) |
72 | 10, 64 | grpidcl 18785 |
. . . . . . . . 9
β’ (πΊ β Grp β 0 β π΅) |
73 | 8, 72 | syl 17 |
. . . . . . . 8
β’ (π β 0 β π΅) |
74 | | en1eqsn 9225 |
. . . . . . . 8
β’ (( 0 β π΅ β§ π΅ β 1o) β π΅ = { 0 }) |
75 | 73, 74 | sylan 581 |
. . . . . . 7
β’ ((π β§ π΅ β 1o) β π΅ = { 0 }) |
76 | 71, 75 | eleqtrd 2840 |
. . . . . 6
β’ ((π β§ π΅ β 1o) β πΆ β { 0 }) |
77 | 68, 76 | sseldd 3950 |
. . . . 5
β’ ((π β§ π΅ β 1o) β πΆ β (π β π)) |
78 | 77 | ex 414 |
. . . 4
β’ (π β (π΅ β 1o β πΆ β (π β π))) |
79 | 46, 78 | syld 47 |
. . 3
β’ (π β (Β¬ π β₯ πΈ β πΆ β (π β π))) |
80 | 2, 79 | mt3d 148 |
. 2
β’ (π β π β₯ πΈ) |
81 | | pgpfac1.oe |
. . . . 5
β’ (π β (πβπ΄) = πΈ) |
82 | 13 | nncnd 12176 |
. . . . . 6
β’ (π β πΈ β β) |
83 | 38 | nnne0d 12210 |
. . . . . 6
β’ (π β π β 0) |
84 | 82, 39, 83 | divcan1d 11939 |
. . . . 5
β’ (π β ((πΈ / π) Β· π) = πΈ) |
85 | 81, 84 | eqtr4d 2780 |
. . . 4
β’ (π β (πβπ΄) = ((πΈ / π) Β· π)) |
86 | | nndivdvds 16152 |
. . . . . . . . . . . . 13
β’ ((πΈ β β β§ π β β) β (π β₯ πΈ β (πΈ / π) β β)) |
87 | 13, 38, 86 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π β₯ πΈ β (πΈ / π) β β)) |
88 | 80, 87 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (πΈ / π) β β) |
89 | 88 | nnzd 12533 |
. . . . . . . . . 10
β’ (π β (πΈ / π) β β€) |
90 | | pgpfac1.m |
. . . . . . . . . 10
β’ (π β π β β€) |
91 | 89, 90 | zmulcld 12620 |
. . . . . . . . 9
β’ (π β ((πΈ / π) Β· π) β β€) |
92 | 55 | snssd 4774 |
. . . . . . . . . . . 12
β’ (π β {π΄} β π΅) |
93 | 50, 56, 92 | mrcssidd 17512 |
. . . . . . . . . . 11
β’ (π β {π΄} β (πΎβ{π΄})) |
94 | 93, 47 | sseqtrrdi 4000 |
. . . . . . . . . 10
β’ (π β {π΄} β π) |
95 | | snssg 4749 |
. . . . . . . . . . 11
β’ (π΄ β π β (π΄ β π β {π΄} β π)) |
96 | 54, 95 | syl 17 |
. . . . . . . . . 10
β’ (π β (π΄ β π β {π΄} β π)) |
97 | 94, 96 | mpbird 257 |
. . . . . . . . 9
β’ (π β π΄ β π) |
98 | | pgpfac1.mg |
. . . . . . . . . 10
β’ Β· =
(.gβπΊ) |
99 | 98 | subgmulgcl 18948 |
. . . . . . . . 9
β’ ((π β (SubGrpβπΊ) β§ ((πΈ / π) Β· π) β β€ β§ π΄ β π) β (((πΈ / π) Β· π) Β· π΄) β π) |
100 | 59, 91, 97, 99 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (((πΈ / π) Β· π) Β· π΄) β π) |
101 | | prmz 16558 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
102 | 5, 101 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
103 | 10, 98 | mulgcl 18900 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ π β β€ β§ πΆ β π΅) β (π Β· πΆ) β π΅) |
104 | 8, 102, 70, 103 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π Β· πΆ) β π΅) |
105 | 10, 98 | mulgcl 18900 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ π β β€ β§ π΄ β π΅) β (π Β· π΄) β π΅) |
106 | 8, 90, 55, 105 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π Β· π΄) β π΅) |
107 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(+gβπΊ) = (+gβπΊ) |
108 | 10, 98, 107 | mulgdi 19612 |
. . . . . . . . . . 11
β’ ((πΊ β Abel β§ ((πΈ / π) β β€ β§ (π Β· πΆ) β π΅ β§ (π Β· π΄) β π΅)) β ((πΈ / π) Β· ((π Β· πΆ)(+gβπΊ)(π Β· π΄))) = (((πΈ / π) Β· (π Β· πΆ))(+gβπΊ)((πΈ / π) Β· (π Β· π΄)))) |
109 | 6, 89, 104, 106, 108 | syl13anc 1373 |
. . . . . . . . . 10
β’ (π β ((πΈ / π) Β· ((π Β· πΆ)(+gβπΊ)(π Β· π΄))) = (((πΈ / π) Β· (π Β· πΆ))(+gβπΊ)((πΈ / π) Β· (π Β· π΄)))) |
110 | 84 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π β (((πΈ / π) Β· π) Β· πΆ) = (πΈ Β· πΆ)) |
111 | 10, 98 | mulgass 18920 |
. . . . . . . . . . . . 13
β’ ((πΊ β Grp β§ ((πΈ / π) β β€ β§ π β β€ β§ πΆ β π΅)) β (((πΈ / π) Β· π) Β· πΆ) = ((πΈ / π) Β· (π Β· πΆ))) |
112 | 8, 89, 102, 70, 111 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ (π β (((πΈ / π) Β· π) Β· πΆ) = ((πΈ / π) Β· (π Β· πΆ))) |
113 | 10, 11, 98, 64 | gexid 19370 |
. . . . . . . . . . . . 13
β’ (πΆ β π΅ β (πΈ Β· πΆ) = 0 ) |
114 | 70, 113 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (πΈ Β· πΆ) = 0 ) |
115 | 110, 112,
114 | 3eqtr3rd 2786 |
. . . . . . . . . . 11
β’ (π β 0 = ((πΈ / π) Β· (π Β· πΆ))) |
116 | 10, 98 | mulgass 18920 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ ((πΈ / π) β β€ β§ π β β€ β§ π΄ β π΅)) β (((πΈ / π) Β· π) Β· π΄) = ((πΈ / π) Β· (π Β· π΄))) |
117 | 8, 89, 90, 55, 116 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (π β (((πΈ / π) Β· π) Β· π΄) = ((πΈ / π) Β· (π Β· π΄))) |
118 | 115, 117 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π β ( 0 (+gβπΊ)(((πΈ / π) Β· π) Β· π΄)) = (((πΈ / π) Β· (π Β· πΆ))(+gβπΊ)((πΈ / π) Β· (π Β· π΄)))) |
119 | 10 | subgss 18936 |
. . . . . . . . . . . . 13
β’ (π β (SubGrpβπΊ) β π β π΅) |
120 | 59, 119 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
121 | 120, 100 | sseldd 3950 |
. . . . . . . . . . 11
β’ (π β (((πΈ / π) Β· π) Β· π΄) β π΅) |
122 | 10, 107, 64 | grplid 18787 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ (((πΈ / π) Β· π) Β· π΄) β π΅) β ( 0 (+gβπΊ)(((πΈ / π) Β· π) Β· π΄)) = (((πΈ / π) Β· π) Β· π΄)) |
123 | 8, 121, 122 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ( 0 (+gβπΊ)(((πΈ / π) Β· π) Β· π΄)) = (((πΈ / π) Β· π) Β· π΄)) |
124 | 109, 118,
123 | 3eqtr2d 2783 |
. . . . . . . . 9
β’ (π β ((πΈ / π) Β· ((π Β· πΆ)(+gβπΊ)(π Β· π΄))) = (((πΈ / π) Β· π) Β· π΄)) |
125 | | pgpfac1.mw |
. . . . . . . . . 10
β’ (π β ((π Β· πΆ)(+gβπΊ)(π Β· π΄)) β π) |
126 | 98 | subgmulgcl 18948 |
. . . . . . . . . 10
β’ ((π β (SubGrpβπΊ) β§ (πΈ / π) β β€ β§ ((π Β· πΆ)(+gβπΊ)(π Β· π΄)) β π) β ((πΈ / π) Β· ((π Β· πΆ)(+gβπΊ)(π Β· π΄))) β π) |
127 | 60, 89, 125, 126 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β ((πΈ / π) Β· ((π Β· πΆ)(+gβπΊ)(π Β· π΄))) β π) |
128 | 124, 127 | eqeltrrd 2839 |
. . . . . . . 8
β’ (π β (((πΈ / π) Β· π) Β· π΄) β π) |
129 | 100, 128 | elind 4159 |
. . . . . . 7
β’ (π β (((πΈ / π) Β· π) Β· π΄) β (π β© π)) |
130 | | pgpfac1.i |
. . . . . . 7
β’ (π β (π β© π) = { 0 }) |
131 | 129, 130 | eleqtrd 2840 |
. . . . . 6
β’ (π β (((πΈ / π) Β· π) Β· π΄) β { 0 }) |
132 | | elsni 4608 |
. . . . . 6
β’ ((((πΈ / π) Β· π) Β· π΄) β { 0 } β (((πΈ / π) Β· π) Β· π΄) = 0 ) |
133 | 131, 132 | syl 17 |
. . . . 5
β’ (π β (((πΈ / π) Β· π) Β· π΄) = 0 ) |
134 | | pgpfac1.o |
. . . . . . 7
β’ π = (odβπΊ) |
135 | 10, 134, 98, 64 | oddvds 19336 |
. . . . . 6
β’ ((πΊ β Grp β§ π΄ β π΅ β§ ((πΈ / π) Β· π) β β€) β ((πβπ΄) β₯ ((πΈ / π) Β· π) β (((πΈ / π) Β· π) Β· π΄) = 0 )) |
136 | 8, 55, 91, 135 | syl3anc 1372 |
. . . . 5
β’ (π β ((πβπ΄) β₯ ((πΈ / π) Β· π) β (((πΈ / π) Β· π) Β· π΄) = 0 )) |
137 | 133, 136 | mpbird 257 |
. . . 4
β’ (π β (πβπ΄) β₯ ((πΈ / π) Β· π)) |
138 | 85, 137 | eqbrtrrd 5134 |
. . 3
β’ (π β ((πΈ / π) Β· π) β₯ ((πΈ / π) Β· π)) |
139 | 88 | nnne0d 12210 |
. . . 4
β’ (π β (πΈ / π) β 0) |
140 | | dvdscmulr 16174 |
. . . 4
β’ ((π β β€ β§ π β β€ β§ ((πΈ / π) β β€ β§ (πΈ / π) β 0)) β (((πΈ / π) Β· π) β₯ ((πΈ / π) Β· π) β π β₯ π)) |
141 | 102, 90, 89, 139, 140 | syl112anc 1375 |
. . 3
β’ (π β (((πΈ / π) Β· π) β₯ ((πΈ / π) Β· π) β π β₯ π)) |
142 | 138, 141 | mpbid 231 |
. 2
β’ (π β π β₯ π) |
143 | 80, 142 | jca 513 |
1
β’ (π β (π β₯ πΈ β§ π β₯ π)) |