Step | Hyp | Ref
| Expression |
1 | | nnex 10637 |
. . . . 5
 |
2 | | indf1ofs 28921 |
. . . . 5
  𝟭                          |
3 | 1, 2 | ax-mp 5 |
. . . 4
 𝟭                         |
4 | | incom 3616 |
. . . . . . 7
           
                 |
5 | | eulerpart.r |
. . . . . . . 8
     
  |
6 | 5 | ineq2i 3622 |
. . . . . . 7
            
         |
7 | | dfrab2 3710 |
. . . . . . 7
     
    
       
        |
8 | 4, 6, 7 | 3eqtr4i 2503 |
. . . . . 6
                    |
9 | | elmapfun 7513 |
. . . . . . . . 9
     
  |
10 | | elmapi 7511 |
. . . . . . . . . 10
     
         |
11 | | frn 5747 |
. . . . . . . . . 10
       
     |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
     
     |
13 | | fimacnvinrn2 28312 |
. . . . . . . . . 10
          
            |
14 | | df-pr 3962 |
. . . . . . . . . . . . . 14
          |
15 | 14 | ineq2i 3622 |
. . . . . . . . . . . . 13
              |
16 | | indi 3680 |
. . . . . . . . . . . . 13
                   |
17 | | 0nnn 10663 |
. . . . . . . . . . . . . . 15
 |
18 | | disjsn 4023 |
. . . . . . . . . . . . . . 15
    
  |
19 | 17, 18 | mpbir 214 |
. . . . . . . . . . . . . 14
     |
20 | | 1nn 10642 |
. . . . . . . . . . . . . . . . 17
 |
21 | | 1ex 9656 |
. . . . . . . . . . . . . . . . . 18
 |
22 | 21 | snss 4087 |
. . . . . . . . . . . . . . . . 17

    |
23 | 20, 22 | mpbi 213 |
. . . . . . . . . . . . . . . 16
 
 |
24 | | dfss 3405 |
. . . . . . . . . . . . . . . 16
           |
25 | 23, 24 | mpbi 213 |
. . . . . . . . . . . . . . 15
       |
26 | | incom 3616 |
. . . . . . . . . . . . . . 15
   
     |
27 | 25, 26 | eqtr2i 2494 |
. . . . . . . . . . . . . 14
       |
28 | 19, 27 | uneq12i 3577 |
. . . . . . . . . . . . 13
          
    |
29 | 15, 16, 28 | 3eqtri 2497 |
. . . . . . . . . . . 12
     
    |
30 | | uncom 3569 |
. . . . . . . . . . . 12
         |
31 | | un0 3762 |
. . . . . . . . . . . 12
       |
32 | 29, 30, 31 | 3eqtri 2497 |
. . . . . . . . . . 11
        |
33 | 32 | imaeq2i 5172 |
. . . . . . . . . 10
                  |
34 | 13, 33 | syl6eq 2521 |
. . . . . . . . 9
          
         |
35 | 9, 12, 34 | syl2anc 673 |
. . . . . . . 8
     
              |
36 | 35 | eleq1d 2533 |
. . . . . . 7
     
     
          |
37 | 36 | rabbiia 3019 |
. . . . . 6
     
    
                |
38 | 8, 37 | eqtr2i 2494 |
. . . . 5
     
       
        |
39 | | f1oeq3 5820 |
. . . . 5
                    
   𝟭                         𝟭               
    |
40 | 38, 39 | ax-mp 5 |
. . . 4
  𝟭                         𝟭               
   |
41 | 3, 40 | mpbi 213 |
. . 3
 𝟭               
  |
42 | | eulerpart.j |
. . . . . . 7
   |
43 | | eulerpart.f |
. . . . . . 7
 
        |
44 | 42, 43 | oddpwdc 29260 |
. . . . . 6
       |
45 | | f1opwfi 7896 |
. . . . . 6
      
                         |
46 | 44, 45 | ax-mp 5 |
. . . . 5
                        |
47 | | eulerpart.p |
. . . . . . . 8
         
         |
48 | | eulerpart.o |
. . . . . . . 8
         |
49 | | eulerpart.d |
. . . . . . . 8
     
  |
50 | | eulerpart.h |
. . . . . . . 8
       supp    |
51 | | eulerpart.m |
. . . . . . . 8
    

        |
52 | 47, 48, 49, 42, 43, 50, 51 | eulerpartlem1 29273 |
. . . . . . 7
       
  |
53 | | bitsf1o 14498 |
. . . . . . . . . . . . . 14
bits          |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
bits           |
55 | 42, 1 | rabex2 4552 |
. . . . . . . . . . . . . 14
 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
  |
57 | | nn0ex 10899 |
. . . . . . . . . . . . . 14
 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
  |
59 | 57 | pwex 4584 |
. . . . . . . . . . . . . . 15
  |
60 | 59 | inex1 4537 |
. . . . . . . . . . . . . 14
 
  |
61 | 60 | a1i 11 |
. . . . . . . . . . . . 13
     |
62 | | 0nn0 10908 |
. . . . . . . . . . . . . 14
 |
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
  |
64 | | fvres 5893 |
. . . . . . . . . . . . . . 15

 bits     bits    |
65 | 62, 64 | ax-mp 5 |
. . . . . . . . . . . . . 14
 bits     bits   |
66 | | 0bits 14492 |
. . . . . . . . . . . . . 14
bits   |
67 | 65, 66 | eqtr2i 2494 |
. . . . . . . . . . . . 13
 bits      |
68 | | elmapi 7511 |
. . . . . . . . . . . . . . . . 17
         |
69 | | frnnn0supp 10947 |
. . . . . . . . . . . . . . . . 17
        supp         |
70 | 55, 68, 69 | sylancr 676 |
. . . . . . . . . . . . . . . 16
    supp         |
71 | 70 | eleq1d 2533 |
. . . . . . . . . . . . . . 15
     supp 
        |
72 | 71 | rabbiia 3019 |
. . . . . . . . . . . . . 14
    supp  
       
  |
73 | | elmapfun 7513 |
. . . . . . . . . . . . . . . 16
     |
74 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
75 | | funisfsupp 7906 |
. . . . . . . . . . . . . . . . 17
    finSupp
 supp     |
76 | 74, 62, 75 | mp3an23 1382 |
. . . . . . . . . . . . . . . 16

 finSupp  supp     |
77 | 73, 76 | syl 17 |
. . . . . . . . . . . . . . 15
    finSupp
 supp     |
78 | 77 | rabbiia 3019 |
. . . . . . . . . . . . . 14
   finSupp      supp    |
79 | | incom 3616 |
. . . . . . . . . . . . . . 15
                   
   |
80 | | dfrab2 3710 |
. . . . . . . . . . . . . . 15
       
       
     |
81 | 5 | ineq2i 3622 |
. . . . . . . . . . . . . . 15
                |
82 | 79, 80, 81 | 3eqtr4ri 2504 |
. . . . . . . . . . . . . 14
              |
83 | 72, 78, 82 | 3eqtr4ri 2504 |
. . . . . . . . . . . . 13
       finSupp   |
84 | | elmapfun 7513 |
. . . . . . . . . . . . . . 15
   
    |
85 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
86 | | 0ex 4528 |
. . . . . . . . . . . . . . . . 17
 |
87 | | funisfsupp 7906 |
. . . . . . . . . . . . . . . . 17
    finSupp
 supp     |
88 | 85, 86, 87 | mp3an23 1382 |
. . . . . . . . . . . . . . . 16

 finSupp  supp     |
89 | 88 | bicomd 206 |
. . . . . . . . . . . . . . 15

  supp  finSupp    |
90 | 84, 89 | syl 17 |
. . . . . . . . . . . . . 14
   
    supp  finSupp    |
91 | 90 | rabbiia 3019 |
. . . . . . . . . . . . 13
   
   supp         finSupp   |
92 | 54, 56, 58, 61, 63, 67, 83, 91 | fcobijfs 28386 |
. . . . . . . . . . . 12
   
  bits                   supp     |
93 | | elinel1 3610 |
. . . . . . . . . . . . . . . 16
         |
94 | | frn 5747 |
. . . . . . . . . . . . . . . . 17
    
  |
95 | | cores 5345 |
. . . . . . . . . . . . . . . . 17

 bits   bits    |
96 | 68, 94, 95 | 3syl 18 |
. . . . . . . . . . . . . . . 16
    bits   bits    |
97 | 93, 96 | syl 17 |
. . . . . . . . . . . . . . 15
      bits   bits    |
98 | 97 | mpteq2ia 4478 |
. . . . . . . . . . . . . 14
      bits         bits    |
99 | 98 | eqcomi 2480 |
. . . . . . . . . . . . 13
     bits      
  bits     |
100 | | f1oeq1 5818 |
. . . . . . . . . . . . 13
      bits         bits          bits
      
          supp  
      bits                   supp      |
101 | 99, 100 | mp1i 13 |
. . . . . . . . . . . 12
      bits
      
          supp  
      bits                   supp      |
102 | 92, 101 | mpbird 240 |
. . . . . . . . . . 11
   
 bits              
   supp     |
103 | 102 | trud 1461 |
. . . . . . . . . 10
     bits                  supp    |
104 | | ssrab2 3500 |
. . . . . . . . . . . . . . . 16
   |
105 | 42, 104 | eqsstri 3448 |
. . . . . . . . . . . . . . 15
 |
106 | 1, 57, 105 | 3pm3.2i 1208 |
. . . . . . . . . . . . . 14
   |
107 | | eulerpart.t |
. . . . . . . . . . . . . . . 16
          |
108 | | cnveq 5013 |
. . . . . . . . . . . . . . . . . . 19
 
   |
109 | | dfn2 10906 |
. . . . . . . . . . . . . . . . . . . 20
     |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
111 | 108, 110 | imaeq12d 5175 |
. . . . . . . . . . . . . . . . . 18
     
           |
112 | 111 | sseq1d 3445 |
. . . . . . . . . . . . . . . . 17
      
            |
113 | 112 | cbvrabv 3030 |
. . . . . . . . . . . . . . . 16
  
                    |
114 | 107, 113 | eqtri 2493 |
. . . . . . . . . . . . . . 15
              |
115 | | eqid 2471 |
. . . . . . . . . . . . . . 15
         |
116 | 114, 115 | resf1o 28390 |
. . . . . . . . . . . . . 14
  
   
          |
117 | 106, 62, 116 | mp2an 686 |
. . . . . . . . . . . . 13
           |
118 | | f1of1 5827 |
. . . . . . . . . . . . 13
  
                    |
119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . . 12
           |
120 | | inss1 3643 |
. . . . . . . . . . . 12
   |
121 | | f1ores 5842 |
. . . . . . . . . . . 12
             
      
          
         |
122 | 119, 120,
121 | mp2an 686 |
. . . . . . . . . . 11
  
                      |
123 | | vex 3034 |
. . . . . . . . . . . . . . . . . 18
 |
124 | 123 | resex 5154 |
. . . . . . . . . . . . . . . . 17
   |
125 | 124, 115 | fnmpti 5716 |
. . . . . . . . . . . . . . . 16
     |
126 | | fvelimab 5936 |
. . . . . . . . . . . . . . . 16
      
             
              |
127 | 125, 120,
126 | mp2an 686 |
. . . . . . . . . . . . . . 15
          
              |
128 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
             |
129 | | vex 3034 |
. . . . . . . . . . . . . . . . . 18
 |
130 | 129 | resex 5154 |
. . . . . . . . . . . . . . . . 17
   |
131 | 128, 130 | elrnmpti 5091 |
. . . . . . . . . . . . . . . 16
      
    
   |
132 | 47, 48, 49, 42, 43, 50, 51, 5, 107 | eulerpartlemt 29277 |
. . . . . . . . . . . . . . . . 17
           |
133 | 132 | eleq2i 2541 |
. . . . . . . . . . . . . . . 16
    
        |
134 | | elinel1 3610 |
. . . . . . . . . . . . . . . . . . 19
  
  |
135 | 115 | fvtresfn 5965 |
. . . . . . . . . . . . . . . . . . . 20
             |
136 | 135 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . 19
               |
137 | 134, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
        
     |
138 | | eqcom 2478 |
. . . . . . . . . . . . . . . . . 18
 


   |
139 | 137, 138 | syl6bb 269 |
. . . . . . . . . . . . . . . . 17
  
        

    |
140 | 139 | rexbiia 2880 |
. . . . . . . . . . . . . . . 16
            
    
   |
141 | 131, 133,
140 | 3bitr4ri 286 |
. . . . . . . . . . . . . . 15
            
      |
142 | 127, 141 | bitri 257 |
. . . . . . . . . . . . . 14
          
      |
143 | 142 | eqriv 2468 |
. . . . . . . . . . . . 13
  
            |
144 | | f1oeq3 5820 |
. . . . . . . . . . . . 13
                     
          
            
               |
145 | 143, 144 | ax-mp 5 |
. . . . . . . . . . . 12
     
                  
  
             
   |
146 | | resmpt 5160 |
. . . . . . . . . . . . 13
       
           |
147 | | f1oeq1 5818 |
. . . . . . . . . . . . 13
     
        
     
                                |
148 | 120, 146,
147 | mp2b 10 |
. . . . . . . . . . . 12
     
                               |
149 | 145, 148 | bitri 257 |
. . . . . . . . . . 11
     
                  
                  |
150 | 122, 149 | mpbi 213 |
. . . . . . . . . 10
                 |
151 | | f1oco 5850 |
. . . . . . . . . 10
     
 bits              
   supp                        
 bits                       supp     |
152 | 103, 150,
151 | mp2an 686 |
. . . . . . . . 9
      bits                       supp    |
153 | | f1of 5828 |
. . . . . . . . . . . . . 14
    
                          
   |
154 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
             |
155 | 154 | fmpt 6058 |
. . . . . . . . . . . . . . 15
 
       
    
          
   |
156 | 155 | biimpri 211 |
. . . . . . . . . . . . . 14
    
          
             |
157 | 150, 153,
156 | mp2b 10 |
. . . . . . . . . . . . 13
        
  |
158 | 157 | a1i 11 |
. . . . . . . . . . . 12
            |
159 | | eqidd 2472 |
. . . . . . . . . . . 12
              |
160 | | eqidd 2472 |
. . . . . . . . . . . 12
   
 bits        bits     |
161 | | coeq2 4998 |
. . . . . . . . . . . 12
   bits  bits      |
162 | 158, 159,
160, 161 | fmptcof 6073 |
. . . . . . . . . . 11
      bits
     
      bits       |
163 | 162 | eqcomd 2477 |
. . . . . . . . . 10
   bits           bits            |
164 | | eqidd 2472 |
. . . . . . . . . 10
      |
165 | 50 | a1i 11 |
. . . . . . . . . 10
       supp     |
166 | 163, 164,
165 | f1oeq123d 5824 |
. . . . . . . . 9
    bits
         
      bits                       supp      |
167 | 152, 166 | mpbiri 241 |
. . . . . . . 8
   bits             |
168 | 167 | trud 1461 |
. . . . . . 7
   bits
           |
169 | | f1oco 5850 |
. . . . . . 7
              bits            
   bits
              
   |
170 | 52, 168, 169 | mp2an 686 |
. . . . . 6
    bits
              
  |
171 | | eqidd 2472 |
. . . . . . . . . . 11
   bits        bits
      |
172 | | bitsf 14479 |
. . . . . . . . . . . . . 14
bits     |
173 | | zex 10970 |
. . . . . . . . . . . . . 14
 |
174 | | fex 6155 |
. . . . . . . . . . . . . 14
 bits     bits   |
175 | 172, 173,
174 | mp2an 686 |
. . . . . . . . . . . . 13
bits  |
176 | 175, 124 | coex 6764 |
. . . . . . . . . . . 12
bits     |
177 | 176 | a1i 11 |
. . . . . . . . . . 11
    bits      |
178 | 171, 177 | fvmpt2d 5974 |
. . . . . . . . . 10
        bits        bits      |
179 | | f1of 5828 |
. . . . . . . . . . . 12
    bits          
   bits
            |
180 | 167, 179 | syl 17 |
. . . . . . . . . . 11
   bits             |
181 | 180 | ffvelrnda 6037 |
. . . . . . . . . 10
        bits          |
182 | 178, 181 | eqeltrrd 2550 |
. . . . . . . . 9
    bits      |
183 | | f1ofn 5829 |
. . . . . . . . . . . 12
            |
184 | 52, 183 | ax-mp 5 |
. . . . . . . . . . 11
 |
185 | | dffn5 5924 |
. . . . . . . . . . 11

        |
186 | 184, 185 | mpbi 213 |
. . . . . . . . . 10
       |
187 | 186 | a1i 11 |
. . . . . . . . 9
        |
188 | | fveq2 5879 |
. . . . . . . . 9
 bits           bits       |
189 | 182, 171,
187, 188 | fmptco 6072 |
. . . . . . . 8
    bits            bits        |
190 | 189 | trud 1461 |
. . . . . . 7
    bits
           bits       |
191 | | f1oeq1 5818 |
. . . . . . 7
     bits
           bits           bits                
      bits                    |
192 | 190, 191 | ax-mp 5 |
. . . . . 6
     bits
              
       bits               
   |
193 | 170, 192 | mpbi 213 |
. . . . 5
      bits                  |
194 | | f1oco 5850 |
. . . . 5
      
           
            bits               
 
                  bits                  |
195 | 46, 193, 194 | mp2an 686 |
. . . 4
                  bits                 |
196 | | simpr 468 |
. . . . . . . . 9
        |
197 | | fvex 5889 |
. . . . . . . . 9
   bits      |
198 | | eqid 2471 |
. . . . . . . . . 10
      bits            bits       |
199 | 198 | fvmpt2 5972 |
. . . . . . . . 9
       bits             bits            bits       |
200 | 196, 197,
199 | sylancl 675 |
. . . . . . . 8
           bits            bits       |
201 | | f1of 5828 |
. . . . . . . . . 10
       bits               
       bits                   |
202 | 193, 201 | mp1i 13 |
. . . . . . . . 9
      bits                   |
203 | 202 | ffvelrnda 6037 |
. . . . . . . 8
           bits            
   |
204 | 200, 203 | eqeltrrd 2550 |
. . . . . . 7
       bits            |
205 | | eqidd 2472 |
. . . . . . 7
      bits            bits        |
206 | | eqidd 2472 |
. . . . . . 7
    
                   |
207 | | imaeq2 5170 |
. . . . . . 7
    bits               bits        |
208 | 204, 205,
206, 207 | fmptco 6072 |
. . . . . 6
                  bits                bits         |
209 | 208 | trud 1461 |
. . . . 5
                  bits                bits        |
210 | | f1oeq1 5818 |
. . . . 5
      
            bits                bits                          bits                         bits                   |
211 | 209, 210 | ax-mp 5 |
. . . 4
      
            bits                         bits                  |
212 | 195, 211 | mpbi 213 |
. . 3
         bits                 |
213 | | f1oco 5850 |
. . 3
   𝟭               
          bits                   𝟭            bits                   
   |
214 | 41, 212, 213 | mp2an 686 |
. 2
  𝟭            bits                   
  |
215 | | eulerpart.g |
. . . 4
    𝟭          bits         |
216 | 43 | mpt2exg 6887 |
. . . . . . . . . 10
     |
217 | 55, 57, 216 | mp2an 686 |
. . . . . . . . 9
 |
218 | | imaexg 6749 |
. . . . . . . . 9
       bits        |
219 | 217, 218 | ax-mp 5 |
. . . . . . . 8
      bits       |
220 | | eqid 2471 |
. . . . . . . . 9
         bits                bits        |
221 | 220 | fvmpt2 5972 |
. . . . . . . 8
          bits                 bits                bits        |
222 | 196, 219,
221 | sylancl 675 |
. . . . . . 7
              bits                bits        |
223 | | f1of 5828 |
. . . . . . . . 9
          bits                         bits                  |
224 | 212, 223 | mp1i 13 |
. . . . . . . 8
         bits                  |
225 | 224 | ffvelrnda 6037 |
. . . . . . 7
              bits               |
226 | 222, 225 | eqeltrrd 2550 |
. . . . . 6
          bits           |
227 | | eqidd 2472 |
. . . . . 6
         bits                bits         |
228 | | indf1o 28919 |
. . . . . . . . . . 11
 𝟭              |
229 | | f1ofn 5829 |
. . . . . . . . . . 11
 𝟭            𝟭     |
230 | 1, 228, 229 | mp2b 10 |
. . . . . . . . . 10
𝟭 
  |
231 | | dffn5 5924 |
. . . . . . . . . 10
 𝟭   𝟭     𝟭        |
232 | 230, 231 | mpbi 213 |
. . . . . . . . 9
𝟭 
   𝟭       |
233 | 232 | reseq1i 5107 |
. . . . . . . 8
 𝟭       𝟭        |
234 | | resmpt3 5161 |
. . . . . . . 8
    𝟭      
     𝟭       |
235 | 233, 234 | eqtri 2493 |
. . . . . . 7
 𝟭        𝟭       |
236 | 235 | a1i 11 |
. . . . . 6
 𝟭        𝟭        |
237 | | fveq2 5879 |
. . . . . 6
       bits       𝟭      𝟭          bits         |
238 | 226, 227,
236, 237 | fmptco 6072 |
. . . . 5
  𝟭            bits            𝟭          bits          |
239 | 238 | trud 1461 |
. . . 4
  𝟭            bits            𝟭          bits         |
240 | 215, 239 | eqtr4i 2496 |
. . 3
  𝟭            bits         |
241 | | f1oeq1 5818 |
. . 3
   𝟭            bits                    
   𝟭            bits                   
    |
242 | 240, 241 | ax-mp 5 |
. 2
            
   𝟭            bits                   
   |
243 | 214, 242 | mpbir 214 |
1
           
  |