Step | Hyp | Ref
| Expression |
1 | | simpl 459 |
. . . . . . . . . . . . 13
 
   |
2 | 1 | fveq1d 5867 |
. . . . . . . . . . . 12
 
           |
3 | 2 | oveq1d 6305 |
. . . . . . . . . . 11
 
               |
4 | 3 | sumeq2dv 13769 |
. . . . . . . . . 10
        
        |
5 | 4 | eqeq1d 2453 |
. . . . . . . . 9
        
          |
6 | 5 | cbvrabv 3044 |
. . . . . . . 8
                       |
7 | 6 | a1i 11 |
. . . . . . 7
                         |
8 | 7 | reseq2d 5105 |
. . . . . 6
              
              |
9 | | eqidd 2452 |
. . . . . 6
         
                         |
10 | 8, 7, 9 | f1oeq123d 5811 |
. . . . 5
                                              
                                              |
11 | 10 | imbi2d 318 |
. . . 4
                                               
                                               |
12 | | eulerpart.g |
. . . . 5
    𝟭          bits         |
13 | | eulerpart.p |
. . . . . . 7
         
         |
14 | | eulerpart.o |
. . . . . . 7
         |
15 | | eulerpart.d |
. . . . . . 7
     
  |
16 | | eulerpart.j |
. . . . . . 7
   |
17 | | eulerpart.f |
. . . . . . 7
 
        |
18 | | eulerpart.h |
. . . . . . 7
       supp    |
19 | | eulerpart.m |
. . . . . . 7
    

        |
20 | | eulerpart.r |
. . . . . . 7
     
  |
21 | | eulerpart.t |
. . . . . . 7
          |
22 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 12 | eulerpartgbij 29205 |
. . . . . 6
           
  |
23 | 22 | a1i 11 |
. . . . 5
               |
24 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
25 | | reseq1 5099 |
. . . . . . . . . . . . . . . . . 18
       |
26 | 25 | coeq2d 4997 |
. . . . . . . . . . . . . . . . 17
 bits    bits      |
27 | 26 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
    bits        bits       |
28 | 27 | imaeq2d 5168 |
. . . . . . . . . . . . . . 15
       bits            bits        |
29 | 28 | fveq2d 5869 |
. . . . . . . . . . . . . 14
  𝟭          bits        𝟭          bits         |
30 | 24, 29 | eqeq12d 2466 |
. . . . . . . . . . . . 13
       𝟭          bits      
     𝟭          bits          |
31 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 12 | eulerpartlemgv 29206 |
. . . . . . . . . . . . 13
  
     𝟭          bits         |
32 | 30, 31 | vtoclga 3113 |
. . . . . . . . . . . 12
  
     𝟭          bits         |
33 | 32 | 3ad2ant2 1030 |
. . . . . . . . . . 11
  
 𝟭          bits             𝟭          bits         |
34 | | simp3 1010 |
. . . . . . . . . . 11
  
 𝟭          bits         𝟭          bits         |
35 | 33, 34 | eqtr4d 2488 |
. . . . . . . . . 10
  
 𝟭          bits              |
36 | 35 | fveq1d 5867 |
. . . . . . . . 9
  
 𝟭          bits                      |
37 | 36 | oveq1d 6305 |
. . . . . . . 8
  
 𝟭          bits                          |
38 | 37 | sumeq2sdv 13770 |
. . . . . . 7
  
 𝟭          bits                            |
39 | 24 | fveq2d 5869 |
. . . . . . . . . . 11
                   |
40 | | fveq2 5865 |
. . . . . . . . . . 11
           |
41 | 39, 40 | eqeq12d 2466 |
. . . . . . . . . 10
             
               |
42 | | eulerpart.s |
. . . . . . . . . . 11
              |
43 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 12, 42 | eulerpartlemgs2 29213 |
. . . . . . . . . 10
  
              |
44 | 41, 43 | vtoclga 3113 |
. . . . . . . . 9
  
              |
45 | | nn0ex 10875 |
. . . . . . . . . . . . 13
 |
46 | | 0nn0 10884 |
. . . . . . . . . . . . . 14
 |
47 | | 1nn0 10885 |
. . . . . . . . . . . . . 14
 |
48 | | prssi 4128 |
. . . . . . . . . . . . . 14
 
   
  |
49 | 46, 47, 48 | mp2an 678 |
. . . . . . . . . . . . 13
    |
50 | | mapss 7514 |
. . . . . . . . . . . . 13
               |
51 | 45, 49, 50 | mp2an 678 |
. . . . . . . . . . . 12
        |
52 | | ssrin 3657 |
. . . . . . . . . . . 12
       
         
   |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . 11
         
  |
54 | | f1of 5814 |
. . . . . . . . . . . . 13
            
            
   |
55 | 22, 54 | ax-mp 5 |
. . . . . . . . . . . 12
              |
56 | 55 | ffvelrni 6021 |
. . . . . . . . . . 11
  
             |
57 | 53, 56 | sseldi 3430 |
. . . . . . . . . 10
  
          |
58 | 20, 42 | eulerpartlemsv1 29189 |
. . . . . . . . . 10
                              |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
  
        
            |
60 | 13, 14, 15, 16, 17, 18, 19, 20, 21 | eulerpartlemt0 29202 |
. . . . . . . . . . . 12
          
        |
61 | 60 | simp1bi 1023 |
. . . . . . . . . . 11
  
    |
62 | | inss2 3653 |
. . . . . . . . . . . 12
   |
63 | 62 | sseli 3428 |
. . . . . . . . . . 11
  
  |
64 | 61, 63 | elind 3618 |
. . . . . . . . . 10
  
  
   |
65 | 20, 42 | eulerpartlemsv1 29189 |
. . . . . . . . . 10
                  |
66 | 64, 65 | syl 17 |
. . . . . . . . 9
  
    
        |
67 | 44, 59, 66 | 3eqtr3d 2493 |
. . . . . . . 8
  
           
        |
68 | 67 | 3ad2ant2 1030 |
. . . . . . 7
  
 𝟭          bits                            |
69 | 38, 68 | eqtr3d 2487 |
. . . . . 6
  
 𝟭          bits                        |
70 | 69 | eqeq1d 2453 |
. . . . 5
  
 𝟭          bits                          |
71 | 12, 23, 70 | f1oresrab 6055 |
. . . 4
                                              |
72 | 11, 71 | chvarv 2107 |
. . 3
                                              |
73 | | cnveq 5008 |
. . . . . . . . . 10
 
   |
74 | 73 | imaeq1d 5167 |
. . . . . . . . 9
     
       |
75 | 74 | raleqdv 2993 |
. . . . . . . 8
  
              |
76 | 75 | cbvrabv 3044 |
. . . . . . 7
 
               |
77 | | nfrab1 2971 |
. . . . . . . 8
           |
78 | | nfrab1 2971 |
. . . . . . . 8
              |
79 | | df-3an 987 |
. . . . . . . . . . . 12
          

      
          
           |
80 | 79 | anbi1i 701 |
. . . . . . . . . . 11
           
             

             
                |
81 | 13 | eulerpartleme 29196 |
. . . . . . . . . . . 12

    
    

         |
82 | 81 | anbi1i 701 |
. . . . . . . . . . 11
                   

                |
83 | | an32 807 |
. . . . . . . . . . 11
       
    
       
                   
              
   |
84 | 80, 82, 83 | 3bitr4i 281 |
. . . . . . . . . 10
                    
       
          |
85 | 13, 14, 15, 16, 17, 18, 19, 20, 21 | eulerpartlemt0 29202 |
. . . . . . . . . . . . 13
          
        |
86 | | nnex 10615 |
. . . . . . . . . . . . . . 15
 |
87 | 45, 86 | elmap 7500 |
. . . . . . . . . . . . . 14
  
      |
88 | 87 | 3anbi1i 1199 |
. . . . . . . . . . . . 13
        
     
    
    
        |
89 | 85, 88 | bitri 253 |
. . . . . . . . . . . 12
       
    
        |
90 | | df-3an 987 |
. . . . . . . . . . . 12
          
     
          
     
   |
91 | | cnvimass 5188 |
. . . . . . . . . . . . . . . . . 18
    
 |
92 | | fdm 5733 |
. . . . . . . . . . . . . . . . . 18
       |
93 | 91, 92 | syl5sseq 3480 |
. . . . . . . . . . . . . . . . 17
            |
94 | | dfss3 3422 |
. . . . . . . . . . . . . . . . 17
     
         |
95 | 93, 94 | sylib 200 |
. . . . . . . . . . . . . . . 16
              |
96 | 95 | biantrurd 511 |
. . . . . . . . . . . . . . 15
                   
          |
97 | | dfss3 3422 |
. . . . . . . . . . . . . . . 16
     
         |
98 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . 19
 
   |
99 | 98 | notbid 296 |
. . . . . . . . . . . . . . . . . 18
 
   |
100 | 99, 16 | elrab2 3198 |
. . . . . . . . . . . . . . . . 17

    |
101 | 100 | ralbii 2819 |
. . . . . . . . . . . . . . . 16
 
     
           |
102 | | r19.26 2917 |
. . . . . . . . . . . . . . . 16
 
      
                  |
103 | 97, 101, 102 | 3bitri 275 |
. . . . . . . . . . . . . . 15
     
 
      
        |
104 | 96, 103 | syl6rbbr 268 |
. . . . . . . . . . . . . 14
          
     
   |
105 | 104 | adantr 467 |
. . . . . . . . . . . . 13
          
                |
106 | 105 | pm5.32i 643 |
. . . . . . . . . . . 12
                  
          
          |
107 | 89, 90, 106 | 3bitri 275 |
. . . . . . . . . . 11
             
          |
108 | 107 | anbi1i 701 |
. . . . . . . . . 10
           
             
                |
109 | 84, 108 | bitr4i 256 |
. . . . . . . . 9
           
          |
110 | | rabid 2967 |
. . . . . . . . 9
       


     
   |
111 | | rabid 2967 |
. . . . . . . . 9
              
          |
112 | 109, 110,
111 | 3bitr4i 281 |
. . . . . . . 8
       

             |
113 | 77, 78, 112 | eqri 28147 |
. . . . . . 7
 
                  |
114 | 14, 76, 113 | 3eqtri 2477 |
. . . . . 6
            |
115 | 114 | reseq2i 5102 |
. . . . 5
  
             |
116 | 115 | a1i 11 |
. . . 4
                 |
117 | 114 | a1i 11 |
. . . 4
             |
118 | | nfcv 2592 |
. . . . . 6
   |
119 | | nfrab1 2971 |
. . . . . 6
                   |
120 | | fnima 5694 |
. . . . . . . . . . . . . . . . 17
       |
121 | 120 | sseq1d 3459 |
. . . . . . . . . . . . . . . 16
        
      |
122 | 121 | anbi2d 710 |
. . . . . . . . . . . . . . 15
  
   
    
       |
123 | | sstr 3440 |
. . . . . . . . . . . . . . . . 17
           |
124 | 49, 123 | mpan2 677 |
. . . . . . . . . . . . . . . 16

  
  |
125 | 124 | pm4.71ri 639 |
. . . . . . . . . . . . . . 15

  

      |
126 | 122, 125 | syl6bbr 267 |
. . . . . . . . . . . . . 14
  
   
   
      |
127 | 126 | pm5.32i 643 |
. . . . . . . . . . . . 13
                   |
128 | | anass 655 |
. . . . . . . . . . . . 13
           
 
           |
129 | | df-f 5586 |
. . . . . . . . . . . . 13
       
       |
130 | 127, 128,
129 | 3bitr4ri 282 |
. . . . . . . . . . . 12
       
 
           |
131 | | prex 4642 |
. . . . . . . . . . . . 13
    |
132 | 131, 86 | elmap 7500 |
. . . . . . . . . . . 12
     
         |
133 | | df-f 5586 |
. . . . . . . . . . . . 13
    
    |
134 | 133 | anbi1i 701 |
. . . . . . . . . . . 12
             
 
           |
135 | 130, 132,
134 | 3bitr4i 281 |
. . . . . . . . . . 11
     
    
          |
136 | | vex 3048 |
. . . . . . . . . . . 12
 |
137 | | cnveq 5008 |
. . . . . . . . . . . . . 14
 
   |
138 | 137 | imaeq1d 5167 |
. . . . . . . . . . . . 13
     
       |
139 | 138 | eleq1d 2513 |
. . . . . . . . . . . 12
      
    
   |
140 | 136, 139,
20 | elab2 3188 |
. . . . . . . . . . 11

       |
141 | 135, 140 | anbi12i 703 |
. . . . . . . . . 10
      
          
            |
142 | | elin 3617 |
. . . . . . . . . 10
       
         |
143 | | an32 807 |
. . . . . . . . . 10
                    
                  
   |
144 | 141, 142,
143 | 3bitr4i 281 |
. . . . . . . . 9
       
          
           |
145 | 144 | anbi1i 701 |
. . . . . . . 8
                
                               |
146 | 13 | eulerpartleme 29196 |
. . . . . . . . . 10

    
    

         |
147 | 146 | anbi1i 701 |
. . . . . . . . 9
         
          

                 |
148 | | df-3an 987 |
. . . . . . . . . 10
          

      
          
           |
149 | 148 | anbi1i 701 |
. . . . . . . . 9
           
                           
            
      |
150 | | an32 807 |
. . . . . . . . 9
       
    
            
               
                   |
151 | 147, 149,
150 | 3bitri 275 |
. . . . . . . 8
         
                               |
152 | 145, 151 | bitr4i 256 |
. . . . . . 7
                

          |
153 | | rabid 2967 |
. . . . . . 7
       
                           |
154 | 13, 14, 15 | eulerpartlemd 29199 |
. . . . . . 7


          |
155 | 152, 153,
154 | 3bitr4ri 282 |
. . . . . 6

                  |
156 | 118, 119,
155 | eqri 28147 |
. . . . 5
                 |
157 | 156 | a1i 11 |
. . . 4
                  |
158 | 116, 117,
157 | f1oeq123d 5811 |
. . 3
       
                                              |
159 | 72, 158 | mpbird 236 |
. 2
        |
160 | 159 | trud 1453 |
1
       |