Proof of Theorem eulerpartlemmf
Step | Hyp | Ref
| Expression |
1 | | bitsf1o 14419 |
. . . . 5
bits          |
2 | | f1of 5814 |
. . . . 5
 bits         bits           |
3 | 1, 2 | ax-mp 5 |
. . . 4
bits          |
4 | | eulerpart.p |
. . . . . . . . 9
         
         |
5 | | eulerpart.o |
. . . . . . . . 9
         |
6 | | eulerpart.d |
. . . . . . . . 9
     
  |
7 | | eulerpart.j |
. . . . . . . . 9
   |
8 | | eulerpart.f |
. . . . . . . . 9
 
        |
9 | | eulerpart.h |
. . . . . . . . 9
       supp    |
10 | | eulerpart.m |
. . . . . . . . 9
    

        |
11 | | eulerpart.r |
. . . . . . . . 9
     
  |
12 | | eulerpart.t |
. . . . . . . . 9
          |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | eulerpartlemt0 29202 |
. . . . . . . 8
               
   |
14 | 13 | biimpi 198 |
. . . . . . 7
  
            
   |
15 | 14 | simp1d 1020 |
. . . . . 6
  
    |
16 | | nn0ex 10875 |
. . . . . . 7
 |
17 | | nnex 10615 |
. . . . . . 7
 |
18 | 16, 17 | elmap 7500 |
. . . . . 6
  
      |
19 | 15, 18 | sylib 200 |
. . . . 5
  
      |
20 | | ssrab2 3514 |
. . . . . 6
   |
21 | 7, 20 | eqsstri 3462 |
. . . . 5
 |
22 | | fssres 5749 |
. . . . 5
               |
23 | 19, 21, 22 | sylancl 668 |
. . . 4
  
        |
24 | | fco2 5740 |
. . . 4
  bits                bits         
   |
25 | 3, 23, 24 | sylancr 669 |
. . 3
  
bits 
       
   |
26 | 16 | pwex 4586 |
. . . . 5
  |
27 | 26 | inex1 4544 |
. . . 4
 
  |
28 | 17, 21 | ssexi 4548 |
. . . 4
 |
29 | 27, 28 | elmap 7500 |
. . 3
 bits         bits
        
   |
30 | 25, 29 | sylibr 216 |
. 2
  
bits 
         |
31 | 14 | simp2d 1021 |
. . . . 5
  
       |
32 | | 0nn0 10884 |
. . . . . . . . 9
 |
33 | | suppimacnv 6925 |
. . . . . . . . 9
   
  supp
            |
34 | 32, 33 | mpan2 677 |
. . . . . . . 8
  
 supp             |
35 | | frnsuppeq 6926 |
. . . . . . . . . 10
 
       supp              |
36 | 17, 32, 35 | mp2an 678 |
. . . . . . . . 9
      supp      
      |
37 | 19, 36 | syl 17 |
. . . . . . . 8
  
 supp             |
38 | 34, 37 | eqtr3d 2487 |
. . . . . . 7
  
                    |
39 | 38 | eleq1d 2513 |
. . . . . 6
  
                      |
40 | | dfn2 10882 |
. . . . . . . 8
     |
41 | 40 | imaeq2i 5166 |
. . . . . . 7
               |
42 | 41 | eleq1i 2520 |
. . . . . 6
     
           |
43 | 39, 42 | syl6bbr 267 |
. . . . 5
  
                  |
44 | 31, 43 | mpbird 236 |
. . . 4
  
           |
45 | | resss 5128 |
. . . . 5
   |
46 | | cnvss 5007 |
. . . . 5
 

      |
47 | | imass1 5203 |
. . . . 5
                           |
48 | 45, 46, 47 | mp2b 10 |
. . . 4
          
          |
49 | | ssfi 7792 |
. . . 4
                                             |
50 | 44, 48, 49 | sylancl 668 |
. . 3
  
  
          |
51 | | cnvco 5020 |
. . . . . 6
 bits        bits |
52 | 51 | imaeq1i 5165 |
. . . . 5
  bits              
 bits        |
53 | | imaco 5340 |
. . . . 5
     bits         
    bits        |
54 | 52, 53 | eqtri 2473 |
. . . 4
  bits                  bits        |
55 | | ffun 5731 |
. . . . . 6
       |
56 | | funres 5621 |
. . . . . 6

    |
57 | 19, 55, 56 | 3syl 18 |
. . . . 5
  
    |
58 | | ssv 3452 |
. . . . . . 7
 bits   |
59 | | ssdif 3568 |
. . . . . . 7
  bits    bits   bits    
  bits       |
60 | 58, 59 | ax-mp 5 |
. . . . . 6
  bits   bits    
  bits      |
61 | | bitsf 14400 |
. . . . . . 7
bits     |
62 | | ffun 5731 |
. . . . . . 7
bits    bits |
63 | | difpreima 6008 |
. . . . . . 7
 bits  bits        bits   bits       |
64 | 61, 62, 63 | mp2b 10 |
. . . . . 6
 bits        bits   bits      |
65 | | bitsf1 14420 |
. . . . . . . . 9
bits     |
66 | | 0z 10948 |
. . . . . . . . . 10
 |
67 | | snssi 4116 |
. . . . . . . . . 10
  
  |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . 9
 
 |
69 | | f1imacnv 5830 |
. . . . . . . . 9
 bits      
 bits bits         |
70 | 65, 68, 69 | mp2an 678 |
. . . . . . . 8
 bits bits        |
71 | | ffn 5728 |
. . . . . . . . . . . 12
bits    bits   |
72 | 61, 71 | ax-mp 5 |
. . . . . . . . . . 11
bits  |
73 | | fnsnfv 5925 |
. . . . . . . . . . 11
 bits
  bits   bits      |
74 | 72, 66, 73 | mp2an 678 |
. . . . . . . . . 10
 bits   bits     |
75 | | 0bits 14413 |
. . . . . . . . . . 11
bits   |
76 | 75 | sneqi 3979 |
. . . . . . . . . 10
 bits      |
77 | 74, 76 | eqtr3i 2475 |
. . . . . . . . 9
bits       |
78 | 77 | imaeq2i 5166 |
. . . . . . . 8
 bits bits      bits     |
79 | 70, 78 | eqtr3i 2475 |
. . . . . . 7
   bits     |
80 | 79 | difeq2i 3548 |
. . . . . 6
      bits      |
81 | 60, 64, 80 | 3sstr4i 3471 |
. . . . 5
 bits           |
82 | | sspreima 28246 |
. . . . 5
     bits          
  
    bits                    |
83 | 57, 81, 82 | sylancl 668 |
. . . 4
  
  
    bits                    |
84 | 54, 83 | syl5eqss 3476 |
. . 3
  
  bits                        |
85 | | ssfi 7792 |
. . 3
               bits 
        
  
           bits
            |
86 | 50, 84, 85 | syl2anc 667 |
. 2
  
  bits             |
87 | | oveq1 6297 |
. . . . 5
 bits     supp   bits    supp    |
88 | 87 | eleq1d 2513 |
. . . 4
 bits      supp 
 bits
   supp     |
89 | 88, 9 | elrab2 3198 |
. . 3
 bits     bits 
        bits
   supp 
   |
90 | | zex 10946 |
. . . . . 6
 |
91 | | fex 6138 |
. . . . . 6
 bits     bits   |
92 | 61, 90, 91 | mp2an 678 |
. . . . 5
bits  |
93 | | resexg 5147 |
. . . . 5
  
    |
94 | | coexg 6744 |
. . . . 5
 bits
   bits      |
95 | 92, 93, 94 | sylancr 669 |
. . . 4
  
bits 
    |
96 | | 0ex 4535 |
. . . . . . 7
 |
97 | | suppimacnv 6925 |
. . . . . . 7
  bits   
  bits 
  supp    bits
            |
98 | 96, 97 | mpan2 677 |
. . . . . 6
 bits     bits 
  supp    bits
            |
99 | 98 | eleq1d 2513 |
. . . . 5
 bits      bits    supp    bits 
            |
100 | 99 | anbi2d 710 |
. . . 4
 bits      bits        
 bits    supp    bits      
    bits
              |
101 | 95, 100 | syl 17 |
. . 3
  
  bits
       
 bits    supp    bits      
    bits
              |
102 | 89, 101 | syl5bb 261 |
. 2
  
 bits   
 bits           bits
              |
103 | 30, 86, 102 | mpbir2and 933 |
1
  
bits 
    |