Step | Hyp | Ref
| Expression |
1 | | ovex 6336 |
. . . 4
          |
2 | | fveq2 5879 |
. . . . . . . 8
           |
3 | 2 | eqeq1d 2473 |
. . . . . . 7
             |
4 | 3 | elrab 3184 |
. . . . . 6
      

       |
5 | | prmrec.4 |
. . . . . . . . . . . . . . . . . . . 20
      
       |
6 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . . . . 20
      
           |
7 | 5, 6 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . 19
     |
8 | | simprl 772 |
. . . . . . . . . . . . . . . . . . . 20
 

        |
9 | 8 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
                   |
10 | 7, 9 | sseldi 3416 |
. . . . . . . . . . . . . . . . . 18
                       |
11 | | elfznn 11854 |
. . . . . . . . . . . . . . . . . 18
       |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . 17
                   |
13 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
                   |
14 | | prmuz2 14721 |
. . . . . . . . . . . . . . . . . 18

      |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
                       |
16 | | prmreclem2.5 |
. . . . . . . . . . . . . . . . . . 19
             |
17 | 16 | prmreclem1 14939 |
. . . . . . . . . . . . . . . . . 18
              
                      |
18 | 17 | simp3d 1044 |
. . . . . . . . . . . . . . . . 17
                       |
19 | 12, 15, 18 | sylc 61 |
. . . . . . . . . . . . . . . 16
                                 |
20 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

            |
21 | 20 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
22 | 21 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . 21
                               |
23 | | sq1 12407 |
. . . . . . . . . . . . . . . . . . . . 21
     |
24 | 22, 23 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . 20
                           |
25 | 24 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
                               |
26 | 12 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . . 20
                   |
27 | 26 | div1d 10397 |
. . . . . . . . . . . . . . . . . . 19
                     |
28 | 25, 27 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
                             |
29 | 28 | breq2d 4407 |
. . . . . . . . . . . . . . . . 17
                               
       |
30 | 12 | nnzd 11062 |
. . . . . . . . . . . . . . . . . 18
                   |
31 | | 2nn0 10910 |
. . . . . . . . . . . . . . . . . . 19
 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                   |
33 | | pcdvdsb 14897 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
34 | 13, 30, 32, 33 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
                 
 
       |
35 | 29, 34 | bitr4d 264 |
. . . . . . . . . . . . . . . 16
                               

    |
36 | 19, 35 | mtbid 307 |
. . . . . . . . . . . . . . 15
                     |
37 | 13, 12 | pccld 14879 |
. . . . . . . . . . . . . . . . 17
                 
   |
38 | 37 | nn0red 10950 |
. . . . . . . . . . . . . . . 16
                 
   |
39 | | 2re 10701 |
. . . . . . . . . . . . . . . 16
 |
40 | | ltnle 9731 |
. . . . . . . . . . . . . . . 16
   
         |
41 | 38, 39, 40 | sylancl 675 |
. . . . . . . . . . . . . . 15
                   
     |
42 | 36, 41 | mpbird 240 |
. . . . . . . . . . . . . 14
                 
   |
43 | | df-2 10690 |
. . . . . . . . . . . . . 14
   |
44 | 42, 43 | syl6breq 4435 |
. . . . . . . . . . . . 13
                 
     |
45 | 37 | nn0zd 11061 |
. . . . . . . . . . . . . 14
                 
   |
46 | | 1z 10991 |
. . . . . . . . . . . . . 14
 |
47 | | zleltp1 11011 |
. . . . . . . . . . . . . 14
   
   
       |
48 | 45, 46, 47 | sylancl 675 |
. . . . . . . . . . . . 13
                   
       |
49 | 44, 48 | mpbird 240 |
. . . . . . . . . . . 12
                 
   |
50 | | nn0uz 11217 |
. . . . . . . . . . . . . 14
     |
51 | 37, 50 | syl6eleq 2559 |
. . . . . . . . . . . . 13
                 
       |
52 | | elfz5 11818 |
. . . . . . . . . . . . 13
               
     |
53 | 51, 46, 52 | sylancl 675 |
. . . . . . . . . . . 12
                       
     |
54 | 49, 53 | mpbird 240 |
. . . . . . . . . . 11
                 
       |
55 | | 0z 10972 |
. . . . . . . . . . . . 13
 |
56 | | fzpr 11877 |
. . . . . . . . . . . . 13
              |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . 12
            |
58 | | 1e0p1 11102 |
. . . . . . . . . . . . 13
   |
59 | 58 | oveq2i 6319 |
. . . . . . . . . . . 12
           |
60 | 58 | preq2i 4046 |
. . . . . . . . . . . 12
         |
61 | 57, 59, 60 | 3eqtr4i 2503 |
. . . . . . . . . . 11
        |
62 | 54, 61 | syl6eleq 2559 |
. . . . . . . . . 10
                 
      |
63 | | c0ex 9655 |
. . . . . . . . . . . 12
 |
64 | 63 | prid1 4071 |
. . . . . . . . . . 11
    |
65 | 64 | a1i 11 |
. . . . . . . . . 10
               
      |
66 | 62, 65 | ifclda 3904 |
. . . . . . . . 9
              
   
        |
67 | | eqid 2471 |
. . . . . . . . 9
        
                  |
68 | 66, 67 | fmptd 6061 |
. . . . . . . 8
 

                                |
69 | | prex 4642 |
. . . . . . . . 9
    |
70 | | ovex 6336 |
. . . . . . . . 9
     |
71 | 69, 70 | elmap 7518 |
. . . . . . . 8
                      
                          |
72 | 68, 71 | sylibr 217 |
. . . . . . 7
 

                              |
73 | 72 | ex 441 |
. . . . . 6
                                 |
74 | 4, 73 | syl5bi 225 |
. . . . 5
                                 |
75 | | fveq2 5879 |
. . . . . . . . 9
           |
76 | 75 | eqeq1d 2473 |
. . . . . . . 8
             |
77 | 76 | elrab 3184 |
. . . . . . 7
      

       |
78 | 4, 77 | anbi12i 711 |
. . . . . 6
  
    

                      |
79 | | ovex 6336 |
. . . . . . . . . . . 12
   |
80 | 79, 63 | ifex 3940 |
. . . . . . . . . . 11
   
    |
81 | 80, 67 | fnmpti 5716 |
. . . . . . . . . 10
        
         |
82 | | ovex 6336 |
. . . . . . . . . . . 12
   |
83 | 82, 63 | ifex 3940 |
. . . . . . . . . . 11
   
    |
84 | | eqid 2471 |
. . . . . . . . . . 11
        
                  |
85 | 83, 84 | fnmpti 5716 |
. . . . . . . . . 10
        
         |
86 | | eqfnfv 5991 |
. . . . . . . . . 10
         
         
                          
                
               
                           |
87 | 81, 85, 86 | mp2an 686 |
. . . . . . . . 9
                      
    
             
                           |
88 | | eleq1 2537 |
. . . . . . . . . . . . 13
 
   |
89 | | oveq1 6315 |
. . . . . . . . . . . . 13
 
     |
90 | 88, 89 | ifbieq1d 3895 |
. . . . . . . . . . . 12
  
              |
91 | | ovex 6336 |
. . . . . . . . . . . . 13
   |
92 | 91, 63 | ifex 3940 |
. . . . . . . . . . . 12
   
    |
93 | 90, 67, 92 | fvmpt 5963 |
. . . . . . . . . . 11
             
           
     |
94 | | oveq1 6315 |
. . . . . . . . . . . . 13
 
     |
95 | 88, 94 | ifbieq1d 3895 |
. . . . . . . . . . . 12
  
              |
96 | | ovex 6336 |
. . . . . . . . . . . . 13
   |
97 | 96, 63 | ifex 3940 |
. . . . . . . . . . . 12
   
    |
98 | 95, 84, 97 | fvmpt 5963 |
. . . . . . . . . . 11
             
           
     |
99 | 93, 98 | eqeq12d 2486 |
. . . . . . . . . 10
                               
          
       
      |
100 | 99 | ralbiia 2822 |
. . . . . . . . 9
 
             
                         
                     |
101 | 87, 100 | bitri 257 |
. . . . . . . 8
                      
    
                     |
102 | | simprll 780 |
. . . . . . . . . . . . 13
 
                 |
103 | | breq2 4399 |
. . . . . . . . . . . . . . . . 17
 
   |
104 | 103 | notbid 301 |
. . . . . . . . . . . . . . . 16
 
   |
105 | 104 | ralbidv 2829 |
. . . . . . . . . . . . . . 15
  
     
 
        |
106 | 105, 5 | elrab2 3186 |
. . . . . . . . . . . . . 14

    
 
        |
107 | 106 | simprbi 471 |
. . . . . . . . . . . . 13
  
       |
108 | 102, 107 | syl 17 |
. . . . . . . . . . . 12
 
                
       |
109 | | simprrl 782 |
. . . . . . . . . . . . 13
 
                 |
110 | | breq2 4399 |
. . . . . . . . . . . . . . . . 17
 
   |
111 | 110 | notbid 301 |
. . . . . . . . . . . . . . . 16
 
   |
112 | 111 | ralbidv 2829 |
. . . . . . . . . . . . . . 15
  
     
 
        |
113 | 112, 5 | elrab2 3186 |
. . . . . . . . . . . . . 14

    
 
        |
114 | 113 | simprbi 471 |
. . . . . . . . . . . . 13
  
       |
115 | 109, 114 | syl 17 |
. . . . . . . . . . . 12
 
                
       |
116 | | r19.26 2904 |
. . . . . . . . . . . . 13
 
       
   
      
        |
117 | | eldifi 3544 |
. . . . . . . . . . . . . . . . 17
         |
118 | 11 | ssriv 3422 |
. . . . . . . . . . . . . . . . . . 19
     |
119 | 7, 118 | sstri 3427 |
. . . . . . . . . . . . . . . . . 18
 |
120 | 119, 102 | sseldi 3416 |
. . . . . . . . . . . . . . . . 17
 
                 |
121 | | pceq0 14899 |
. . . . . . . . . . . . . . . . 17
         |
122 | 117, 120,
121 | syl2anr 486 |
. . . . . . . . . . . . . . . 16
                  
     
 

   |
123 | 119, 109 | sseldi 3416 |
. . . . . . . . . . . . . . . . 17
 
                 |
124 | | pceq0 14899 |
. . . . . . . . . . . . . . . . 17
         |
125 | 117, 123,
124 | syl2anr 486 |
. . . . . . . . . . . . . . . 16
                  
     
 

   |
126 | 122, 125 | anbi12d 725 |
. . . . . . . . . . . . . . 15
                  
     
            |
127 | | eqtr3 2492 |
. . . . . . . . . . . . . . 15
             |
128 | 126, 127 | syl6bir 237 |
. . . . . . . . . . . . . 14
                  
     
 
        |
129 | 128 | ralimdva 2805 |
. . . . . . . . . . . . 13
 
                
        
 
             |
130 | 116, 129 | syl5bir 226 |
. . . . . . . . . . . 12
 
                  
      
     
 
             |
131 | 108, 115,
130 | mp2and 693 |
. . . . . . . . . . 11
 
                
            |
132 | 131 | biantrud 515 |
. . . . . . . . . 10
 
                
       
     
                  
       |
133 | | incom 3616 |
. . . . . . . . . . . . . . 15
          
  |
134 | 133 | uneq1i 3575 |
. . . . . . . . . . . . . 14
 
                           |
135 | | inundif 3836 |
. . . . . . . . . . . . . 14
     
             |
136 | 134, 135 | eqtri 2493 |
. . . . . . . . . . . . 13
 
                 |
137 | 136 | raleqi 2977 |
. . . . . . . . . . . 12
 
                             
                     |
138 | | ralunb 3606 |
. . . . . . . . . . . 12
 
                               
        
       
              
     
       |
139 | 137, 138 | bitr3i 259 |
. . . . . . . . . . 11
 
                  
 
          
     
              
       
      |
140 | | eldifn 3545 |
. . . . . . . . . . . . . . 15
      
  |
141 | | iffalse 3881 |
. . . . . . . . . . . . . . . 16
          |
142 | | iffalse 3881 |
. . . . . . . . . . . . . . . 16
          |
143 | 141, 142 | eqtr4d 2508 |
. . . . . . . . . . . . . . 15
                 |
144 | 140, 143 | syl 17 |
. . . . . . . . . . . . . 14
      
   
     
      |
145 | 144 | rgen 2766 |
. . . . . . . . . . . . 13
          
       
    |
146 | 145 | biantru 513 |
. . . . . . . . . . . 12
 
          
     
      
        
       
              
     
       |
147 | | inss1 3643 |
. . . . . . . . . . . . . . 15
       |
148 | 147 | sseli 3414 |
. . . . . . . . . . . . . 14
         |
149 | | iftrue 3878 |
. . . . . . . . . . . . . . 15

   
       |
150 | | iftrue 3878 |
. . . . . . . . . . . . . . 15

   
       |
151 | 149, 150 | eqeq12d 2486 |
. . . . . . . . . . . . . 14

              
  
    |
152 | 148, 151 | syl 17 |
. . . . . . . . . . . . 13
                     
  
    |
153 | 152 | ralbiia 2822 |
. . . . . . . . . . . 12
 
          
     
     
            |
154 | 146, 153 | bitr3i 259 |
. . . . . . . . . . 11
   
        
       
              
     
    
 
            |
155 | 139, 154 | bitri 257 |
. . . . . . . . . 10
 
                  
 
            |
156 | | inundif 3836 |
. . . . . . . . . . . 12
 
             |
157 | 156 | raleqi 2977 |
. . . . . . . . . . 11
 
       
          
       |
158 | | ralunb 3606 |
. . . . . . . . . . 11
 
       
          
 
          
 
             |
159 | 157, 158 | bitr3i 259 |
. . . . . . . . . 10
 
      
                  
      |
160 | 132, 155,
159 | 3bitr4g 296 |
. . . . . . . . 9
 
                
                  
        |
161 | 120 | nnnn0d 10949 |
. . . . . . . . . 10
 
                 |
162 | 123 | nnnn0d 10949 |
. . . . . . . . . 10
 
                 |
163 | | pc11 14908 |
. . . . . . . . . 10
 
  

      |
164 | 161, 162,
163 | syl2anc 673 |
. . . . . . . . 9
 
               
        |
165 | 160, 164 | bitr4d 264 |
. . . . . . . 8
 
                
                  
   |
166 | 101, 165 | syl5bb 265 |
. . . . . . 7
 
                       
                     |
167 | 166 | ex 441 |
. . . . . 6
               
                      
        |
168 | 78, 167 | syl5bi 225 |
. . . . 5
                        
                      |
169 | 74, 168 | dom2d 7628 |
. . . 4
                             |
170 | 1, 169 | mpi 20 |
. . 3
                  |
171 | | fzfi 12223 |
. . . . . . 7
     |
172 | | ssfi 7810 |
. . . . . . 7
            
           
     
     
  |
173 | 171, 6, 172 | mp2an 686 |
. . . . . 6
      
     
 |
174 | 5, 173 | eqeltri 2545 |
. . . . 5
 |
175 | | ssrab2 3500 |
. . . . 5

      |
176 | | ssfi 7810 |
. . . . 5
         
       |
177 | 174, 175,
176 | mp2an 686 |
. . . 4

      |
178 | | prfi 7864 |
. . . . 5
    |
179 | | fzfid 12224 |
. . . . 5
       |
180 | | mapfi 7888 |
. . . . 5
                     |
181 | 178, 179,
180 | sylancr 676 |
. . . 4
            |
182 | | hashdom 12596 |
. . . 4
                            
                               |
183 | 177, 181,
182 | sylancr 676 |
. . 3
           
                               |
184 | 170, 183 | mpbird 240 |
. 2
          
               |
185 | | hashmap 12648 |
. . . 4
                                            |
186 | 178, 179,
185 | sylancr 676 |
. . 3
                                   |
187 | | 0ne1 10699 |
. . . . . 6
 |
188 | | 0cn 9653 |
. . . . . . 7
 |
189 | | ax-1cn 9615 |
. . . . . . 7
 |
190 | | hashprg 12610 |
. . . . . . 7
 
            |
191 | 188, 189,
190 | mp2an 686 |
. . . . . 6

         |
192 | 187, 191 | mpbi 213 |
. . . . 5
        |
193 | 192 | a1i 11 |
. . . 4
          |
194 | | prmrec.2 |
. . . . . 6
   |
195 | 194 | nnnn0d 10949 |
. . . . 5
   |
196 | | hashfz1 12567 |
. . . . 5

          |
197 | 195, 196 | syl 17 |
. . . 4
           |
198 | 193, 197 | oveq12d 6326 |
. . 3
                          |
199 | 186, 198 | eqtrd 2505 |
. 2
                    |
200 | 184, 199 | breqtrd 4420 |
1
          
      |