Step | Hyp | Ref
| Expression |
1 | | o1fsum.2 |
. . 3
        |
2 | | nnssre 10613 |
. . . . 5
 |
3 | 2 | a1i 11 |
. . . 4

  |
4 | | o1fsum.1 |
. . . . 5
 

  |
5 | 4, 1 | o1mptrcl 13686 |
. . . 4
 

  |
6 | | 1red 9658 |
. . . 4
   |
7 | 3, 5, 6 | elo1mpt2 13599 |
. . 3
       
 
  
 
        |
8 | 1, 7 | mpbid 214 |
. 2
      
 
       |
9 | | rpssre 11312 |
. . . . . 6
 |
10 | 9 | a1i 11 |
. . . . 5
      
 
 
        |
11 | | nfcv 2592 |
. . . . . . . 8
   |
12 | | nfcsb1v 3379 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)  |
13 | | csbeq1a 3372 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   |
14 | 11, 12, 13 | cbvsumi 13763 |
. . . . . . 7
                      ![]_ ]_](_urbrack.gif)  |
15 | | fzfid 12186 |
. . . . . . . 8
       
  

                 |
16 | | o1f 13593 |
. . . . . . . . . . . . 13
                |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . 12
           |
18 | 4 | ralrimiva 2802 |
. . . . . . . . . . . . . 14
 
  |
19 | | dmmptg 5332 |
. . . . . . . . . . . . . 14
 
    |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . 13
     |
21 | 20 | feq2d 5715 |
. . . . . . . . . . . 12
                   |
22 | 17, 21 | mpbid 214 |
. . . . . . . . . . 11
         |
23 | | eqid 2451 |
. . . . . . . . . . . 12
     |
24 | 23 | fmpt 6043 |
. . . . . . . . . . 11
 
        |
25 | 22, 24 | sylibr 216 |
. . . . . . . . . 10
 
  |
26 | 25 | ad3antrrr 736 |
. . . . . . . . 9
       
  

       
  |
27 | | elfznn 11828 |
. . . . . . . . 9
           |
28 | 12 | nfel1 2606 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)
 |
29 | 13 | eleq1d 2513 |
. . . . . . . . . . 11
 
  ![]_ ]_](_urbrack.gif)    |
30 | 28, 29 | rspc 3144 |
. . . . . . . . . 10
  
  ![]_ ]_](_urbrack.gif)
   |
31 | 30 | impcom 432 |
. . . . . . . . 9
  
   ![]_ ]_](_urbrack.gif)   |
32 | 26, 27, 31 | syl2an 480 |
. . . . . . . 8
        
  

               
  ![]_ ]_](_urbrack.gif)   |
33 | 15, 32 | fsumcl 13799 |
. . . . . . 7
       
  

                   ![]_ ]_](_urbrack.gif)
  |
34 | 14, 33 | syl5eqel 2533 |
. . . . . 6
       
  

                   |
35 | | rpcn 11310 |
. . . . . . 7

  |
36 | 35 | adantl 468 |
. . . . . 6
       
  

         |
37 | | rpne0 11317 |
. . . . . . 7

  |
38 | 37 | adantl 468 |
. . . . . 6
       
  

         |
39 | 34, 36, 38 | divcld 10383 |
. . . . 5
       
  

                     |
40 | | simplrl 770 |
. . . . . . 7
      
 
 
           |
41 | | 1re 9642 |
. . . . . . . 8
 |
42 | | elicopnf 11730 |
. . . . . . . 8
    
     |
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
   
    |
44 | 40, 43 | sylib 200 |
. . . . . 6
      
 
 
          |
45 | 44 | simpld 461 |
. . . . 5
      
 
 
        |
46 | | fzfid 12186 |
. . . . . . 7
      
 
 
                |
47 | 25 | ad2antrr 732 |
. . . . . . . . 9
      
 
 
         |
48 | | elfznn 11828 |
. . . . . . . . 9
           |
49 | 47, 48, 31 | syl2an 480 |
. . . . . . . 8
       
  

              
  ![]_ ]_](_urbrack.gif)   |
50 | 49 | abscld 13498 |
. . . . . . 7
       
  

              
     ![]_ ]_](_urbrack.gif)    |
51 | 46, 50 | fsumrecl 13800 |
. . . . . 6
      
 
 
                     ![]_ ]_](_urbrack.gif)    |
52 | | simplrr 771 |
. . . . . 6
      
 
 
        |
53 | 51, 52 | readdcld 9670 |
. . . . 5
      
 
 
                      ![]_ ]_](_urbrack.gif)     |
54 | 34, 36, 38 | absdivd 13517 |
. . . . . . . 8
       
  

                                             |
55 | 54 | adantrr 723 |
. . . . . . 7
       
  

                                               |
56 | | rprege0 11316 |
. . . . . . . . . 10

    |
57 | 56 | ad2antrl 734 |
. . . . . . . . 9
       
  

             |
58 | | absid 13359 |
. . . . . . . . 9
         |
59 | 57, 58 | syl 17 |
. . . . . . . 8
       
  

               |
60 | 59 | oveq2d 6306 |
. . . . . . 7
       
  

             
                   
             |
61 | 55, 60 | eqtrd 2485 |
. . . . . 6
       
  

                                           |
62 | 34 | adantrr 723 |
. . . . . . . . 9
       
  

                     |
63 | 62 | abscld 13498 |
. . . . . . . 8
       
  

                         |
64 | | fzfid 12186 |
. . . . . . . . 9
       
  

                   |
65 | 47, 27, 31 | syl2an 480 |
. . . . . . . . . . 11
       
  

              
  ![]_ ]_](_urbrack.gif)   |
66 | 65 | adantlr 721 |
. . . . . . . . . 10
        
  

                 
  ![]_ ]_](_urbrack.gif)   |
67 | 66 | abscld 13498 |
. . . . . . . . 9
        
  

                 
     ![]_ ]_](_urbrack.gif)    |
68 | 64, 67 | fsumrecl 13800 |
. . . . . . . 8
       
  

                        ![]_ ]_](_urbrack.gif)    |
69 | 57 | simpld 461 |
. . . . . . . . 9
       
  

           |
70 | 51 | adantr 467 |
. . . . . . . . . 10
       
  

                        ![]_ ]_](_urbrack.gif)    |
71 | 52 | adantr 467 |
. . . . . . . . . 10
       
  

           |
72 | 70, 71 | readdcld 9670 |
. . . . . . . . 9
       
  

                         ![]_ ]_](_urbrack.gif)     |
73 | 69, 72 | remulcld 9671 |
. . . . . . . 8
       
  

                          ![]_ ]_](_urbrack.gif)      |
74 | 14 | fveq2i 5868 |
. . . . . . . . 9
                             ![]_ ]_](_urbrack.gif)   |
75 | 64, 66 | fsumabs 13861 |
. . . . . . . . 9
       
  

                        ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)    |
76 | 74, 75 | syl5eqbr 4436 |
. . . . . . . 8
       
  

                                      ![]_ ]_](_urbrack.gif)    |
77 | | fzfid 12186 |
. . . . . . . . . . 11
       
  

                         |
78 | | ssun2 3598 |
. . . . . . . . . . . . . 14
                                       |
79 | | flge1nn 12055 |
. . . . . . . . . . . . . . . . . 18
         |
80 | 44, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
      
 
 
            |
81 | 80 | adantr 467 |
. . . . . . . . . . . . . . . 16
       
  

               |
82 | 81 | nnred 10624 |
. . . . . . . . . . . . . . . . 17
       
  

               |
83 | 45 | adantr 467 |
. . . . . . . . . . . . . . . . 17
       
  

           |
84 | | flle 12035 |
. . . . . . . . . . . . . . . . . 18
       |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
       
  

               |
86 | | simprr 766 |
. . . . . . . . . . . . . . . . 17
       
  

           |
87 | 82, 83, 69, 85, 86 | letrd 9792 |
. . . . . . . . . . . . . . . 16
       
  

               |
88 | | fznnfl 12089 |
. . . . . . . . . . . . . . . . 17
             
             |
89 | 69, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
       
  

                     
             |
90 | 81, 87, 89 | mpbir2and 933 |
. . . . . . . . . . . . . . 15
       
  

                       |
91 | | fzsplit 11825 |
. . . . . . . . . . . . . . 15
                                               |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . 14
       
  

                                           |
93 | 78, 92 | syl5sseqr 3481 |
. . . . . . . . . . . . 13
       
  

                                 |
94 | 93 | sselda 3432 |
. . . . . . . . . . . 12
        
  

                       
          |
95 | 65 | abscld 13498 |
. . . . . . . . . . . . 13
       
  

              
     ![]_ ]_](_urbrack.gif)    |
96 | 95 | adantlr 721 |
. . . . . . . . . . . 12
        
  

                 
     ![]_ ]_](_urbrack.gif)    |
97 | 94, 96 | syldan 473 |
. . . . . . . . . . 11
        
  

                       
     ![]_ ]_](_urbrack.gif)    |
98 | 77, 97 | fsumrecl 13800 |
. . . . . . . . . 10
       
  

                              ![]_ ]_](_urbrack.gif)    |
99 | 69, 70 | remulcld 9671 |
. . . . . . . . . 10
       
  

                         ![]_ ]_](_urbrack.gif)     |
100 | 69, 71 | remulcld 9671 |
. . . . . . . . . 10
       
  

             |
101 | 70 | recnd 9669 |
. . . . . . . . . . . 12
       
  

                        ![]_ ]_](_urbrack.gif)    |
102 | 101 | mulid2d 9661 |
. . . . . . . . . . 11
       
  

                         ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)    |
103 | | 1red 9658 |
. . . . . . . . . . . 12
       
  

           |
104 | 49 | absge0d 13506 |
. . . . . . . . . . . . . . 15
       
  

              
     ![]_ ]_](_urbrack.gif)    |
105 | 46, 50, 104 | fsumge0 13855 |
. . . . . . . . . . . . . 14
      
 
 
      
              ![]_ ]_](_urbrack.gif)    |
106 | 51, 105 | jca 535 |
. . . . . . . . . . . . 13
      
 
 
                      ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)     |
107 | 106 | adantr 467 |
. . . . . . . . . . . 12
       
  

                         ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)     |
108 | 44 | simprd 465 |
. . . . . . . . . . . . . 14
      
 
 
        |
109 | 108 | adantr 467 |
. . . . . . . . . . . . 13
       
  

           |
110 | 103, 83, 69, 109, 86 | letrd 9792 |
. . . . . . . . . . . 12
       
  

           |
111 | | lemul1a 10459 |
. . . . . . . . . . . 12
                   ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)     |
112 | 103, 69, 107, 110, 111 | syl31anc 1271 |
. . . . . . . . . . 11
       
  

                         ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)     |
113 | 102, 112 | eqbrtrrd 4425 |
. . . . . . . . . 10
       
  

                        ![]_ ]_](_urbrack.gif) 
                ![]_ ]_](_urbrack.gif)     |
114 | | hashcl 12538 |
. . . . . . . . . . . . 13
                                   |
115 | | nn0re 10878 |
. . . . . . . . . . . . 13
                  
                    |
116 | 77, 114, 115 | 3syl 18 |
. . . . . . . . . . . 12
       
  

                             |
117 | 116, 71 | remulcld 9671 |
. . . . . . . . . . 11
       
  

                               |
118 | 71 | adantr 467 |
. . . . . . . . . . . . 13
        
  

                       
  |
119 | | elfzuz 11796 |
. . . . . . . . . . . . . 14
                           |
120 | 81 | peano2nnd 10626 |
. . . . . . . . . . . . . . . 16
       
  

                 |
121 | | eluznn 11229 |
. . . . . . . . . . . . . . . 16
       
          
  |
122 | 120, 121 | sylan 474 |
. . . . . . . . . . . . . . 15
        
  

                      |
123 | | simpllr 769 |
. . . . . . . . . . . . . . 15
        
  

                         
   |
124 | 83 | adantr 467 |
. . . . . . . . . . . . . . . 16
        
  

                      |
125 | | reflcl 12032 |
. . . . . . . . . . . . . . . . 17
       |
126 | | peano2re 9806 |
. . . . . . . . . . . . . . . . 17
             |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . 16
        
  

                            |
128 | 122 | nnred 10624 |
. . . . . . . . . . . . . . . 16
        
  

                      |
129 | | fllep1 12037 |
. . . . . . . . . . . . . . . . 17
         |
130 | 124, 129 | syl 17 |
. . . . . . . . . . . . . . . 16
        
  

                            |
131 | | eluzle 11171 |
. . . . . . . . . . . . . . . . 17
          
        |
132 | 131 | adantl 468 |
. . . . . . . . . . . . . . . 16
        
  

                            |
133 | 124, 127,
128, 130, 132 | letrd 9792 |
. . . . . . . . . . . . . . 15
        
  

                      |
134 | | nfv 1761 |
. . . . . . . . . . . . . . . . 17

 |
135 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . 19
   |
136 | 135, 12 | nffv 5872 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)   |
137 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . 18
  |
138 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . 18
   |
139 | 136, 137,
138 | nfbr 4447 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif) 
 |
140 | 134, 139 | nfim 2003 |
. . . . . . . . . . . . . . . 16
        ![]_ ]_](_urbrack.gif) 
  |
141 | | breq2 4406 |
. . . . . . . . . . . . . . . . 17
 
   |
142 | 13 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
          ![]_ ]_](_urbrack.gif)    |
143 | 142 | breq1d 4412 |
. . . . . . . . . . . . . . . . 17
     
     ![]_ ]_](_urbrack.gif)     |
144 | 141, 143 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
      
 
     ![]_ ]_](_urbrack.gif) 
    |
145 | 140, 144 | rspc 3144 |
. . . . . . . . . . . . . . 15
  
    
       ![]_ ]_](_urbrack.gif) 
    |
146 | 122, 123,
133, 145 | syl3c 63 |
. . . . . . . . . . . . . 14
        
  

                         ![]_ ]_](_urbrack.gif) 
  |
147 | 119, 146 | sylan2 477 |
. . . . . . . . . . . . 13
        
  

                       
     ![]_ ]_](_urbrack.gif)    |
148 | 77, 97, 118, 147 | fsumle 13859 |
. . . . . . . . . . . 12
       
  

                              ![]_ ]_](_urbrack.gif) 
                  |
149 | 71 | recnd 9669 |
. . . . . . . . . . . . 13
       
  

           |
150 | | fsumconst 13851 |
. . . . . . . . . . . . 13
                                                       |
151 | 77, 149, 150 | syl2anc 667 |
. . . . . . . . . . . 12
       
  

                                               |
152 | 148, 151 | breqtrd 4427 |
. . . . . . . . . . 11
       
  

                              ![]_ ]_](_urbrack.gif) 
                      |
153 | 120 | nnzd 11039 |
. . . . . . . . . . . . . 14
       
  

                 |
154 | | uzid 11173 |
. . . . . . . . . . . . . 14
                         |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . 13
       
  

                           |
156 | | 0red 9644 |
. . . . . . . . . . . . . . 15
        
  

                      |
157 | 47, 30 | mpan9 472 |
. . . . . . . . . . . . . . . . . 18
       
  

         ![]_ ]_](_urbrack.gif)
  |
158 | 157 | adantlr 721 |
. . . . . . . . . . . . . . . . 17
        
  

            ![]_ ]_](_urbrack.gif)   |
159 | 122, 158 | syldan 473 |
. . . . . . . . . . . . . . . 16
        
  

                      ![]_ ]_](_urbrack.gif)
  |
160 | 159 | abscld 13498 |
. . . . . . . . . . . . . . 15
        
  

                         ![]_ ]_](_urbrack.gif)    |
161 | 71 | adantr 467 |
. . . . . . . . . . . . . . 15
        
  

                      |
162 | 159 | absge0d 13506 |
. . . . . . . . . . . . . . 15
        
  

                         ![]_ ]_](_urbrack.gif)    |
163 | 156, 160,
161, 162, 146 | letrd 9792 |
. . . . . . . . . . . . . 14
        
  

                      |
164 | 163 | ralrimiva 2802 |
. . . . . . . . . . . . 13
       
  

                       |
165 | | biidd 241 |
. . . . . . . . . . . . . 14
       
   |
166 | 165 | rspcv 3146 |
. . . . . . . . . . . . 13
                
 
              |
167 | 155, 164,
166 | sylc 62 |
. . . . . . . . . . . 12
       
  

           |
168 | | reflcl 12032 |
. . . . . . . . . . . . . 14
       |
169 | 69, 168 | syl 17 |
. . . . . . . . . . . . 13
       
  

               |
170 | | ssdomg 7615 |
. . . . . . . . . . . . . . . 16
                                                         |
171 | 64, 93, 170 | sylc 62 |
. . . . . . . . . . . . . . 15
       
  

                                 |
172 | | hashdomi 12559 |
. . . . . . . . . . . . . . 15
                                        
              |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . 14
       
  

                                         |
174 | | flge0nn0 12054 |
. . . . . . . . . . . . . . 15
         |
175 | | hashfz1 12529 |
. . . . . . . . . . . . . . 15
    
                  |
176 | 57, 174, 175 | 3syl 18 |
. . . . . . . . . . . . . 14
       
  

                           |
177 | 173, 176 | breqtrd 4427 |
. . . . . . . . . . . . 13
       
  

                                 |
178 | | flle 12035 |
. . . . . . . . . . . . . 14
       |
179 | 69, 178 | syl 17 |
. . . . . . . . . . . . 13
       
  

               |
180 | 116, 169,
69, 177, 179 | letrd 9792 |
. . . . . . . . . . . 12
       
  

                             |
181 | 116, 69, 71, 167, 180 | lemul1ad 10546 |
. . . . . . . . . . 11
       
  

                                 |
182 | 98, 117, 100, 152, 181 | letrd 9792 |
. . . . . . . . . 10
       
  

                              ![]_ ]_](_urbrack.gif) 
    |
183 | 70, 98, 99, 100, 113, 182 | le2addd 10232 |
. . . . . . . . 9
       
  

                         ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)        |
184 | | ltp1 10443 |
. . . . . . . . . . 11
                 |
185 | | fzdisj 11826 |
. . . . . . . . . . 11
                                     |
186 | 82, 184, 185 | 3syl 18 |
. . . . . . . . . 10
       
  

                                   |
187 | 96 | recnd 9669 |
. . . . . . . . . 10
        
  

                 
     ![]_ ]_](_urbrack.gif)    |
188 | 186, 92, 64, 187 | fsumsplit 13806 |
. . . . . . . . 9
       
  

                        ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)     |
189 | 36 | adantrr 723 |
. . . . . . . . . 10
       
  

           |
190 | 189, 101,
149 | adddid 9667 |
. . . . . . . . 9
       
  

                          ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)        |
191 | 183, 188,
190 | 3brtr4d 4433 |
. . . . . . . 8
       
  

                        ![]_ ]_](_urbrack.gif) 
                 ![]_ ]_](_urbrack.gif)      |
192 | 63, 68, 73, 76, 191 | letrd 9792 |
. . . . . . 7
       
  

                                        ![]_ ]_](_urbrack.gif)      |
193 | | rpregt0 11315 |
. . . . . . . . 9

    |
194 | 193 | ad2antrl 734 |
. . . . . . . 8
       
  

             |
195 | | ledivmul 10481 |
. . . . . . . 8
     
                          ![]_ ]_](_urbrack.gif)                      
                ![]_ ]_](_urbrack.gif)      
         
                 ![]_ ]_](_urbrack.gif)       |
196 | 63, 72, 194, 195 | syl3anc 1268 |
. . . . . . 7
       
  

              
                           ![]_ ]_](_urbrack.gif)      
         
                 ![]_ ]_](_urbrack.gif)       |
197 | 192, 196 | mpbird 236 |
. . . . . 6
       
  

             
                           ![]_ ]_](_urbrack.gif)     |
198 | 61, 197 | eqbrtrd 4423 |
. . . . 5
       
  

                        
                ![]_ ]_](_urbrack.gif)     |
199 | 10, 39, 45, 53, 198 | elo1d 13600 |
. . . 4
      
 
 
        
                |
200 | 199 | ex 436 |
. . 3
 
       
    
                     |
201 | 200 | rexlimdvva 2886 |
. 2
         
                         |
202 | 8, 201 | mpd 15 |
1
                    |