Step | Hyp | Ref
| Expression |
1 | | eulerpartlems.r |
. . . . . 6
     
  |
2 | | eulerpartlems.s |
. . . . . 6
              |
3 | 1, 2 | eulerpartlemsf 29240 |
. . . . 5
    
    |
4 | 3 | ffvelrni 6043 |
. . . 4
           |
5 | | nndiffz1 28414 |
. . . . 5
    
                      |
6 | 5 | eleq2d 2524 |
. . . 4
    
          
             |
7 | 4, 6 | syl 17 |
. . 3
               
             |
8 | 7 | pm5.32i 647 |
. 2
     
          
   
              |
9 | | simpr 467 |
. . . . . 6
     
                       |
10 | | eldif 3425 |
. . . . . 6
          
            |
11 | 9, 10 | sylib 201 |
. . . . 5
     
                       |
12 | 11 | simpld 465 |
. . . 4
     
             |
13 | 1, 2 | eulerpartlemelr 29238 |
. . . . . 6
                  |
14 | 13 | simpld 465 |
. . . . 5
           |
15 | 14 | ffvelrnda 6044 |
. . . 4
     
       |
16 | 12, 15 | syldan 477 |
. . 3
     
                 |
17 | | simpl 463 |
. . . 4
     
          
      |
18 | 4 | adantr 471 |
. . . . 5
     
                 |
19 | 11 | simprd 469 |
. . . . 5
     
          
          |
20 | | simpl 463 |
. . . . . . . . . 10
         |
21 | | nnuz 11222 |
. . . . . . . . . 10
     |
22 | 20, 21 | syl6eleq 2549 |
. . . . . . . . 9
             |
23 | | simpr 467 |
. . . . . . . . . 10
             |
24 | 23 | nn0zd 11066 |
. . . . . . . . 9
             |
25 | | elfz5 11820 |
. . . . . . . . 9
                   
       |
26 | 22, 24, 25 | syl2anc 671 |
. . . . . . . 8
               
       |
27 | 26 | notbid 300 |
. . . . . . 7
               
       |
28 | 23 | nn0red 10954 |
. . . . . . . 8
             |
29 | 20 | nnred 10651 |
. . . . . . . 8
         |
30 | 28, 29 | ltnled 9807 |
. . . . . . 7
           
       |
31 | 27, 30 | bitr4d 264 |
. . . . . 6
                       |
32 | 31 | biimpa 491 |
. . . . 5
                
      |
33 | 12, 18, 19, 32 | syl21anc 1275 |
. . . 4
     
              
  |
34 | 1, 2 | eulerpartlemsv1 29237 |
. . . . . . . . . 10
                  |
35 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
36 | | id 22 |
. . . . . . . . . . . 12
   |
37 | 35, 36 | oveq12d 6332 |
. . . . . . . . . . 11
               |
38 | 37 | cbvsumv 13810 |
. . . . . . . . . 10
       
       |
39 | 34, 38 | syl6req 2512 |
. . . . . . . . 9
                  |
40 | | breq2 4419 |
. . . . . . . . . . . . 13
     
       |
41 | | fveq2 5887 |
. . . . . . . . . . . . . 14
           |
42 | 41 | breq2d 4427 |
. . . . . . . . . . . . 13
 
   
       |
43 | 40, 42 | anbi12d 722 |
. . . . . . . . . . . 12
      
         
        |
44 | 43 | cbvrexv 3031 |
. . . . . . . . . . 11
      
    
     
       |
45 | 4 | adantr 471 |
. . . . . . . . . . . . . 14
           
            |
46 | 45 | nn0red 10954 |
. . . . . . . . . . . . 13
           
            |
47 | 4 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
      
     
     
      |
48 | 47 | nn0red 10954 |
. . . . . . . . . . . . . . 15
      
     
     
      |
49 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
     
   |
50 | 49 | adantr 471 |
. . . . . . . . . . . . . . . 16
      
     
     
  |
51 | 50 | nnred 10651 |
. . . . . . . . . . . . . . 15
      
     
     
  |
52 | | 1zzd 10996 |
. . . . . . . . . . . . . . . . 17
     
   |
53 | 14 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
      

       |
54 | | simpr 467 |
. . . . . . . . . . . . . . . . . 18
      

   |
55 | | eqidd 2462 |
. . . . . . . . . . . . . . . . . . 19
     
                   |
56 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . 21
        
  |
57 | 56 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . . 20
        
          |
58 | 57, 56 | oveq12d 6332 |
. . . . . . . . . . . . . . . . . . 19
        
              |
59 | | simpr 467 |
. . . . . . . . . . . . . . . . . . 19
     
   |
60 | | ffvelrn 6042 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
61 | 59 | nnnn0d 10953 |
. . . . . . . . . . . . . . . . . . . 20
     
   |
62 | 60, 61 | nn0mulcld 10958 |
. . . . . . . . . . . . . . . . . . 19
     
         |
63 | 55, 58, 59, 62 | fvmptd 5976 |
. . . . . . . . . . . . . . . . . 18
     
                     |
64 | 53, 54, 63 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
      

                     |
65 | 14 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
66 | 65 | ffvelrnda 6044 |
. . . . . . . . . . . . . . . . . . 19
      

       |
67 | 54 | nnnn0d 10953 |
. . . . . . . . . . . . . . . . . . 19
      

   |
68 | 66, 67 | nn0mulcld 10958 |
. . . . . . . . . . . . . . . . . 18
      

         |
69 | 68 | nn0red 10954 |
. . . . . . . . . . . . . . . . 17
      

         |
70 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
71 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
72 | 70, 71 | oveq12d 6332 |
. . . . . . . . . . . . . . . . . . . . 21
               |
73 | 72 | cbvmptv 4508 |
. . . . . . . . . . . . . . . . . . . 20
                 |
74 | 68, 73 | fmptd 6068 |
. . . . . . . . . . . . . . . . . . 19
     
               |
75 | | nn0sscn 10902 |
. . . . . . . . . . . . . . . . . . 19
 |
76 | | fss 5759 |
. . . . . . . . . . . . . . . . . . 19
             
               |
77 | 74, 75, 76 | sylancl 673 |
. . . . . . . . . . . . . . . . . 18
     
               |
78 | | nnex 10642 |
. . . . . . . . . . . . . . . . . . . . 21
 |
79 | | 0nn0 10912 |
. . . . . . . . . . . . . . . . . . . . 21
 |
80 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
81 | 80 | ffs2 28361 |
. . . . . . . . . . . . . . . . . . . . 21
 
                      supp                     |
82 | 78, 79, 81 | mp3an12 1363 |
. . . . . . . . . . . . . . . . . . . 20
                      supp                     |
83 | 77, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     
          supp                     |
84 | | frnnn0supp 10951 |
. . . . . . . . . . . . . . . . . . . . . 22
        supp         |
85 | 78, 65, 84 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . . 21
     
  supp         |
86 | 13 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . 22
            |
87 | 86 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
     
     
  |
88 | 85, 87 | eqeltrd 2539 |
. . . . . . . . . . . . . . . . . . . 20
     
  supp    |
89 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
90 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
91 | | ffn 5750 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
92 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
           |
93 | 92 | oveq1d 6329 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
               |
94 | | simp2 1015 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
95 | 94 | nncnd 10652 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       |
96 | 95 | mul02d 9856 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
         |
97 | 93, 96 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . . . . 22
     
             |
98 | 73, 89, 90, 91, 97 | suppss3 28360 |
. . . . . . . . . . . . . . . . . . . . 21
              supp   supp    |
99 | 65, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
     
          supp 
 supp    |
100 | | ssfi 7817 |
. . . . . . . . . . . . . . . . . . . 20
   supp           supp   supp            supp    |
101 | 88, 99, 100 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
     
          supp    |
102 | 83, 101 | eqeltrrd 2540 |
. . . . . . . . . . . . . . . . . 18
     
                    |
103 | 21, 52, 77, 102 | fsumcvg4 28804 |
. . . . . . . . . . . . . . . . 17
     
             |
104 | 21, 52, 64, 69, 103 | isumrecl 13874 |
. . . . . . . . . . . . . . . 16
     
          |
105 | 104 | adantr 471 |
. . . . . . . . . . . . . . 15
      
     
     
         |
106 | | simprl 769 |
. . . . . . . . . . . . . . 15
      
     
     
      |
107 | 14 | ffvelrnda 6044 |
. . . . . . . . . . . . . . . . . . 19
     
       |
108 | 107 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
      
     
     
      |
109 | 108 | nn0red 10954 |
. . . . . . . . . . . . . . . . 17
      
     
     
      |
110 | 109, 51 | remulcld 9696 |
. . . . . . . . . . . . . . . 16
      
     
     
        |
111 | 50 | nnnn0d 10953 |
. . . . . . . . . . . . . . . . . 18
      
     
     
  |
112 | 111 | nn0ge0d 10956 |
. . . . . . . . . . . . . . . . 17
      
     
     
  |
113 | | simprr 771 |
. . . . . . . . . . . . . . . . . 18
      
     
     
      |
114 | | elnnnn0b 10942 |
. . . . . . . . . . . . . . . . . . 19
    
            |
115 | | nnge1 10662 |
. . . . . . . . . . . . . . . . . . 19
           |
116 | 114, 115 | sylbir 218 |
. . . . . . . . . . . . . . . . . 18
          
      |
117 | 108, 113,
116 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
      
     
     
      |
118 | 51, 109, 112, 117 | lemulge12d 10572 |
. . . . . . . . . . . . . . . 16
      
     
     
        |
119 | 107 | nn0cnd 10955 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
120 | 49 | nncnd 10652 |
. . . . . . . . . . . . . . . . . . . 20
     
   |
121 | 119, 120 | mulcld 9688 |
. . . . . . . . . . . . . . . . . . 19
     
         |
122 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
   |
123 | 41, 122 | oveq12d 6332 |
. . . . . . . . . . . . . . . . . . . 20
               |
124 | 123 | sumsn 13855 |
. . . . . . . . . . . . . . . . . . 19
                          |
125 | 49, 121, 124 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
     
                  |
126 | | snfi 7675 |
. . . . . . . . . . . . . . . . . . . 20
   |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     
     |
128 | 49 | snssd 4129 |
. . . . . . . . . . . . . . . . . . 19
     
     |
129 | 68 | nn0ge0d 10956 |
. . . . . . . . . . . . . . . . . . 19
      

         |
130 | 21, 52, 127, 128, 64, 69, 129, 103 | isumless 13951 |
. . . . . . . . . . . . . . . . . 18
     
                   |
131 | 125, 130 | eqbrtrrd 4438 |
. . . . . . . . . . . . . . . . 17
     
      
         |
132 | 131 | adantr 471 |
. . . . . . . . . . . . . . . 16
      
     
     
               |
133 | 51, 110, 105, 118, 132 | letrd 9817 |
. . . . . . . . . . . . . . 15
      
     
     
         |
134 | 48, 51, 105, 106, 133 | ltletrd 9820 |
. . . . . . . . . . . . . 14
      
     
     
    
        |
135 | 134 | r19.29an 2942 |
. . . . . . . . . . . . 13
           
          
        |
136 | 46, 135 | gtned 9795 |
. . . . . . . . . . . 12
           
                   |
137 | 136 | ex 440 |
. . . . . . . . . . 11
      
    
                   |
138 | 44, 137 | syl5bi 225 |
. . . . . . . . . 10
      
    
                   |
139 | 138 | necon2bd 2651 |
. . . . . . . . 9
                      
        |
140 | 39, 139 | mpd 15 |
. . . . . . . 8
          
       |
141 | | ralnex 2845 |
. . . . . . . 8
 
    
          
       |
142 | 140, 141 | sylibr 217 |
. . . . . . 7
                  |
143 | | imnan 428 |
. . . . . . . 8
     
         
       |
144 | 143 | ralbii 2830 |
. . . . . . 7
 
    
     
    
       |
145 | 142, 144 | sylibr 217 |
. . . . . 6
          
       |
146 | 145 | r19.21bi 2768 |
. . . . 5
     
             |
147 | 146 | imp 435 |
. . . 4
      
    
       |
148 | 17, 12, 33, 147 | syl21anc 1275 |
. . 3
     
          
      |
149 | | nn0re 10906 |
. . . . . 6
    
      |
150 | | 0red 9669 |
. . . . . 6
    
  |
151 | 149, 150 | lenltd 9806 |
. . . . 5
    
    
       |
152 | | nn0le0eq0 10926 |
. . . . 5
    
    
       |
153 | 151, 152 | bitr3d 263 |
. . . 4
    
    
       |
154 | 153 | biimpa 491 |
. . 3
     
           |
155 | 16, 148, 154 | syl2anc 671 |
. 2
     
                 |
156 | 8, 155 | sylbir 218 |
1
     
                 |