Step | Hyp | Ref
| Expression |
1 | | elmapi 7339 |
. . . . . . . . . 10
         |
2 | 1 | adantr 465 |
. . . . . . . . 9
   
       |
3 | | c0ex 9486 |
. . . . . . . . . . 11
 |
4 | 3 | fconst 5699 |
. . . . . . . . . 10
               |
5 | 4 | a1i 11 |
. . . . . . . . 9
   
                 |
6 | | disjdif 3854 |
. . . . . . . . . 10
     |
7 | 6 | a1i 11 |
. . . . . . . . 9
   
       |
8 | | fun 5678 |
. . . . . . . . 9
                          
                      |
9 | 2, 5, 7, 8 | syl21anc 1218 |
. . . . . . . 8
   
                       |
10 | | eulerpart.j |
. . . . . . . . . . 11
   |
11 | | ssrab2 3540 |
. . . . . . . . . . 11
   |
12 | 10, 11 | eqsstri 3489 |
. . . . . . . . . 10
 |
13 | | undif 3862 |
. . . . . . . . . 10

 
    |
14 | 12, 13 | mpbi 208 |
. . . . . . . . 9
     |
15 | | 0nn0 10700 |
. . . . . . . . . . 11
 |
16 | | snssi 4120 |
. . . . . . . . . . 11

 
  |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . 10
 
 |
18 | | ssequn2 3632 |
. . . . . . . . . 10
  
      |
19 | 17, 18 | mpbi 208 |
. . . . . . . . 9
     |
20 | 14, 19 | feq23i 5656 |
. . . . . . . 8
                    
              |
21 | 9, 20 | sylib 196 |
. . . . . . 7
   
               |
22 | | nn0ex 10691 |
. . . . . . . 8
 |
23 | | nnex 10434 |
. . . . . . . 8
 |
24 | 22, 23 | elmap 7346 |
. . . . . . 7
                         |
25 | 21, 24 | sylibr 212 |
. . . . . 6
   
             |
26 | | cnvun 5345 |
. . . . . . . . 9
          
         |
27 | 26 | imaeq1i 5269 |
. . . . . . . 8
            
               |
28 | | imaundir 5353 |
. . . . . . . 8
  
                              |
29 | 27, 28 | eqtri 2481 |
. . . . . . 7
            
     
             |
30 | | vex 3075 |
. . . . . . . . . . 11
 |
31 | | cnveq 5116 |
. . . . . . . . . . . . 13
 
   |
32 | 31 | imaeq1d 5271 |
. . . . . . . . . . . 12
     
       |
33 | 32 | eleq1d 2521 |
. . . . . . . . . . 11
      
    
   |
34 | | eulerpart.r |
. . . . . . . . . . 11
     
  |
35 | 30, 33, 34 | elab2 3210 |
. . . . . . . . . 10

       |
36 | 35 | biimpi 194 |
. . . . . . . . 9
     
  |
37 | 36 | adantl 466 |
. . . . . . . 8
   
     
  |
38 | | cnvxp 5358 |
. . . . . . . . . . . . . 14
          
   |
39 | 38 | dmeqi 5144 |
. . . . . . . . . . . . 13
              |
40 | | 2nn 10585 |
. . . . . . . . . . . . . . 15
 |
41 | | 2z 10784 |
. . . . . . . . . . . . . . . . 17
 |
42 | | iddvds 13659 |
. . . . . . . . . . . . . . . . 17
   |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 |
44 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . 19
 
   |
45 | 44 | notbid 294 |
. . . . . . . . . . . . . . . . . 18
 
   |
46 | 45, 10 | elrab2 3220 |
. . . . . . . . . . . . . . . . 17

    |
47 | 46 | simprbi 464 |
. . . . . . . . . . . . . . . 16
   |
48 | 43, 47 | mt2 179 |
. . . . . . . . . . . . . . 15
 |
49 | | eldif 3441 |
. . . . . . . . . . . . . . 15
  

   |
50 | 40, 48, 49 | mpbir2an 911 |
. . . . . . . . . . . . . 14
   |
51 | | ne0i 3746 |
. . . . . . . . . . . . . 14
       |
52 | | dmxp 5161 |
. . . . . . . . . . . . . 14
  
          |
53 | 50, 51, 52 | mp2b 10 |
. . . . . . . . . . . . 13
   
     |
54 | 39, 53 | eqtri 2481 |
. . . . . . . . . . . 12
          |
55 | 54 | ineq1i 3651 |
. . . . . . . . . . 11
              |
56 | | incom 3646 |
. . . . . . . . . . 11
         |
57 | | 0nnn 10459 |
. . . . . . . . . . . 12
 |
58 | | disjsn 4039 |
. . . . . . . . . . . 12
    
  |
59 | 57, 58 | mpbir 209 |
. . . . . . . . . . 11
     |
60 | 55, 56, 59 | 3eqtr2i 2487 |
. . . . . . . . . 10
          |
61 | | imadisj 5291 |
. . . . . . . . . 10
                    
  |
62 | 60, 61 | mpbir 209 |
. . . . . . . . 9
          
 |
63 | | 0fin 7646 |
. . . . . . . . 9
 |
64 | 62, 63 | eqeltri 2536 |
. . . . . . . 8
          
 |
65 | | unfi 7685 |
. . . . . . . 8
      
                                |
66 | 37, 64, 65 | sylancl 662 |
. . . . . . 7
   
                     |
67 | 29, 66 | syl5eqel 2544 |
. . . . . 6
   
                |
68 | | cnvimass 5292 |
. . . . . . . . 9
    
 |
69 | | fdm 5666 |
. . . . . . . . . 10
       |
70 | 2, 69 | syl 16 |
. . . . . . . . 9
   
   |
71 | 68, 70 | syl5sseq 3507 |
. . . . . . . 8
   
     
  |
72 | | 0ss 3769 |
. . . . . . . . . 10
 |
73 | 62, 72 | eqsstri 3489 |
. . . . . . . . 9
          
 |
74 | 73 | a1i 11 |
. . . . . . . 8
   
              |
75 | 71, 74 | unssd 3635 |
. . . . . . 7
   
                  
  |
76 | 29, 75 | syl5eqss 3503 |
. . . . . 6
   
                |
77 | | eulerpart.p |
. . . . . . 7
         
         |
78 | | eulerpart.o |
. . . . . . 7
         |
79 | | eulerpart.d |
. . . . . . 7
     
  |
80 | | eulerpart.f |
. . . . . . 7
 
        |
81 | | eulerpart.h |
. . . . . . 7
       supp    |
82 | | eulerpart.m |
. . . . . . 7
    

        |
83 | | eulerpart.t |
. . . . . . 7
          |
84 | 77, 78, 79, 10, 80, 81, 82, 34, 83 | eulerpartlemt0 26891 |
. . . . . 6
                     
            
            
   |
85 | 25, 67, 76, 84 | syl3anbrc 1172 |
. . . . 5
   
             |
86 | | resundir 5228 |
. . . . . 6
                       |
87 | | ffn 5662 |
. . . . . . . 8
       |
88 | | fnresdm 5623 |
. . . . . . . . 9
     |
89 | | incom 3646 |
. . . . . . . . . . . 12
         |
90 | 89, 6 | eqtri 2481 |
. . . . . . . . . . 11
     |
91 | | fnconstg 5701 |
. . . . . . . . . . . 12

          |
92 | | fnresdisj 5624 |
. . . . . . . . . . . 12
                         |
93 | 15, 91, 92 | mp2b 10 |
. . . . . . . . . . 11
   
       
   |
94 | 90, 93 | mpbi 208 |
. . . . . . . . . 10
         |
95 | 94 | a1i 11 |
. . . . . . . . 9
           |
96 | 88, 95 | uneq12d 3614 |
. . . . . . . 8
          
      |
97 | 2, 87, 96 | 3syl 20 |
. . . . . . 7
   
                 |
98 | | un0 3765 |
. . . . . . 7
   |
99 | 97, 98 | syl6eq 2509 |
. . . . . 6
   
               |
100 | 86, 99 | syl5req 2506 |
. . . . 5
   
             |
101 | | reseq1 5207 |
. . . . . . 7
                       |
102 | 101 | eqeq2d 2466 |
. . . . . 6
                         |
103 | 102 | rspcev 3173 |
. . . . 5
           
           
       |
104 | 85, 100, 103 | syl2anc 661 |
. . . 4
   
         |
105 | | simpr 461 |
. . . . . . 7
   
       |
106 | | simpl 457 |
. . . . . . . . . . . 12
   
  
    |
107 | 77, 78, 79, 10, 80, 81, 82, 34, 83 | eulerpartlemt0 26891 |
. . . . . . . . . . . 12
               
   |
108 | 106, 107 | sylib 196 |
. . . . . . . . . . 11
   
               
   |
109 | 108 | simp1d 1000 |
. . . . . . . . . 10
   
  
    |
110 | 22, 23 | elmap 7346 |
. . . . . . . . . 10
  
      |
111 | 109, 110 | sylib 196 |
. . . . . . . . 9
   
         |
112 | | fssres 5681 |
. . . . . . . . 9
               |
113 | 111, 12, 112 | sylancl 662 |
. . . . . . . 8
   
           |
114 | 23 | rabex 4546 |
. . . . . . . . . 10
   |
115 | 10, 114 | eqeltri 2536 |
. . . . . . . . 9
 |
116 | 22, 115 | elmap 7346 |
. . . . . . . 8
 
           |
117 | 113, 116 | sylibr 212 |
. . . . . . 7
   
         |
118 | 105, 117 | eqeltrd 2540 |
. . . . . 6
   
       |
119 | | ffun 5664 |
. . . . . . . . . 10
       |
120 | | respreima 5936 |
. . . . . . . . . 10

  
             |
121 | 111, 119,
120 | 3syl 20 |
. . . . . . . . 9
   
         
         |
122 | 108 | simp2d 1001 |
. . . . . . . . . 10
   
       
  |
123 | | infi 7642 |
. . . . . . . . . 10
           
   |
124 | 122, 123 | syl 16 |
. . . . . . . . 9
   
            |
125 | 121, 124 | eqeltrd 2540 |
. . . . . . . 8
   
         
  |
126 | | vex 3075 |
. . . . . . . . . 10
 |
127 | 126 | resex 5253 |
. . . . . . . . 9
   |
128 | | cnveq 5116 |
. . . . . . . . . . 11
   
     |
129 | 128 | imaeq1d 5271 |
. . . . . . . . . 10
       
  
      |
130 | 129 | eleq1d 2521 |
. . . . . . . . 9
        
      
   |
131 | 127, 130,
34 | elab2 3210 |
. . . . . . . 8
 

  
      |
132 | 125, 131 | sylibr 212 |
. . . . . . 7
   
       |
133 | 105, 132 | eqeltrd 2540 |
. . . . . 6
   
     |
134 | 118, 133 | jca 532 |
. . . . 5
   
         |
135 | 134 | rexlimiva 2936 |
. . . 4
         
   |
136 | 104, 135 | impbii 188 |
. . 3
   
         |
137 | 136 | abbii 2586 |
. 2
   
   
       |
138 | | df-in 3438 |
. 2
       
   |
139 | | eqid 2452 |
. . 3
             |
140 | 139 | rnmpt 5188 |
. 2
   
       
   |
141 | 137, 138,
140 | 3eqtr4i 2491 |
1
           |