Step | Hyp | Ref
| Expression |
1 | | pgpfac1.c |
. . 3
β’ (π β πΆ β (π β (π β π))) |
2 | 1 | eldifbd 3928 |
. 2
β’ (π β Β¬ πΆ β (π β π)) |
3 | 1 | eldifad 3927 |
. . . . . . 7
β’ (π β πΆ β π) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ (π Β· πΆ) β (π β π)) β πΆ β π) |
5 | | pgpfac1.u |
. . . . . . . . . 10
β’ (π β π β (SubGrpβπΊ)) |
6 | | pgpfac1.p |
. . . . . . . . . . . 12
β’ (π β π pGrp πΊ) |
7 | | pgpprm 19382 |
. . . . . . . . . . . 12
β’ (π pGrp πΊ β π β β) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β β) |
9 | | prmz 16558 |
. . . . . . . . . . 11
β’ (π β β β π β
β€) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
β’ (π β π β β€) |
11 | | pgpfac1.mg |
. . . . . . . . . . 11
β’ Β· =
(.gβπΊ) |
12 | 11 | subgmulgcl 18948 |
. . . . . . . . . 10
β’ ((π β (SubGrpβπΊ) β§ π β β€ β§ πΆ β π) β (π Β· πΆ) β π) |
13 | 5, 10, 3, 12 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π Β· πΆ) β π) |
14 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ Β¬ (π Β· πΆ) β (π β π)) β (π Β· πΆ) β π) |
15 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ Β¬ (π Β· πΆ) β (π β π)) β Β¬ (π Β· πΆ) β (π β π)) |
16 | 14, 15 | eldifd 3926 |
. . . . . . 7
β’ ((π β§ Β¬ (π Β· πΆ) β (π β π)) β (π Β· πΆ) β (π β (π β π))) |
17 | | pgpfac1.k |
. . . . . . . 8
β’ πΎ =
(mrClsβ(SubGrpβπΊ)) |
18 | | pgpfac1.s |
. . . . . . . 8
β’ π = (πΎβ{π΄}) |
19 | | pgpfac1.b |
. . . . . . . 8
β’ π΅ = (BaseβπΊ) |
20 | | pgpfac1.o |
. . . . . . . 8
β’ π = (odβπΊ) |
21 | | pgpfac1.e |
. . . . . . . 8
β’ πΈ = (gExβπΊ) |
22 | | pgpfac1.z |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
23 | | pgpfac1.l |
. . . . . . . 8
β’ β =
(LSSumβπΊ) |
24 | | pgpfac1.g |
. . . . . . . 8
β’ (π β πΊ β Abel) |
25 | | pgpfac1.n |
. . . . . . . 8
β’ (π β π΅ β Fin) |
26 | | pgpfac1.oe |
. . . . . . . 8
β’ (π β (πβπ΄) = πΈ) |
27 | | pgpfac1.au |
. . . . . . . 8
β’ (π β π΄ β π) |
28 | | pgpfac1.w |
. . . . . . . 8
β’ (π β π β (SubGrpβπΊ)) |
29 | | pgpfac1.i |
. . . . . . . 8
β’ (π β (π β© π) = { 0 }) |
30 | | pgpfac1.ss |
. . . . . . . 8
β’ (π β (π β π) β π) |
31 | | pgpfac1.2 |
. . . . . . . 8
β’ (π β βπ€ β (SubGrpβπΊ)((π€ β π β§ π΄ β π€) β Β¬ (π β π) β π€)) |
32 | 17, 18, 19, 20, 21, 22, 23, 6, 24, 25, 26, 5, 27, 28, 29, 30, 31 | pgpfac1lem1 19860 |
. . . . . . 7
β’ ((π β§ (π Β· πΆ) β (π β (π β π))) β ((π β π) β (πΎβ{(π Β· πΆ)})) = π) |
33 | 16, 32 | syldan 592 |
. . . . . 6
β’ ((π β§ Β¬ (π Β· πΆ) β (π β π)) β ((π β π) β (πΎβ{(π Β· πΆ)})) = π) |
34 | 4, 33 | eleqtrrd 2841 |
. . . . 5
β’ ((π β§ Β¬ (π Β· πΆ) β (π β π)) β πΆ β ((π β π) β (πΎβ{(π Β· πΆ)}))) |
35 | 34 | ex 414 |
. . . 4
β’ (π β (Β¬ (π Β· πΆ) β (π β π) β πΆ β ((π β π) β (πΎβ{(π Β· πΆ)})))) |
36 | | eqid 2737 |
. . . . . 6
β’
(-gβπΊ) = (-gβπΊ) |
37 | | ablgrp 19574 |
. . . . . . . . . . . 12
β’ (πΊ β Abel β πΊ β Grp) |
38 | 24, 37 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΊ β Grp) |
39 | 19 | subgacs 18970 |
. . . . . . . . . . 11
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβπ΅)) |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
β’ (π β (SubGrpβπΊ) β (ACSβπ΅)) |
41 | 40 | acsmred 17543 |
. . . . . . . . 9
β’ (π β (SubGrpβπΊ) β (Mooreβπ΅)) |
42 | 19 | subgss 18936 |
. . . . . . . . . . 11
β’ (π β (SubGrpβπΊ) β π β π΅) |
43 | 5, 42 | syl 17 |
. . . . . . . . . 10
β’ (π β π β π΅) |
44 | 43, 27 | sseldd 3950 |
. . . . . . . . 9
β’ (π β π΄ β π΅) |
45 | 17 | mrcsncl 17499 |
. . . . . . . . 9
β’
(((SubGrpβπΊ)
β (Mooreβπ΅)
β§ π΄ β π΅) β (πΎβ{π΄}) β (SubGrpβπΊ)) |
46 | 41, 44, 45 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΎβ{π΄}) β (SubGrpβπΊ)) |
47 | 18, 46 | eqeltrid 2842 |
. . . . . . 7
β’ (π β π β (SubGrpβπΊ)) |
48 | 23 | lsmsubg2 19644 |
. . . . . . 7
β’ ((πΊ β Abel β§ π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ)) β (π β π) β (SubGrpβπΊ)) |
49 | 24, 47, 28, 48 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β π) β (SubGrpβπΊ)) |
50 | 43, 13 | sseldd 3950 |
. . . . . . 7
β’ (π β (π Β· πΆ) β π΅) |
51 | 17 | mrcsncl 17499 |
. . . . . . 7
β’
(((SubGrpβπΊ)
β (Mooreβπ΅)
β§ (π Β· πΆ) β π΅) β (πΎβ{(π Β· πΆ)}) β (SubGrpβπΊ)) |
52 | 41, 50, 51 | syl2anc 585 |
. . . . . 6
β’ (π β (πΎβ{(π Β· πΆ)}) β (SubGrpβπΊ)) |
53 | 36, 23, 49, 52 | lsmelvalm 19440 |
. . . . 5
β’ (π β (πΆ β ((π β π) β (πΎβ{(π Β· πΆ)})) β βπ β (π β π)βπ‘ β (πΎβ{(π Β· πΆ)})πΆ = (π (-gβπΊ)π‘))) |
54 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β β€ β¦ (π Β· (π Β· πΆ))) = (π β β€ β¦ (π Β· (π Β· πΆ))) |
55 | 19, 11, 54, 17 | cycsubg2 19010 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ (π Β· πΆ) β π΅) β (πΎβ{(π Β· πΆ)}) = ran (π β β€ β¦ (π Β· (π Β· πΆ)))) |
56 | 38, 50, 55 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΎβ{(π Β· πΆ)}) = ran (π β β€ β¦ (π Β· (π Β· πΆ)))) |
57 | 56 | rexeqdv 3317 |
. . . . . . 7
β’ (π β (βπ‘ β (πΎβ{(π Β· πΆ)})πΆ = (π (-gβπΊ)π‘) β βπ‘ β ran (π β β€ β¦ (π Β· (π Β· πΆ)))πΆ = (π (-gβπΊ)π‘))) |
58 | | ovex 7395 |
. . . . . . . . 9
β’ (π Β· (π Β· πΆ)) β V |
59 | 58 | rgenw 3069 |
. . . . . . . 8
β’
βπ β
β€ (π Β· (π Β· πΆ)) β V |
60 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π‘ = (π Β· (π Β· πΆ)) β (π (-gβπΊ)π‘) = (π (-gβπΊ)(π Β· (π Β· πΆ)))) |
61 | 60 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π‘ = (π Β· (π Β· πΆ)) β (πΆ = (π (-gβπΊ)π‘) β πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))))) |
62 | 54, 61 | rexrnmptw 7050 |
. . . . . . . 8
β’
(βπ β
β€ (π Β· (π Β· πΆ)) β V β (βπ‘ β ran (π β β€ β¦ (π Β· (π Β· πΆ)))πΆ = (π (-gβπΊ)π‘) β βπ β β€ πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))))) |
63 | 59, 62 | mp1i 13 |
. . . . . . 7
β’ (π β (βπ‘ β ran (π β β€ β¦ (π Β· (π Β· πΆ)))πΆ = (π (-gβπΊ)π‘) β βπ β β€ πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))))) |
64 | 57, 63 | bitrd 279 |
. . . . . 6
β’ (π β (βπ‘ β (πΎβ{(π Β· πΆ)})πΆ = (π (-gβπΊ)π‘) β βπ β β€ πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))))) |
65 | 64 | rexbidv 3176 |
. . . . 5
β’ (π β (βπ β (π β π)βπ‘ β (πΎβ{(π Β· πΆ)})πΆ = (π (-gβπΊ)π‘) β βπ β (π β π)βπ β β€ πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))))) |
66 | | rexcom 3276 |
. . . . . 6
β’
(βπ β
(π β π)βπ β β€ πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))) β βπ β β€ βπ β (π β π)πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ)))) |
67 | 38 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β (π β π)) β πΊ β Grp) |
68 | 30, 43 | sstrd 3959 |
. . . . . . . . . . . . . 14
β’ (π β (π β π) β π΅) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β€) β (π β π) β π΅) |
70 | 69 | sselda 3949 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β (π β π)) β π β π΅) |
71 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β (π β π)) β π β β€) |
72 | 50 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β (π β π)) β (π Β· πΆ) β π΅) |
73 | 19, 11 | mulgcl 18900 |
. . . . . . . . . . . . 13
β’ ((πΊ β Grp β§ π β β€ β§ (π Β· πΆ) β π΅) β (π Β· (π Β· πΆ)) β π΅) |
74 | 67, 71, 72, 73 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β (π β π)) β (π Β· (π Β· πΆ)) β π΅) |
75 | 43, 3 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ (π β πΆ β π΅) |
76 | 75 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β (π β π)) β πΆ β π΅) |
77 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(+gβπΊ) = (+gβπΊ) |
78 | 19, 77, 36 | grpsubadd 18842 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ (π β π΅ β§ (π Β· (π Β· πΆ)) β π΅ β§ πΆ β π΅)) β ((π (-gβπΊ)(π Β· (π Β· πΆ))) = πΆ β (πΆ(+gβπΊ)(π Β· (π Β· πΆ))) = π )) |
79 | 67, 70, 74, 76, 78 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((π β§ π β β€) β§ π β (π β π)) β ((π (-gβπΊ)(π Β· (π Β· πΆ))) = πΆ β (πΆ(+gβπΊ)(π Β· (π Β· πΆ))) = π )) |
80 | | 1zzd 12541 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β€) β§ π β (π β π)) β 1 β β€) |
81 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β€) β§ π β (π β π)) β π β β€) |
82 | 71, 81 | zmulcld 12620 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β€) β§ π β (π β π)) β (π Β· π) β β€) |
83 | 19, 11, 77 | mulgdir 18915 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ (1 β
β€ β§ (π Β·
π) β β€ β§
πΆ β π΅)) β ((1 + (π Β· π)) Β· πΆ) = ((1 Β· πΆ)(+gβπΊ)((π Β· π) Β· πΆ))) |
84 | 67, 80, 82, 76, 83 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β (π β π)) β ((1 + (π Β· π)) Β· πΆ) = ((1 Β· πΆ)(+gβπΊ)((π Β· π) Β· πΆ))) |
85 | 19, 11 | mulg1 18890 |
. . . . . . . . . . . . . . 15
β’ (πΆ β π΅ β (1 Β· πΆ) = πΆ) |
86 | 76, 85 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β€) β§ π β (π β π)) β (1 Β· πΆ) = πΆ) |
87 | 19, 11 | mulgass 18920 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β Grp β§ (π β β€ β§ π β β€ β§ πΆ β π΅)) β ((π Β· π) Β· πΆ) = (π Β· (π Β· πΆ))) |
88 | 67, 71, 81, 76, 87 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β€) β§ π β (π β π)) β ((π Β· π) Β· πΆ) = (π Β· (π Β· πΆ))) |
89 | 86, 88 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β (π β π)) β ((1 Β· πΆ)(+gβπΊ)((π Β· π) Β· πΆ)) = (πΆ(+gβπΊ)(π Β· (π Β· πΆ)))) |
90 | 84, 89 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β (π β π)) β ((1 + (π Β· π)) Β· πΆ) = (πΆ(+gβπΊ)(π Β· (π Β· πΆ)))) |
91 | 90 | eqeq1d 2739 |
. . . . . . . . . . 11
β’ (((π β§ π β β€) β§ π β (π β π)) β (((1 + (π Β· π)) Β· πΆ) = π β (πΆ(+gβπΊ)(π Β· (π Β· πΆ))) = π )) |
92 | 79, 91 | bitr4d 282 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ π β (π β π)) β ((π (-gβπΊ)(π Β· (π Β· πΆ))) = πΆ β ((1 + (π Β· π)) Β· πΆ) = π )) |
93 | | eqcom 2744 |
. . . . . . . . . 10
β’ (πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))) β (π (-gβπΊ)(π Β· (π Β· πΆ))) = πΆ) |
94 | | eqcom 2744 |
. . . . . . . . . 10
β’ (π = ((1 + (π Β· π)) Β· πΆ) β ((1 + (π Β· π)) Β· πΆ) = π ) |
95 | 92, 93, 94 | 3bitr4g 314 |
. . . . . . . . 9
β’ (((π β§ π β β€) β§ π β (π β π)) β (πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))) β π = ((1 + (π Β· π)) Β· πΆ))) |
96 | 95 | rexbidva 3174 |
. . . . . . . 8
β’ ((π β§ π β β€) β (βπ β (π β π)πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))) β βπ β (π β π)π = ((1 + (π Β· π)) Β· πΆ))) |
97 | | risset 3224 |
. . . . . . . 8
β’ (((1 +
(π Β· π)) Β· πΆ) β (π β π) β βπ β (π β π)π = ((1 + (π Β· π)) Β· πΆ)) |
98 | 96, 97 | bitr4di 289 |
. . . . . . 7
β’ ((π β§ π β β€) β (βπ β (π β π)πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))) β ((1 + (π Β· π)) Β· πΆ) β (π β π))) |
99 | 98 | rexbidva 3174 |
. . . . . 6
β’ (π β (βπ β β€ βπ β (π β π)πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))) β βπ β β€ ((1 + (π Β· π)) Β· πΆ) β (π β π))) |
100 | 66, 99 | bitrid 283 |
. . . . 5
β’ (π β (βπ β (π β π)βπ β β€ πΆ = (π (-gβπΊ)(π Β· (π Β· πΆ))) β βπ β β€ ((1 + (π Β· π)) Β· πΆ) β (π β π))) |
101 | 53, 65, 100 | 3bitrd 305 |
. . . 4
β’ (π β (πΆ β ((π β π) β (πΎβ{(π Β· πΆ)})) β βπ β β€ ((1 + (π Β· π)) Β· πΆ) β (π β π))) |
102 | 35, 101 | sylibd 238 |
. . 3
β’ (π β (Β¬ (π Β· πΆ) β (π β π) β βπ β β€ ((1 + (π Β· π)) Β· πΆ) β (π β π))) |
103 | 38 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β€) β πΊ β Grp) |
104 | 75 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β€) β πΆ β π΅) |
105 | | 1z 12540 |
. . . . . . 7
β’ 1 β
β€ |
106 | | id 22 |
. . . . . . . 8
β’ (π β β€ β π β
β€) |
107 | | zmulcl 12559 |
. . . . . . . 8
β’ ((π β β€ β§ π β β€) β (π Β· π) β β€) |
108 | 106, 10, 107 | syl2anr 598 |
. . . . . . 7
β’ ((π β§ π β β€) β (π Β· π) β β€) |
109 | | zaddcl 12550 |
. . . . . . 7
β’ ((1
β β€ β§ (π
Β· π) β β€)
β (1 + (π Β·
π)) β
β€) |
110 | 105, 108,
109 | sylancr 588 |
. . . . . 6
β’ ((π β§ π β β€) β (1 + (π Β· π)) β β€) |
111 | 19, 20 | odcl 19325 |
. . . . . . . . 9
β’ (πΆ β π΅ β (πβπΆ) β
β0) |
112 | 104, 111 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β€) β (πβπΆ) β
β0) |
113 | 112 | nn0zd 12532 |
. . . . . . 7
β’ ((π β§ π β β€) β (πβπΆ) β β€) |
114 | | hashcl 14263 |
. . . . . . . . . 10
β’ (π΅ β Fin β
(β―βπ΅) β
β0) |
115 | 25, 114 | syl 17 |
. . . . . . . . 9
β’ (π β (β―βπ΅) β
β0) |
116 | 115 | nn0zd 12532 |
. . . . . . . 8
β’ (π β (β―βπ΅) β
β€) |
117 | 116 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β€) β (β―βπ΅) β
β€) |
118 | 110, 117 | gcdcomd 16401 |
. . . . . . . 8
β’ ((π β§ π β β€) β ((1 + (π Β· π)) gcd (β―βπ΅)) = ((β―βπ΅) gcd (1 + (π Β· π)))) |
119 | 19 | pgphash 19396 |
. . . . . . . . . . 11
β’ ((π pGrp πΊ β§ π΅ β Fin) β (β―βπ΅) = (πβ(π pCnt (β―βπ΅)))) |
120 | 6, 25, 119 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (β―βπ΅) = (πβ(π pCnt (β―βπ΅)))) |
121 | 120 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β€) β (β―βπ΅) = (πβ(π pCnt (β―βπ΅)))) |
122 | 121 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β§ π β β€) β ((β―βπ΅) gcd (1 + (π Β· π))) = ((πβ(π pCnt (β―βπ΅))) gcd (1 + (π Β· π)))) |
123 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β π β β€) |
124 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β π β β€) |
125 | | 1zzd 12541 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β 1 β
β€) |
126 | | gcdaddm 16412 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β€ β§ 1 β
β€) β (π gcd 1) =
(π gcd (1 + (π Β· π)))) |
127 | 123, 124,
125, 126 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π β β€) β (π gcd 1) = (π gcd (1 + (π Β· π)))) |
128 | | gcd1 16415 |
. . . . . . . . . . 11
β’ (π β β€ β (π gcd 1) = 1) |
129 | 124, 128 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β€) β (π gcd 1) = 1) |
130 | 127, 129 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π β§ π β β€) β (π gcd (1 + (π Β· π))) = 1) |
131 | 19 | grpbn0 18786 |
. . . . . . . . . . . . . 14
β’ (πΊ β Grp β π΅ β β
) |
132 | 38, 131 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π΅ β β
) |
133 | | hashnncl 14273 |
. . . . . . . . . . . . . 14
β’ (π΅ β Fin β
((β―βπ΅) β
β β π΅ β
β
)) |
134 | 25, 133 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β ((β―βπ΅) β β β π΅ β β
)) |
135 | 132, 134 | mpbird 257 |
. . . . . . . . . . . 12
β’ (π β (β―βπ΅) β
β) |
136 | 8, 135 | pccld 16729 |
. . . . . . . . . . 11
β’ (π β (π pCnt (β―βπ΅)) β
β0) |
137 | 136 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β€) β (π pCnt (β―βπ΅)) β
β0) |
138 | | rpexp1i 16606 |
. . . . . . . . . 10
β’ ((π β β€ β§ (1 +
(π Β· π)) β β€ β§ (π pCnt (β―βπ΅)) β β0)
β ((π gcd (1 + (π Β· π))) = 1 β ((πβ(π pCnt (β―βπ΅))) gcd (1 + (π Β· π))) = 1)) |
139 | 124, 110,
137, 138 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β β€) β ((π gcd (1 + (π Β· π))) = 1 β ((πβ(π pCnt (β―βπ΅))) gcd (1 + (π Β· π))) = 1)) |
140 | 130, 139 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π β β€) β ((πβ(π pCnt (β―βπ΅))) gcd (1 + (π Β· π))) = 1) |
141 | 118, 122,
140 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ π β β€) β ((1 + (π Β· π)) gcd (β―βπ΅)) = 1) |
142 | 19, 20 | oddvds2 19355 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π΅ β Fin β§ πΆ β π΅) β (πβπΆ) β₯ (β―βπ΅)) |
143 | 38, 25, 75, 142 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (πβπΆ) β₯ (β―βπ΅)) |
144 | 143 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β€) β (πβπΆ) β₯ (β―βπ΅)) |
145 | | rpdvds 16543 |
. . . . . . 7
β’ ((((1 +
(π Β· π)) β β€ β§ (πβπΆ) β β€ β§ (β―βπ΅) β β€) β§ (((1 +
(π Β· π)) gcd (β―βπ΅)) = 1 β§ (πβπΆ) β₯ (β―βπ΅))) β ((1 + (π Β· π)) gcd (πβπΆ)) = 1) |
146 | 110, 113,
117, 141, 144, 145 | syl32anc 1379 |
. . . . . 6
β’ ((π β§ π β β€) β ((1 + (π Β· π)) gcd (πβπΆ)) = 1) |
147 | 19, 20, 11 | odbezout 19347 |
. . . . . 6
β’ (((πΊ β Grp β§ πΆ β π΅ β§ (1 + (π Β· π)) β β€) β§ ((1 + (π Β· π)) gcd (πβπΆ)) = 1) β βπ β β€ (π Β· ((1 + (π Β· π)) Β· πΆ)) = πΆ) |
148 | 103, 104,
110, 146, 147 | syl31anc 1374 |
. . . . 5
β’ ((π β§ π β β€) β βπ β β€ (π Β· ((1 + (π Β· π)) Β· πΆ)) = πΆ) |
149 | 49 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ π β β€) β (π β π) β (SubGrpβπΊ)) |
150 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ π β β€) β π β β€) |
151 | 11 | subgmulgcl 18948 |
. . . . . . . . 9
β’ (((π β π) β (SubGrpβπΊ) β§ π β β€ β§ ((1 + (π Β· π)) Β· πΆ) β (π β π)) β (π Β· ((1 + (π Β· π)) Β· πΆ)) β (π β π)) |
152 | 151 | 3expia 1122 |
. . . . . . . 8
β’ (((π β π) β (SubGrpβπΊ) β§ π β β€) β (((1 + (π Β· π)) Β· πΆ) β (π β π) β (π Β· ((1 + (π Β· π)) Β· πΆ)) β (π β π))) |
153 | 149, 150,
152 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β β€) β§ π β β€) β (((1 + (π Β· π)) Β· πΆ) β (π β π) β (π Β· ((1 + (π Β· π)) Β· πΆ)) β (π β π))) |
154 | | eleq1 2826 |
. . . . . . . 8
β’ ((π Β· ((1 + (π Β· π)) Β· πΆ)) = πΆ β ((π Β· ((1 + (π Β· π)) Β· πΆ)) β (π β π) β πΆ β (π β π))) |
155 | 154 | imbi2d 341 |
. . . . . . 7
β’ ((π Β· ((1 + (π Β· π)) Β· πΆ)) = πΆ β ((((1 + (π Β· π)) Β· πΆ) β (π β π) β (π Β· ((1 + (π Β· π)) Β· πΆ)) β (π β π)) β (((1 + (π Β· π)) Β· πΆ) β (π β π) β πΆ β (π β π)))) |
156 | 153, 155 | syl5ibcom 244 |
. . . . . 6
β’ (((π β§ π β β€) β§ π β β€) β ((π Β· ((1 + (π Β· π)) Β· πΆ)) = πΆ β (((1 + (π Β· π)) Β· πΆ) β (π β π) β πΆ β (π β π)))) |
157 | 156 | rexlimdva 3153 |
. . . . 5
β’ ((π β§ π β β€) β (βπ β β€ (π Β· ((1 + (π Β· π)) Β· πΆ)) = πΆ β (((1 + (π Β· π)) Β· πΆ) β (π β π) β πΆ β (π β π)))) |
158 | 148, 157 | mpd 15 |
. . . 4
β’ ((π β§ π β β€) β (((1 + (π Β· π)) Β· πΆ) β (π β π) β πΆ β (π β π))) |
159 | 158 | rexlimdva 3153 |
. . 3
β’ (π β (βπ β β€ ((1 + (π Β· π)) Β· πΆ) β (π β π) β πΆ β (π β π))) |
160 | 102, 159 | syld 47 |
. 2
β’ (π β (Β¬ (π Β· πΆ) β (π β π) β πΆ β (π β π))) |
161 | 2, 160 | mt3d 148 |
1
β’ (π β (π Β· πΆ) β (π β π)) |