Step | Hyp | Ref
| Expression |
1 | | ablfac1eu.1 |
. . . . 5
   DProd 
DProd     |
2 | 1 | simpld 466 |
. . . 4
  DProd
  |
3 | | ablfac1eu.2 |
. . . 4
   |
4 | 2, 3 | dprdf2 17717 |
. . 3
     SubGrp    |
5 | | ffn 5739 |
. . 3
     SubGrp    |
6 | 4, 5 | syl 17 |
. 2
   |
7 | | ablfac1.b |
. . . . 5
     |
8 | | ablfac1.o |
. . . . 5
     |
9 | | ablfac1.s |
. . . . 5
                   |
10 | | ablfac1.g |
. . . . 5
   |
11 | | ablfac1.f |
. . . . 5
   |
12 | | ablfac1.1 |
. . . . 5

  |
13 | 7, 8, 9, 10, 11, 12 | ablfac1b 17781 |
. . . 4
  DProd
  |
14 | | fvex 5889 |
. . . . . . . 8
     |
15 | 7, 14 | eqeltri 2545 |
. . . . . . 7
 |
16 | 15 | rabex 4550 |
. . . . . 6

       
        |
17 | 16, 9 | dmmpti 5717 |
. . . . 5
 |
18 | 17 | a1i 11 |
. . . 4
   |
19 | 13, 18 | dprdf2 17717 |
. . 3
     SubGrp    |
20 | | ffn 5739 |
. . 3
     SubGrp    |
21 | 19, 20 | syl 17 |
. 2
   |
22 | 11 | adantr 472 |
. . . 4
 
   |
23 | 19 | ffvelrnda 6037 |
. . . . 5
 
     SubGrp    |
24 | 7 | subgss 16896 |
. . . . 5
     SubGrp 
      |
25 | 23, 24 | syl 17 |
. . . 4
 
       |
26 | | ssfi 7810 |
. . . 4
             |
27 | 22, 25, 26 | syl2anc 673 |
. . 3
 
       |
28 | 4 | ffvelrnda 6037 |
. . . . . 6
 
     SubGrp    |
29 | 7 | subgss 16896 |
. . . . . 6
     SubGrp 
      |
30 | 28, 29 | syl 17 |
. . . . 5
 
       |
31 | 28 | adantr 472 |
. . . . . . 7
             SubGrp    |
32 | | ssfi 7810 |
. . . . . . . . 9
             |
33 | 22, 30, 32 | syl2anc 673 |
. . . . . . . 8
 
       |
34 | 33 | adantr 472 |
. . . . . . 7
               |
35 | | simpr 468 |
. . . . . . 7
               |
36 | 8 | odsubdvds 17298 |
. . . . . . 7
      SubGrp                         |
37 | 31, 34, 35, 36 | syl3anc 1292 |
. . . . . 6
                       |
38 | | ablfac1eu.4 |
. . . . . . . 8
 
               |
39 | 12 | sselda 3418 |
. . . . . . . . . 10
 
   |
40 | | prmz 14705 |
. . . . . . . . . 10

  |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
 
   |
42 | | ablfac1eu.3 |
. . . . . . . . 9
 
   |
43 | 42 | nn0zd 11061 |
. . . . . . . . . 10
 
   |
44 | | ablgrp 17513 |
. . . . . . . . . . . . . . . 16

  |
45 | 10, 44 | syl 17 |
. . . . . . . . . . . . . . 15
   |
46 | 7 | grpbn0 16773 |
. . . . . . . . . . . . . . 15
   |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
   |
48 | | hashnncl 12585 |
. . . . . . . . . . . . . . 15
     
   |
49 | 11, 48 | syl 17 |
. . . . . . . . . . . . . 14
     
   |
50 | 47, 49 | mpbird 240 |
. . . . . . . . . . . . 13
       |
51 | 50 | adantr 472 |
. . . . . . . . . . . 12
 
       |
52 | 39, 51 | pccld 14879 |
. . . . . . . . . . 11
 
 
       |
53 | 52 | nn0zd 11061 |
. . . . . . . . . 10
 
 
       |
54 | 7 | lagsubg 16957 |
. . . . . . . . . . . . 13
      SubGrp                 |
55 | 28, 22, 54 | syl2anc 673 |
. . . . . . . . . . . 12
 
               |
56 | 38, 55 | eqbrtrrd 4418 |
. . . . . . . . . . 11
 
           |
57 | 51 | nnzd 11062 |
. . . . . . . . . . . 12
 
       |
58 | | pcdvdsb 14897 |
. . . . . . . . . . . 12
                         |
59 | 39, 57, 42, 58 | syl3anc 1292 |
. . . . . . . . . . 11
 
                   |
60 | 56, 59 | mpbird 240 |
. . . . . . . . . 10
 
         |
61 | | eluz2 11188 |
. . . . . . . . . 10
 
        
      
         |
62 | 43, 53, 60, 61 | syl3anbrc 1214 |
. . . . . . . . 9
 
 
           |
63 | | dvdsexp 14439 |
. . . . . . . . 9
 

                          |
64 | 41, 42, 62, 63 | syl3anc 1292 |
. . . . . . . 8
 
                 |
65 | 38, 64 | eqbrtrd 4416 |
. . . . . . 7
 
            
        |
66 | 65 | adantr 472 |
. . . . . 6
                    
        |
67 | 30 | sselda 3418 |
. . . . . . . . 9
           |
68 | 7, 8 | odcl 17263 |
. . . . . . . . 9
       |
69 | 67, 68 | syl 17 |
. . . . . . . 8
               |
70 | 69 | nn0zd 11061 |
. . . . . . 7
               |
71 | | hashcl 12576 |
. . . . . . . . . 10
               |
72 | 33, 71 | syl 17 |
. . . . . . . . 9
 
           |
73 | 72 | nn0zd 11061 |
. . . . . . . 8
 
           |
74 | 73 | adantr 472 |
. . . . . . 7
                   |
75 | | prmnn 14704 |
. . . . . . . . . . 11

  |
76 | 39, 75 | syl 17 |
. . . . . . . . . 10
 
   |
77 | 76, 52 | nnexpcld 12475 |
. . . . . . . . 9
 
             |
78 | 77 | nnzd 11062 |
. . . . . . . 8
 
             |
79 | 78 | adantr 472 |
. . . . . . 7
                     |
80 | | dvdstr 14414 |
. . . . . . 7
                                                                 
         |
81 | 70, 74, 79, 80 | syl3anc 1292 |
. . . . . 6
                                                 
         |
82 | 37, 66, 81 | mp2and 693 |
. . . . 5
                
        |
83 | 30, 82 | ssrabdv 3494 |
. . . 4
 
                       |
84 | | id 22 |
. . . . . . . . 9
   |
85 | | oveq1 6315 |
. . . . . . . . 9
 
     
       |
86 | 84, 85 | oveq12d 6326 |
. . . . . . . 8
              
        |
87 | 86 | breq2d 4407 |
. . . . . . 7
     
         
                 |
88 | 87 | rabbidv 3022 |
. . . . . 6
 
       
               
         |
89 | 88, 9, 16 | fvmpt3i 5968 |
. . . . 5
                       |
90 | 89 | adantl 473 |
. . . 4
 
                       |
91 | 83, 90 | sseqtr4d 3455 |
. . 3
 
           |
92 | 77 | nnnn0d 10949 |
. . . . . 6
 
             |
93 | | pcdvds 14892 |
. . . . . . . . . 10
                       |
94 | 39, 51, 93 | syl2anc 673 |
. . . . . . . . 9
 
                 |
95 | 2 | adantr 472 |
. . . . . . . . . . . . . . 15
 
  DProd   |
96 | 3 | adantr 472 |
. . . . . . . . . . . . . . 15
 
   |
97 | | ablfac1.2 |
. . . . . . . . . . . . . . . 16

  |
98 | 97 | adantr 472 |
. . . . . . . . . . . . . . 15
 
   |
99 | 95, 96, 98 | dprdres 17739 |
. . . . . . . . . . . . . 14
 
   DProd    DProd   
 DProd     |
100 | 99 | simpld 466 |
. . . . . . . . . . . . 13
 
  DProd     |
101 | 4 | adantr 472 |
. . . . . . . . . . . . . . 15
 
     SubGrp    |
102 | 101, 98 | fssresd 5762 |
. . . . . . . . . . . . . 14
 
       SubGrp    |
103 | | fdm 5745 |
. . . . . . . . . . . . . 14
 
     SubGrp      |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . 13
 
 
   |
105 | | difssd 3550 |
. . . . . . . . . . . . 13
 
    
  |
106 | 100, 104,
105 | dprdres 17739 |
. . . . . . . . . . . 12
 
   DProd          DProd          
DProd       |
107 | 106 | simpld 466 |
. . . . . . . . . . 11
 
  DProd           |
108 | | dprdsubg 17735 |
. . . . . . . . . . 11
  DProd          DProd          SubGrp    |
109 | 107, 108 | syl 17 |
. . . . . . . . . 10
 
  DProd          SubGrp    |
110 | 7 | lagsubg 16957 |
. . . . . . . . . 10
   DProd  
       SubGrp       DProd                 |
111 | 109, 22, 110 | syl2anc 673 |
. . . . . . . . 9
 
     DProd                 |
112 | | eqid 2471 |
. . . . . . . . . . . . . . 15
         |
113 | 112 | subg0cl 16903 |
. . . . . . . . . . . . . 14
  DProd          SubGrp       DProd            |
114 | 109, 113 | syl 17 |
. . . . . . . . . . . . 13
 
      DProd  
         |
115 | | ne0i 3728 |
. . . . . . . . . . . . 13
      DProd         
 DProd            |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . 12
 
  DProd            |
117 | 7 | dprdssv 17727 |
. . . . . . . . . . . . . 14
 DProd           |
118 | | ssfi 7810 |
. . . . . . . . . . . . . 14
  
DProd    
       DProd
   
       |
119 | 22, 117, 118 | sylancl 675 |
. . . . . . . . . . . . 13
 
  DProd            |
120 | | hashnncl 12585 |
. . . . . . . . . . . . 13
  DProd               DProd  
         DProd             |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . 12
 
      DProd          
 DProd             |
122 | 116, 121 | mpbird 240 |
. . . . . . . . . . 11
 
     DProd             |
123 | 122 | nnzd 11062 |
. . . . . . . . . 10
 
     DProd             |
124 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
                                     |
125 | 10 | adantr 472 |
. . . . . . . . . . . . . . . 16
 

  |
126 | 11 | adantr 472 |
. . . . . . . . . . . . . . . 16
 

  |
127 | | ablfac1c.d |
. . . . . . . . . . . . . . . . . 18
       |
128 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . . 18
     
 |
129 | 127, 128 | eqsstri 3448 |
. . . . . . . . . . . . . . . . 17
 |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . . . 16
 

  |
131 | | ssid 3437 |
. . . . . . . . . . . . . . . . 17
 |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . 16
 

  |
133 | 2, 3, 97 | dprdres 17739 |
. . . . . . . . . . . . . . . . . . 19
   DProd    DProd   
 DProd     |
134 | 133 | simpld 466 |
. . . . . . . . . . . . . . . . . 18
  DProd
    |
135 | | dprdsubg 17735 |
. . . . . . . . . . . . . . . . . . . . 21
  DProd    DProd    SubGrp    |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
  DProd    SubGrp    |
137 | | difssd 3550 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
  |
138 | 2, 3, 137 | dprdres 17739 |
. . . . . . . . . . . . . . . . . . . . . 22
   DProd      DProd     
 DProd     |
139 | 138 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . 21
  DProd
      |
140 | | dprdsubg 17735 |
. . . . . . . . . . . . . . . . . . . . 21
  DProd  
 
 DProd 
    SubGrp    |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
  DProd      SubGrp    |
142 | | difss 3549 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
143 | | fssres 5761 |
. . . . . . . . . . . . . . . . . . . . . . 23
      SubGrp               SubGrp    |
144 | 4, 142, 143 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
           SubGrp    |
145 | | fdm 5745 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         SubGrp   
      |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
  
      |
147 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
148 | 147 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
 

 
              |
149 | | eldif 3400 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

   |
150 | 33 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

        |
151 | 112 | subg0cl 16903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     SubGrp 
          |
152 | 28, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
           |
153 | 152 | snssd 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
      
      |
154 | 153 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

              |
155 | 38 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

                |
156 | 39 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
157 | | iddvdsexp 14403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
       |
158 | 41, 157 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           |
159 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               |
160 | 38, 73 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
       |
161 | | dvdstr 14414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                
                |
162 | 41, 160, 57, 161 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
                       |
163 | 162 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                           |
164 | 158, 159,
163 | mp2and 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
165 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
           |
166 | 165, 127 | elrab2 3186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34


       |
167 | 156, 164,
166 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
168 | 167 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
 
   |
169 | 168 | con3d 140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
 
   |
170 | 169 | impr 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

 
  |
171 | 42 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 

 
  |
172 | | elnn0 10895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

    |
173 | 171, 172 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

  
   |
174 | 173 | ord 384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

  
   |
175 | 170, 174 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

 
  |
176 | 175 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

            |
177 | 76 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

    |
178 | 177 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

    |
179 | 178 | exp0d 12448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

        |
180 | 155, 176,
179 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

            |
181 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
182 | | hashsng 12587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 |
183 | 181, 182 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
184 | 180, 183 | syl6reqr 2524 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

                      |
185 | | snfi 7668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
186 | | hashen 12568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                             |
187 | 185, 150,
186 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

                                  |
188 | 184, 187 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

              |
189 | | fisseneq 7801 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                          
            |
190 | 150, 154,
188, 189 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

              |
191 | 112 | subg0cl 16903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  DProd    SubGrp       DProd      |
192 | 136, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      DProd      |
193 | 192 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

       DProd      |
194 | 193 | snssd 4108 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

        
DProd      |
195 | 190, 194 | eqsstr3d 3453 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

     
 DProd 
    |
196 | 149, 195 | sylan2b 483 |
. . . . . . . . . . . . . . . . . . . . . 22
 

 
     DProd      |
197 | 148, 196 | eqsstrd 3452 |
. . . . . . . . . . . . . . . . . . . . 21
 

 
         DProd      |
198 | 139, 146,
136, 197 | dprdlub 17737 |
. . . . . . . . . . . . . . . . . . . 20
  DProd      
DProd      |
199 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . 21
         |
200 | 199 | lsmss2 17396 |
. . . . . . . . . . . . . . . . . . . 20
   DProd    SubGrp   DProd      SubGrp   DProd      
DProd       DProd           DProd        DProd      |
201 | 136, 141,
198, 200 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . 19
   DProd           DProd
       DProd      |
202 | | disjdif 3830 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
203 | 202 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
       |
204 | | undif2 3834 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
205 | | ssequn1 3595 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
206 | 97, 205 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
207 | 204, 206 | syl5req 2518 |
. . . . . . . . . . . . . . . . . . . . 21
       |
208 | 4, 203, 207, 199, 2 | dprdsplit 17759 |
. . . . . . . . . . . . . . . . . . . 20
  DProd    DProd           DProd         |
209 | 1 | simprd 470 |
. . . . . . . . . . . . . . . . . . . 20
  DProd    |
210 | 208, 209 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . 19
   DProd           DProd
        |
211 | 201, 210 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . 18
  DProd      |
212 | 134, 211 | jca 541 |
. . . . . . . . . . . . . . . . 17
   DProd    DProd       |
213 | 212 | adantr 472 |
. . . . . . . . . . . . . . . 16
 

  DProd    DProd       |
214 | 4, 97 | fssresd 5762 |
. . . . . . . . . . . . . . . . . 18
       SubGrp    |
215 | 214, 103 | syl 17 |
. . . . . . . . . . . . . . . . 17
     |
216 | 215 | adantr 472 |
. . . . . . . . . . . . . . . 16
 

    |
217 | 97 | sselda 3418 |
. . . . . . . . . . . . . . . . . 18
 
   |
218 | 217, 42 | syldan 478 |
. . . . . . . . . . . . . . . . 17
 
   |
219 | 218 | adantlr 729 |
. . . . . . . . . . . . . . . 16
       |
220 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . 20
             |
221 | 220 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
 
             |
222 | 221 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
 
                     |
223 | 217, 38 | syldan 478 |
. . . . . . . . . . . . . . . . . 18
 
               |
224 | 222, 223 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
 
                 |
225 | 224 | adantlr 729 |
. . . . . . . . . . . . . . . 16
                     |
226 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 

  |
227 | | fzfid 12224 |
. . . . . . . . . . . . . . . . . 18
           |
228 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
229 | 228 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
230 | | prmz 14705 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
231 | | dvdsle 14427 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
232 | 230, 50, 231 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    
       |
233 | 232 | 3impia 1228 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
234 | 50 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
235 | 234 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
236 | | fznn 11889 |
. . . . . . . . . . . . . . . . . . . . . 22
    
         
        |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
              
        |
238 | 229, 233,
237 | mpbir2and 936 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
239 | 238 | rabssdv 3495 |
. . . . . . . . . . . . . . . . . . 19
                 |
240 | 127, 239 | syl5eqss 3462 |
. . . . . . . . . . . . . . . . . 18

          |
241 | | ssfi 7810 |
. . . . . . . . . . . . . . . . . 18
                  
  |
242 | 227, 240,
241 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
   |
243 | 242 | adantr 472 |
. . . . . . . . . . . . . . . 16
 

  |
244 | 7, 8, 124, 125, 126, 130, 127, 132, 213, 216, 219, 225, 226, 243 | ablfac1eulem 17783 |
. . . . . . . . . . . . . . 15
 

    DProd             |
245 | 244 | ralrimiva 2809 |
. . . . . . . . . . . . . 14
      DProd  
          |
246 | 245 | adantr 472 |
. . . . . . . . . . . . 13
 
 
    DProd             |
247 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
248 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
249 | 248 | difeq2d 3540 |
. . . . . . . . . . . . . . . . . . 19
           |
250 | 249 | reseq2d 5111 |
. . . . . . . . . . . . . . . . . 18
                   |
251 | 250 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
  DProd           DProd  
         |
252 | 251 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
     DProd               DProd             |
253 | 247, 252 | breq12d 4408 |
. . . . . . . . . . . . . . 15
 
    DProd          
    DProd              |
254 | 253 | notbid 301 |
. . . . . . . . . . . . . 14
 
    DProd  
       
    DProd              |
255 | 254 | rspcv 3132 |
. . . . . . . . . . . . 13

 
    DProd          
    DProd              |
256 | 39, 246, 255 | sylc 61 |
. . . . . . . . . . . 12
 
     DProd             |
257 | | coprm 14736 |
. . . . . . . . . . . . 13
      DProd                 DProd                DProd               |
258 | 39, 123, 257 | syl2anc 673 |
. . . . . . . . . . . 12
 
 
    DProd  
       
     DProd               |
259 | 256, 258 | mpbid 215 |
. . . . . . . . . . 11
 
 
    DProd              |
260 | | rpexp1i 14752 |
. . . . . . . . . . . 12
      DProd           
            DProd                           DProd  
            |
261 | 41, 123, 52, 260 | syl3anc 1292 |
. . . . . . . . . . 11
 
       DProd           
               DProd               |
262 | 259, 261 | mpd 15 |
. . . . . . . . . 10
 
     
          DProd              |
263 | | coprmdvds2 14739 |
. . . . . . . . . 10
                 DProd                    
          DProd                                 DProd                    
          DProd                   |
264 | 78, 123, 57, 262, 263 | syl31anc 1295 |
. . . . . . . . 9
 
                     DProd                               DProd                   |
265 | 94, 111, 264 | mp2and 693 |
. . . . . . . 8
 
     
          DProd                  |
266 | | eqid 2471 |
. . . . . . . . . 10
Cntz  Cntz   |
267 | | inss1 3643 |
. . . . . . . . . . . . . 14
   
 |
268 | 267 | a1i 11 |
. . . . . . . . . . . . 13
 
    
  |
269 | 100, 104,
268 | dprdres 17739 |
. . . . . . . . . . . 12
 
   DProd          DProd          
DProd       |
270 | 269 | simpld 466 |
. . . . . . . . . . 11
 
  DProd           |
271 | | dprdsubg 17735 |
. . . . . . . . . . 11
  DProd          DProd          SubGrp    |
272 | 270, 271 | syl 17 |
. . . . . . . . . 10
 
  DProd          SubGrp    |
273 | | inass 3633 |
. . . . . . . . . . . . 13
                     |
274 | | disjdif 3830 |
. . . . . . . . . . . . . 14
         |
275 | 274 | ineq2i 3622 |
. . . . . . . . . . . . 13
             |
276 | | in0 3763 |
. . . . . . . . . . . . 13
   |
277 | 273, 275,
276 | 3eqtri 2497 |
. . . . . . . . . . . 12
           |
278 | 277 | a1i 11 |
. . . . . . . . . . 11
 
             |
279 | 100, 104,
268, 105, 278, 112 | dprddisj2 17750 |
. . . . . . . . . 10
 
   DProd
   
      DProd                   |
280 | 100, 104,
268, 105, 278, 266 | dprdcntz2 17749 |
. . . . . . . . . 10
 
  DProd           Cntz     DProd  
          |
281 | 7 | dprdssv 17727 |
. . . . . . . . . . 11
 DProd           |
282 | | ssfi 7810 |
. . . . . . . . . . 11
  
DProd    
       DProd
   
       |
283 | 22, 281, 282 | sylancl 675 |
. . . . . . . . . 10
 
  DProd            |
284 | 199, 112,
266, 272, 109, 279, 280, 283, 119 | lsmhash 17433 |
. . . . . . . . 9
 
      DProd                 DProd                 DProd               DProd              |
285 | | inundif 3836 |
. . . . . . . . . . . . . 14
           |
286 | 285 | eqcomi 2480 |
. . . . . . . . . . . . 13
           |
287 | 286 | a1i 11 |
. . . . . . . . . . . 12
 
             |
288 | 102, 278,
287, 199, 100 | dprdsplit 17759 |
. . . . . . . . . . 11
 
  DProd      DProd                 DProd             |
289 | 211 | adantr 472 |
. . . . . . . . . . 11
 
  DProd      |
290 | 288, 289 | eqtr3d 2507 |
. . . . . . . . . 10
 
   DProd
   
            DProd
   
        |
291 | 290 | fveq2d 5883 |
. . . . . . . . 9
 
      DProd                 DProd                  |
292 | | snssi 4107 |
. . . . . . . . . . . . . . . . 17
  
  |
293 | 292 | adantl 473 |
. . . . . . . . . . . . . . . 16
      
  |
294 | | dfss1 3628 |
. . . . . . . . . . . . . . . 16
           |
295 | 293, 294 | sylib 201 |
. . . . . . . . . . . . . . 15
             |
296 | 295 | reseq2d 5111 |
. . . . . . . . . . . . . 14
                     |
297 | 296 | oveq2d 6324 |
. . . . . . . . . . . . 13
      DProd           DProd  
       |
298 | 100 | adantr 472 |
. . . . . . . . . . . . . 14
      DProd     |
299 | 215 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     
   |
300 | | simpr 468 |
. . . . . . . . . . . . . 14
       |
301 | 298, 299,
300 | dpjlem 17762 |
. . . . . . . . . . . . 13
      DProd                |
302 | 220 | adantl 473 |
. . . . . . . . . . . . 13
                 |
303 | 297, 301,
302 | 3eqtrd 2509 |
. . . . . . . . . . . 12
      DProd                |
304 | | simprr 774 |
. . . . . . . . . . . . . . . . . 18
 

 
  |
305 | | disjsn 4023 |
. . . . . . . . . . . . . . . . . 18
    
  |
306 | 304, 305 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
 

        |
307 | 306 | reseq2d 5111 |
. . . . . . . . . . . . . . . 16
 

                |
308 | | res0 5115 |
. . . . . . . . . . . . . . . 16
 
 
 |
309 | 307, 308 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
 

            |
310 | 309 | oveq2d 6324 |
. . . . . . . . . . . . . 14
 

   DProd
   
      DProd    |
311 | 112 | dprd0 17742 |
. . . . . . . . . . . . . . . . 17
   DProd  DProd           |
312 | 45, 311 | syl 17 |
. . . . . . . . . . . . . . . 16
   DProd  DProd           |
313 | 312 | simprd 470 |
. . . . . . . . . . . . . . 15
  DProd          |
314 | 313 | adantr 472 |
. . . . . . . . . . . . . 14
 

   DProd
         |
315 | 310, 314,
190 | 3eqtrd 2509 |
. . . . . . . . . . . . 13
 

   DProd
   
           |
316 | 315 | anassrs 660 |
. . . . . . . . . . . 12
   
  DProd  
             |
317 | 303, 316 | pm2.61dan 808 |
. . . . . . . . . . 11
 
  DProd                |
318 | 317 | fveq2d 5883 |
. . . . . . . . . 10
 
     DProd                     |
319 | 318 | oveq1d 6323 |
. . . . . . . . 9
 
      DProd               DProd                         DProd              |
320 | 284, 291,
319 | 3eqtr3d 2513 |
. . . . . . . 8
 
                  DProd  
           |
321 | 265, 320 | breqtrd 4420 |
. . . . . . 7
 
     
          DProd                         DProd              |
322 | 122 | nnne0d 10676 |
. . . . . . . 8
 
     DProd             |
323 | | dvdsmulcr 14409 |
. . . . . . . 8
     
                   DProd               DProd                             DProd  
                      DProd  
        
                     |
324 | 78, 73, 123, 322, 323 | syl112anc 1296 |
. . . . . . 7
 
                 DProd  
                      DProd  
        
                     |
325 | 321, 324 | mpbid 215 |
. . . . . 6
 
                     |
326 | | dvdseq 14429 |
. . . . . 6
              
                                             
                    |
327 | 72, 92, 65, 325, 326 | syl22anc 1293 |
. . . . 5
 
            
        |
328 | 7, 8, 9, 10, 11, 12 | ablfac1a 17780 |
. . . . 5
 
            
        |
329 | 327, 328 | eqtr4d 2508 |
. . . 4
 
                   |
330 | | hashen 12568 |
. . . . 5
                           
           |
331 | 33, 27, 330 | syl2anc 673 |
. . . 4
 
                             |
332 | 329, 331 | mpbid 215 |
. . 3
 
           |
333 | | fisseneq 7801 |
. . 3
                                 |
334 | 27, 91, 332, 333 | syl3anc 1292 |
. 2
 
           |
335 | 6, 21, 334 | eqfnfvd 5994 |
1
   |