Step | Hyp | Ref
| Expression |
1 | | nprmdvds1 14643 |
. . . . . . 7

  |
2 | 1 | adantl 468 |
. . . . . 6
 

  |
3 | | ablfacrp.1 |
. . . . . . . 8
     |
4 | 3 | adantr 467 |
. . . . . . 7
 

    |
5 | 4 | breq2d 4413 |
. . . . . 6
 

  
   |
6 | 2, 5 | mtbird 303 |
. . . . 5
 

    |
7 | | ablfacrp.k |
. . . . . . . . . . . . . 14
       |
8 | | ablfacrp.g |
. . . . . . . . . . . . . . 15
   |
9 | | ablfacrp.m |
. . . . . . . . . . . . . . . 16
   |
10 | 9 | nnzd 11036 |
. . . . . . . . . . . . . . 15
   |
11 | | ablfacrp.o |
. . . . . . . . . . . . . . . 16
     |
12 | | ablfacrp.b |
. . . . . . . . . . . . . . . 16
     |
13 | 11, 12 | oddvdssubg 17486 |
. . . . . . . . . . . . . . 15
   
     SubGrp    |
14 | 8, 10, 13 | syl2anc 666 |
. . . . . . . . . . . . . 14
      
SubGrp    |
15 | 7, 14 | syl5eqel 2532 |
. . . . . . . . . . . . 13
 SubGrp    |
16 | 15 | ad2antrr 731 |
. . . . . . . . . . . 12
         SubGrp    |
17 | | eqid 2450 |
. . . . . . . . . . . . 13
 ↾s   ↾s   |
18 | 17 | subggrp 16813 |
. . . . . . . . . . . 12
 SubGrp 
 ↾s    |
19 | 16, 18 | syl 17 |
. . . . . . . . . . 11
          ↾s    |
20 | 17 | subgbas 16814 |
. . . . . . . . . . . . 13
 SubGrp 
    ↾s     |
21 | 16, 20 | syl 17 |
. . . . . . . . . . . 12
             ↾s     |
22 | | ablfacrp.2 |
. . . . . . . . . . . . . . . 16
         |
23 | 9 | nnnn0d 10922 |
. . . . . . . . . . . . . . . . 17
   |
24 | | ablfacrp.n |
. . . . . . . . . . . . . . . . . 18
   |
25 | 24 | nnnn0d 10922 |
. . . . . . . . . . . . . . . . 17
   |
26 | 23, 25 | nn0mulcld 10927 |
. . . . . . . . . . . . . . . 16
     |
27 | 22, 26 | eqeltrd 2528 |
. . . . . . . . . . . . . . 15
       |
28 | | fvex 5873 |
. . . . . . . . . . . . . . . . 17
     |
29 | 12, 28 | eqeltri 2524 |
. . . . . . . . . . . . . . . 16
 |
30 | | hashclb 12537 |
. . . . . . . . . . . . . . . 16
 
       |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . . . 15

      |
32 | 27, 31 | sylibr 216 |
. . . . . . . . . . . . . 14
   |
33 | | ssrab2 3513 |
. . . . . . . . . . . . . . 15

      |
34 | 7, 33 | eqsstri 3461 |
. . . . . . . . . . . . . 14
 |
35 | | ssfi 7789 |
. . . . . . . . . . . . . 14
  
  |
36 | 32, 34, 35 | sylancl 667 |
. . . . . . . . . . . . 13
   |
37 | 36 | ad2antrr 731 |
. . . . . . . . . . . 12
           |
38 | 21, 37 | eqeltrrd 2529 |
. . . . . . . . . . 11
             ↾s     |
39 | | simplr 761 |
. . . . . . . . . . 11
           |
40 | | simpr 463 |
. . . . . . . . . . . 12
               |
41 | 21 | fveq2d 5867 |
. . . . . . . . . . . 12
                    ↾s      |
42 | 40, 41 | breqtrd 4426 |
. . . . . . . . . . 11
                ↾s      |
43 | | eqid 2450 |
. . . . . . . . . . . 12
   
↾s       ↾s    |
44 | | eqid 2450 |
. . . . . . . . . . . 12
    ↾s       ↾s    |
45 | 43, 44 | odcau 17249 |
. . . . . . . . . . 11
    ↾s      ↾s  
        ↾s     
    ↾s         ↾s        |
46 | 19, 38, 39, 42, 45 | syl31anc 1270 |
. . . . . . . . . 10
              ↾s         ↾s        |
47 | 21 | rexeqdv 2993 |
. . . . . . . . . 10
          
    
↾s      
    ↾s         ↾s         |
48 | 46, 47 | mpbird 236 |
. . . . . . . . 9
         
     ↾s        |
49 | 17, 11, 44 | subgod 17212 |
. . . . . . . . . . . . 13
  SubGrp            ↾s        |
50 | 16, 49 | sylan 474 |
. . . . . . . . . . . 12
   
                ↾s        |
51 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
52 | 51 | breq1d 4411 |
. . . . . . . . . . . . . . 15
     
       |
53 | 52, 7 | elrab2 3197 |
. . . . . . . . . . . . . 14


       |
54 | 53 | simprbi 466 |
. . . . . . . . . . . . 13
       |
55 | 54 | adantl 468 |
. . . . . . . . . . . 12
   
             |
56 | 50, 55 | eqbrtrrd 4424 |
. . . . . . . . . . 11
   
            ↾s        |
57 | | breq1 4404 |
. . . . . . . . . . 11
      ↾s            ↾s     
   |
58 | 56, 57 | syl5ibcom 224 |
. . . . . . . . . 10
   
            
↾s         |
59 | 58 | rexlimdva 2878 |
. . . . . . . . 9
          
    
↾s         |
60 | 48, 59 | mpd 15 |
. . . . . . . 8
           |
61 | 60 | ex 436 |
. . . . . . 7
 

    
   |
62 | 61 | anim1d 567 |
. . . . . 6
 

 
   

     |
63 | | prmz 14619 |
. . . . . . . 8

  |
64 | 63 | adantl 468 |
. . . . . . 7
 

  |
65 | | hashcl 12535 |
. . . . . . . . . 10
       |
66 | 36, 65 | syl 17 |
. . . . . . . . 9
       |
67 | 66 | nn0zd 11035 |
. . . . . . . 8
       |
68 | 67 | adantr 467 |
. . . . . . 7
 

      |
69 | 24 | nnzd 11036 |
. . . . . . . 8
   |
70 | 69 | adantr 467 |
. . . . . . 7
 

  |
71 | | dvdsgcdb 14505 |
. . . . . . 7
             
         |
72 | 64, 68, 70, 71 | syl3anc 1267 |
. . . . . 6
 

 
   

         |
73 | 10 | adantr 467 |
. . . . . . 7
 

  |
74 | | dvdsgcdb 14505 |
. . . . . . 7
 
  

     |
75 | 64, 73, 70, 74 | syl3anc 1267 |
. . . . . 6
 

 

     |
76 | 62, 72, 75 | 3imtr3d 271 |
. . . . 5
 

     
      |
77 | 6, 76 | mtod 181 |
. . . 4
 

    
   |
78 | 77 | nrexdv 2842 |
. . 3
 
        |
79 | | exprmfct 14641 |
. . 3
     
              |
80 | 78, 79 | nsyl 125 |
. 2
             |
81 | 24 | nnne0d 10651 |
. . . . . 6
   |
82 | | simpr 463 |
. . . . . . 7
         |
83 | 82 | necon3ai 2648 |
. . . . . 6
         |
84 | 81, 83 | syl 17 |
. . . . 5
         |
85 | | gcdn0cl 14469 |
. . . . 5
      
                |
86 | 67, 69, 84, 85 | syl21anc 1266 |
. . . 4
     
   |
87 | | elnn1uz2 11232 |
. . . 4
     
                     |
88 | 86, 87 | sylib 200 |
. . 3
            
        |
89 | 88 | ord 379 |
. 2
                     |
90 | 80, 89 | mt3d 129 |
1
     
   |