Step | Hyp | Ref
| Expression |
1 | | sylow2a.y |
. . . . 5
   |
2 | | pwfi 7887 |
. . . . 5

   |
3 | 1, 2 | sylib 201 |
. . . 4
    |
4 | | sylow2a.m |
. . . . . 6

    |
5 | | sylow2a.r |
. . . . . . 7
   
    
     |
6 | | sylow2a.x |
. . . . . . 7
     |
7 | 5, 6 | gaorber 17040 |
. . . . . 6
 
  |
8 | 4, 7 | syl 17 |
. . . . 5
   |
9 | 8 | qsss 7442 |
. . . 4
      |
10 | | ssfi 7810 |
. . . 4
           |
11 | 3, 9, 10 | syl2anc 673 |
. . 3
  
  |
12 | | diffi 7821 |
. . 3
  
       |
13 | 11, 12 | syl 17 |
. 2
        |
14 | | sylow2a.p |
. . . . 5
 pGrp   |
15 | | gagrp 17024 |
. . . . . . 7
    |
16 | 4, 15 | syl 17 |
. . . . . 6
   |
17 | | sylow2a.f |
. . . . . 6
   |
18 | 6 | pgpfi 17335 |
. . . . . 6
 
  pGrp

             |
19 | 16, 17, 18 | syl2anc 673 |
. . . . 5
  pGrp

             |
20 | 14, 19 | mpbid 215 |
. . . 4
              |
21 | 20 | simpld 466 |
. . 3
   |
22 | | prmz 14705 |
. . 3

  |
23 | 21, 22 | syl 17 |
. 2
   |
24 | | eldifi 3544 |
. . . . 5
          |
25 | 1 | adantr 472 |
. . . . . 6
 
  
  |
26 | 9 | sselda 3418 |
. . . . . . 7
 
  
   |
27 | 26 | elpwid 3952 |
. . . . . 6
 
  
  |
28 | | ssfi 7810 |
. . . . . 6
     |
29 | 25, 27, 28 | syl2anc 673 |
. . . . 5
 
  
  |
30 | 24, 29 | sylan2 482 |
. . . 4
 
        |
31 | | hashcl 12576 |
. . . 4
       |
32 | 30, 31 | syl 17 |
. . 3
 
            |
33 | 32 | nn0zd 11061 |
. 2
 
            |
34 | | eldif 3400 |
. . 3
     
       |
35 | | eqid 2471 |
. . . . 5
     |
36 | | sseq1 3439 |
. . . . . . . 8
     
   |
37 | | selpw 3949 |
. . . . . . . 8
 
  |
38 | 36, 37 | syl6bbr 271 |
. . . . . . 7
     
    |
39 | 38 | notbid 301 |
. . . . . 6
          |
40 | | fveq2 5879 |
. . . . . . 7
              |
41 | 40 | breq2d 4407 |
. . . . . 6
        
       |
42 | 39, 41 | imbi12d 327 |
. . . . 5
      
     

         |
43 | 21 | adantr 472 |
. . . . . . . . . 10
 
   |
44 | 8 | adantr 472 |
. . . . . . . . . . . . . 14
 
   |
45 | | simpr 468 |
. . . . . . . . . . . . . 14
 
   |
46 | 44, 45 | erref 7401 |
. . . . . . . . . . . . 13
 
   |
47 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
48 | 47, 47 | elec 7421 |
. . . . . . . . . . . . 13
     |
49 | 46, 48 | sylibr 217 |
. . . . . . . . . . . 12
 
    |
50 | | ne0i 3728 |
. . . . . . . . . . . 12
       |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
 
     |
52 | 8 | ecss 7423 |
. . . . . . . . . . . . . 14
     |
53 | | ssfi 7810 |
. . . . . . . . . . . . . 14
    
    |
54 | 1, 52, 53 | syl2anc 673 |
. . . . . . . . . . . . 13
     |
55 | 54 | adantr 472 |
. . . . . . . . . . . 12
 
     |
56 | | hashnncl 12585 |
. . . . . . . . . . . 12
        
     |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
 
            |
58 | 51, 57 | mpbird 240 |
. . . . . . . . . 10
 
     
  |
59 | | pceq0 14899 |
. . . . . . . . . 10
      
                 |
60 | 43, 58, 59 | syl2anc 673 |
. . . . . . . . 9
 
        
        |
61 | | oveq2 6316 |
. . . . . . . . . 10
 
                       |
62 | | hashcl 12576 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
63 | 54, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
        |
64 | 63 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . . . 20
        |
65 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
66 | | ssfi 7810 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
    |
67 | 17, 65, 66 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
68 | | hashcl 12576 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
           |
70 | 69 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . . . 20
           |
71 | | dvdsmul1 14401 |
. . . . . . . . . . . . . . . . . . . 20
                                      |
72 | 64, 70, 71 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
                       |
73 | 72 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
     
                 |
74 | 4 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
     |
75 | 17 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
   |
76 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
77 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
 ~QG       ~QG  
    |
78 | 6, 76, 77, 5 | orbsta2 17046 |
. . . . . . . . . . . . . . . . . . 19
 
 

                      |
79 | 74, 45, 75, 78 | syl21anc 1291 |
. . . . . . . . . . . . . . . . . 18
 
                      |
80 | 73, 79 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . 17
 
     
      |
81 | 20 | simprd 470 |
. . . . . . . . . . . . . . . . . 18
            |
82 | 81 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
            |
83 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . 19
                  
            |
84 | 83 | biimpcd 232 |
. . . . . . . . . . . . . . . . . 18
                               |
85 | 84 | reximdv 2857 |
. . . . . . . . . . . . . . . . 17
                    
            |
86 | 80, 82, 85 | sylc 61 |
. . . . . . . . . . . . . . . 16
 
             |
87 | | pcprmpw2 14910 |
. . . . . . . . . . . . . . . . 17
      
                               |
88 | 43, 58, 87 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
 
  
        
                   |
89 | 86, 88 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
     
             |
90 | 89 | eqcomd 2477 |
. . . . . . . . . . . . . 14
 
                   |
91 | 23 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
   |
92 | 91 | zcnd 11064 |
. . . . . . . . . . . . . . . 16
 
   |
93 | 92 | exp0d 12448 |
. . . . . . . . . . . . . . 15
 
       |
94 | | hash1 12619 |
. . . . . . . . . . . . . . 15
     |
95 | 93, 94 | syl6eqr 2523 |
. . . . . . . . . . . . . 14
 
           |
96 | 90, 95 | eqeq12d 2486 |
. . . . . . . . . . . . 13
 
                             |
97 | | df1o2 7212 |
. . . . . . . . . . . . . . 15
   |
98 | | snfi 7668 |
. . . . . . . . . . . . . . 15
   |
99 | 97, 98 | eqeltri 2545 |
. . . . . . . . . . . . . 14
 |
100 | | hashen 12568 |
. . . . . . . . . . . . . 14
    
               |
101 | 55, 99, 100 | sylancl 675 |
. . . . . . . . . . . . 13
 
                |
102 | 96, 101 | bitrd 261 |
. . . . . . . . . . . 12
 
                      |
103 | | en1b 7655 |
. . . . . . . . . . . 12
           |
104 | 102, 103 | syl6bb 269 |
. . . . . . . . . . 11
 
                          |
105 | 45 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
            
  |
106 | 4 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
                 |
107 | 6 | gaf 17027 |
. . . . . . . . . . . . . . . . . . . 20
         |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                    |
109 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
            
  |
110 | 108, 109,
105 | fovrnd 6460 |
. . . . . . . . . . . . . . . . . 18
                 |
111 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
  
  |
112 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . 21
       |
113 | 112 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . 20
             |
114 | 113 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . 19
  
    
  
   |
115 | 109, 111,
114 | sylancl 675 |
. . . . . . . . . . . . . . . . . 18
             
      |
116 | 5 | gaorb 17039 |
. . . . . . . . . . . . . . . . . 18
              |
117 | 105, 110,
115, 116 | syl3anbrc 1214 |
. . . . . . . . . . . . . . . . 17
                 |
118 | | ovex 6336 |
. . . . . . . . . . . . . . . . . 18
   |
119 | 118, 47 | elec 7421 |
. . . . . . . . . . . . . . . . 17
 
       |
120 | 117, 119 | sylibr 217 |
. . . . . . . . . . . . . . . 16
                  |
121 | | simprr 774 |
. . . . . . . . . . . . . . . 16
                     |
122 | 120, 121 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
                     |
123 | 118 | elsnc 3984 |
. . . . . . . . . . . . . . 15
 
    
      |
124 | 122, 123 | sylib 201 |
. . . . . . . . . . . . . 14
                   |
125 | 49 | adantr 472 |
. . . . . . . . . . . . . . . 16
            
   |
126 | 125, 121 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
            
      |
127 | 47 | elsnc 3984 |
. . . . . . . . . . . . . . 15
         |
128 | 126, 127 | sylib 201 |
. . . . . . . . . . . . . 14
            
    |
129 | 124, 128 | eqtr4d 2508 |
. . . . . . . . . . . . 13
                 |
130 | 129 | expr 626 |
. . . . . . . . . . . 12
                 |
131 | 130 | ralrimdva 2812 |
. . . . . . . . . . 11
 
        
     |
132 | 104, 131 | sylbid 223 |
. . . . . . . . . 10
 
                  
    |
133 | 61, 132 | syl5 32 |
. . . . . . . . 9
 
          
    |
134 | 60, 133 | sylbird 243 |
. . . . . . . 8
 
 
      
    |
135 | | oveq2 6316 |
. . . . . . . . . . . . 13
       |
136 | | id 22 |
. . . . . . . . . . . . 13
   |
137 | 135, 136 | eqeq12d 2486 |
. . . . . . . . . . . 12
   
     |
138 | 137 | ralbidv 2829 |
. . . . . . . . . . 11
  



     |
139 | | sylow2a.z |
. . . . . . . . . . 11
  
   |
140 | 138, 139 | elrab2 3186 |
. . . . . . . . . 10



     |
141 | 140 | baib 919 |
. . . . . . . . 9
 

     |
142 | 141 | adantl 473 |
. . . . . . . 8
 
 

     |
143 | 134, 142 | sylibrd 242 |
. . . . . . 7
 
 
        |
144 | 6, 4, 14, 17, 1, 139, 5 | sylow2alem1 17347 |
. . . . . . . . . 10
 
       |
145 | | simpr 468 |
. . . . . . . . . . 11
 
   |
146 | 145 | snssd 4108 |
. . . . . . . . . 10
 
     |
147 | 144, 146 | eqsstrd 3452 |
. . . . . . . . 9
 
  
  |
148 | 147 | ex 441 |
. . . . . . . 8
       |
149 | 148 | adantr 472 |
. . . . . . 7
 
       |
150 | 143, 149 | syld 44 |
. . . . . 6
 
 
          |
151 | 150 | con1d 129 |
. . . . 5
 
   
        |
152 | 35, 42, 151 | ectocld 7448 |
. . . 4
 
  

        |
153 | 152 | impr 631 |
. . 3
 
            |
154 | 34, 153 | sylan2b 483 |
. 2
 
            |
155 | 13, 23, 33, 154 | fsumdvds 14425 |
1
              |