Step | Hyp | Ref
| Expression |
1 | | pgpfi.1 |
. . . 4
|
2 | | eqid 2622 |
. . . 4
|
3 | 1, 2 | ispgp 18007 |
. . 3
pGrp
|
4 | | simprl 794 |
. . . . . 6
|
5 | 1 | grpbn0 17451 |
. . . . . . . . . . 11
|
6 | 5 | ad2antrr 762 |
. . . . . . . . . 10
|
7 | | hashnncl 13157 |
. . . . . . . . . . 11
|
8 | 7 | ad2antlr 763 |
. . . . . . . . . 10
|
9 | 6, 8 | mpbird 247 |
. . . . . . . . 9
|
10 | 4, 9 | pccld 15555 |
. . . . . . . 8
|
11 | 10 | nn0red 11352 |
. . . . . . . . . . . . . . 15
|
12 | 11 | leidd 10594 |
. . . . . . . . . . . . . 14
|
13 | 10 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
|
14 | | pcid 15577 |
. . . . . . . . . . . . . . 15
|
15 | 4, 13, 14 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
16 | 12, 15 | breqtrrd 4681 |
. . . . . . . . . . . . 13
|
17 | 16 | ad2antrr 762 |
. . . . . . . . . . . 12
|
18 | | simpr 477 |
. . . . . . . . . . . . 13
|
19 | 18 | oveq1d 6665 |
. . . . . . . . . . . 12
|
20 | 18 | oveq1d 6665 |
. . . . . . . . . . . 12
|
21 | 17, 19, 20 | 3brtr4d 4685 |
. . . . . . . . . . 11
|
22 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . 18
|
23 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
|
24 | 23 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
25 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
|
26 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
27 | 1, 2 | odcau 18019 |
. . . . . . . . . . . . . . . . . 18
|
28 | 22, 24, 25, 26, 27 | syl31anc 1329 |
. . . . . . . . . . . . . . . . 17
|
29 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | | iddvds 14995 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 32, 33 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . 19
|
35 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
37 | 36 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
38 | 37 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
39 | 38 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . . 22
|
40 | 35, 39 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | 40 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | 4 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
44 | 29, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
45 | 33, 44 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | | pcprmpw 15587 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | 42, 45, 46 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
48 | 41, 47 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 34, 48 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
|
50 | 42, 45 | pccld 15555 |
. . . . . . . . . . . . . . . . . . 19
|
51 | | prmdvdsexpr 15429 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 29, 42, 50, 51 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
54 | 28, 53 | rexlimddv 3035 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | ex 450 |
. . . . . . . . . . . . . . 15
|
56 | 55 | necon3ad 2807 |
. . . . . . . . . . . . . 14
|
57 | 56 | imp 445 |
. . . . . . . . . . . . 13
|
58 | | simplr 792 |
. . . . . . . . . . . . . 14
|
59 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
60 | | pceq0 15575 |
. . . . . . . . . . . . . 14
|
61 | 58, 59, 60 | syl2anc 693 |
. . . . . . . . . . . . 13
|
62 | 57, 61 | mpbird 247 |
. . . . . . . . . . . 12
|
63 | | prmnn 15388 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
|
65 | 64, 10 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
|
66 | 65 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
67 | 58, 66 | pccld 15555 |
. . . . . . . . . . . . 13
|
68 | 67 | nn0ge0d 11354 |
. . . . . . . . . . . 12
|
69 | 62, 68 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
70 | 21, 69 | pm2.61dane 2881 |
. . . . . . . . . 10
|
71 | 70 | ralrimiva 2966 |
. . . . . . . . 9
|
72 | | hashcl 13147 |
. . . . . . . . . . . 12
|
73 | 72 | ad2antlr 763 |
. . . . . . . . . . 11
|
74 | 73 | nn0zd 11480 |
. . . . . . . . . 10
|
75 | 65 | nnzd 11481 |
. . . . . . . . . 10
|
76 | | pc2dvds 15583 |
. . . . . . . . . 10
|
77 | 74, 75, 76 | syl2anc 693 |
. . . . . . . . 9
|
78 | 71, 77 | mpbird 247 |
. . . . . . . 8
|
79 | | oveq2 6658 |
. . . . . . . . . 10
|
80 | 79 | breq2d 4665 |
. . . . . . . . 9
|
81 | 80 | rspcev 3309 |
. . . . . . . 8
|
82 | 10, 78, 81 | syl2anc 693 |
. . . . . . 7
|
83 | | pcprmpw2 15586 |
. . . . . . . . 9
|
84 | | pcprmpw 15587 |
. . . . . . . . 9
|
85 | 83, 84 | bitr4d 271 |
. . . . . . . 8
|
86 | 4, 9, 85 | syl2anc 693 |
. . . . . . 7
|
87 | 82, 86 | mpbid 222 |
. . . . . 6
|
88 | 4, 87 | jca 554 |
. . . . 5
|
89 | 88 | 3adantr2 1221 |
. . . 4
|
90 | 89 | ex 450 |
. . 3
|
91 | 3, 90 | syl5bi 232 |
. 2
pGrp |
92 | 1 | pgpfi1 18010 |
. . . . . 6
pGrp |
93 | 92 | 3expia 1267 |
. . . . 5
pGrp |
94 | 93 | rexlimdv 3030 |
. . . 4
pGrp |
95 | 94 | expimpd 629 |
. . 3
pGrp |
96 | 95 | adantr 481 |
. 2
pGrp
|
97 | 91, 96 | impbid 202 |
1
pGrp
|