Proof of Theorem stoweidlem11
Step | Hyp | Ref
| Expression |
1 | | stoweidlem11.2 |
. . 3
   |
2 | | sumex 13831 |
. . 3
                 |
3 | | eqid 2471 |
. . . 4
                                     |
4 | 3 | fvmpt2 5972 |
. . 3
                                                           |
5 | 1, 2, 4 | sylancl 675 |
. 2
                                         |
6 | | fzfid 12224 |
. . . 4
       |
7 | | stoweidlem11.7 |
. . . . . . 7
   |
8 | 7 | rpred 11364 |
. . . . . 6
   |
9 | 8 | adantr 472 |
. . . . 5
 
       |
10 | | stoweidlem11.4 |
. . . . . 6
 
               |
11 | 1 | adantr 472 |
. . . . . 6
 
       |
12 | 10, 11 | ffvelrnd 6038 |
. . . . 5
 
               |
13 | 9, 12 | remulcld 9689 |
. . . 4
 
     
           |
14 | 6, 13 | fsumrecl 13877 |
. . 3
                   |
15 | | stoweidlem11.3 |
. . . . . . . . 9
       |
16 | | elfzuz 11822 |
. . . . . . . . 9
           |
17 | 15, 16 | syl 17 |
. . . . . . . 8
       |
18 | | eluz2 11188 |
. . . . . . . 8
         |
19 | 17, 18 | sylib 201 |
. . . . . . 7
     |
20 | 19 | simp2d 1043 |
. . . . . 6
   |
21 | 20 | zred 11063 |
. . . . 5
   |
22 | 8, 21 | remulcld 9689 |
. . . 4
     |
23 | | stoweidlem11.1 |
. . . . . . . 8
   |
24 | 23 | nnred 10646 |
. . . . . . 7
   |
25 | 24, 21 | resubcld 10068 |
. . . . . 6
     |
26 | | 1red 9676 |
. . . . . 6
   |
27 | 25, 26 | readdcld 9688 |
. . . . 5
       |
28 | 8, 23 | nndivred 10680 |
. . . . . 6
     |
29 | 8, 28 | remulcld 9689 |
. . . . 5
       |
30 | 27, 29 | remulcld 9689 |
. . . 4
      
      |
31 | 22, 30 | readdcld 9688 |
. . 3
                 |
32 | | 3re 10705 |
. . . . . . 7
 |
33 | 32 | a1i 11 |
. . . . . 6
   |
34 | | 3ne0 10726 |
. . . . . . 7
 |
35 | 34 | a1i 11 |
. . . . . 6
   |
36 | 33, 35 | rereccld 10456 |
. . . . 5
     |
37 | 21, 36 | readdcld 9688 |
. . . 4
       |
38 | 37, 8 | remulcld 9689 |
. . 3
         |
39 | | fzfid 12224 |
. . . . . 6
         |
40 | 8 | adantr 472 |
. . . . . . 7
 
         |
41 | | elfzelz 11826 |
. . . . . . . . . . . 12
       |
42 | | peano2zm 11004 |
. . . . . . . . . . . 12
     |
43 | 15, 41, 42 | 3syl 18 |
. . . . . . . . . . 11
     |
44 | 23 | nnzd 11062 |
. . . . . . . . . . 11
   |
45 | 21, 26 | resubcld 10068 |
. . . . . . . . . . . 12
     |
46 | 21 | lem1d 10562 |
. . . . . . . . . . . 12
  
  |
47 | | elfzuz3 11823 |
. . . . . . . . . . . . 13
           |
48 | | eluzle 11195 |
. . . . . . . . . . . . 13
    
  |
49 | 15, 47, 48 | 3syl 18 |
. . . . . . . . . . . 12

  |
50 | 45, 21, 24, 46, 49 | letrd 9809 |
. . . . . . . . . . 11
  
  |
51 | | eluz2 11188 |
. . . . . . . . . . 11
               |
52 | 43, 44, 50, 51 | syl3anbrc 1214 |
. . . . . . . . . 10
         |
53 | | fzss2 11864 |
. . . . . . . . . 10
      
            |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
      
      |
55 | 54 | sselda 3418 |
. . . . . . . 8
 
             |
56 | 55, 12 | syldan 478 |
. . . . . . 7
 
                 |
57 | 40, 56 | remulcld 9689 |
. . . . . 6
 
       
           |
58 | 39, 57 | fsumrecl 13877 |
. . . . 5
                     |
59 | 58, 30 | readdcld 9688 |
. . . 4
                          
      |
60 | 21 | ltm1d 10561 |
. . . . . . 7
     |
61 | | fzdisj 11852 |
. . . . . . 7
                 |
62 | 60, 61 | syl 17 |
. . . . . 6
               |
63 | | fzssp1 11867 |
. . . . . . . . . 10
               |
64 | 23 | nncnd 10647 |
. . . . . . . . . . . 12
   |
65 | | 1cnd 9677 |
. . . . . . . . . . . 12
   |
66 | 64, 65 | npcand 10009 |
. . . . . . . . . . 11
       |
67 | 66 | oveq2d 6324 |
. . . . . . . . . 10
               |
68 | 63, 67 | syl5sseq 3466 |
. . . . . . . . 9
    
 
      |
69 | | 1zzd 10992 |
. . . . . . . . . . . 12
   |
70 | | fzsubel 11860 |
. . . . . . . . . . . 12
                         |
71 | 69, 44, 20, 69, 70 | syl22anc 1293 |
. . . . . . . . . . 11
                   |
72 | 15, 71 | mpbid 215 |
. . . . . . . . . 10
             |
73 | | 1m1e0 10700 |
. . . . . . . . . . 11
   |
74 | 73 | oveq1i 6318 |
. . . . . . . . . 10
           
   |
75 | 72, 74 | syl6eleq 2559 |
. . . . . . . . 9
           |
76 | 68, 75 | sseldd 3419 |
. . . . . . . 8
         |
77 | | fzsplit 11851 |
. . . . . . . 8
                             |
78 | 76, 77 | syl 17 |
. . . . . . 7
                       |
79 | 20 | zcnd 11064 |
. . . . . . . . . 10
   |
80 | 79, 65 | npcand 10009 |
. . . . . . . . 9
       |
81 | 80 | oveq1d 6323 |
. . . . . . . 8
               |
82 | 81 | uneq2d 3579 |
. . . . . . 7
                               |
83 | 78, 82 | eqtrd 2505 |
. . . . . 6
                   |
84 | 7 | rpcnd 11366 |
. . . . . . . 8
   |
85 | 84 | adantr 472 |
. . . . . . 7
 
       |
86 | 12 | recnd 9687 |
. . . . . . 7
 
               |
87 | 85, 86 | mulcld 9681 |
. . . . . 6
 
     
           |
88 | 62, 83, 6, 87 | fsumsplit 13883 |
. . . . 5
                  
                                    |
89 | | fzfid 12224 |
. . . . . . 7
       |
90 | 8 | adantr 472 |
. . . . . . . 8
 
       |
91 | | 0zd 10973 |
. . . . . . . . . . . . 13
   |
92 | | 0red 9662 |
. . . . . . . . . . . . . 14
   |
93 | | 0le1 10158 |
. . . . . . . . . . . . . . 15
 |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . 14

  |
95 | 19 | simp3d 1044 |
. . . . . . . . . . . . . 14

  |
96 | 92, 26, 21, 94, 95 | letrd 9809 |
. . . . . . . . . . . . 13

  |
97 | | eluz2 11188 |
. . . . . . . . . . . . 13
         |
98 | 91, 20, 96, 97 | syl3anbrc 1214 |
. . . . . . . . . . . 12
       |
99 | | fzss1 11863 |
. . . . . . . . . . . 12
    
          |
100 | 98, 99 | syl 17 |
. . . . . . . . . . 11
    
      |
101 | 100 | sselda 3418 |
. . . . . . . . . 10
 
           |
102 | 101, 10 | syldan 478 |
. . . . . . . . 9
 
               |
103 | 1 | adantr 472 |
. . . . . . . . 9
 
       |
104 | 102, 103 | ffvelrnd 6038 |
. . . . . . . 8
 
               |
105 | 90, 104 | remulcld 9689 |
. . . . . . 7
 
     
           |
106 | 89, 105 | fsumrecl 13877 |
. . . . . 6
                   |
107 | | eluzfz2 11833 |
. . . . . . . . 9
    
      |
108 | | ne0i 3728 |
. . . . . . . . 9
           |
109 | 15, 47, 107, 108 | 4syl 19 |
. . . . . . . 8
       |
110 | 23 | adantr 472 |
. . . . . . . . . 10
 
       |
111 | 90, 110 | nndivred 10680 |
. . . . . . . . 9
 
         |
112 | 90, 111 | remulcld 9689 |
. . . . . . . 8
 
     
     |
113 | | stoweidlem11.6 |
. . . . . . . . 9
 
                 |
114 | 7 | rpgt0d 11367 |
. . . . . . . . . . 11
   |
115 | 114 | adantr 472 |
. . . . . . . . . 10
 
       |
116 | | ltmul2 10478 |
. . . . . . . . . 10
          
 
 
                     
      |
117 | 104, 111,
90, 115, 116 | syl112anc 1296 |
. . . . . . . . 9
 
             
 
          
      |
118 | 113, 117 | mpbid 215 |
. . . . . . . 8
 
     
               |
119 | 89, 109, 105, 112, 118 | fsumlt 13937 |
. . . . . . 7
                
       
    |
120 | 23 | nnne0d 10676 |
. . . . . . . . . . 11
   |
121 | 84, 64, 120 | divcld 10405 |
. . . . . . . . . 10
     |
122 | 84, 121 | mulcld 9681 |
. . . . . . . . 9
       |
123 | | fsumconst 13928 |
. . . . . . . . 9
      
                       
      |
124 | 89, 122, 123 | syl2anc 673 |
. . . . . . . 8
                    
      |
125 | | hashfz 12640 |
. . . . . . . . . 10
    
              |
126 | 15, 47, 125 | 3syl 18 |
. . . . . . . . 9
               |
127 | 126 | oveq1d 6323 |
. . . . . . . 8
           
        
      |
128 | 124, 127 | eqtrd 2505 |
. . . . . . 7
                       |
129 | 119, 128 | breqtrd 4420 |
. . . . . 6
                
      
     |
130 | 106, 30, 58, 129 | ltadd2dd 9811 |
. . . . 5
                                                              
      |
131 | 88, 130 | eqbrtrd 4416 |
. . . 4
                
 
                              |
132 | | stoweidlem11.5 |
. . . . . . . . . 10
 
               |
133 | 55, 132 | syldan 478 |
. . . . . . . . 9
 
                 |
134 | | 1red 9676 |
. . . . . . . . . 10
 
         |
135 | 114 | adantr 472 |
. . . . . . . . . 10
 
         |
136 | | lemul2 10480 |
. . . . . . . . . 10
         

                          |
137 | 56, 134, 40, 135, 136 | syl112anc 1296 |
. . . . . . . . 9
 
               
          
    |
138 | 133, 137 | mpbid 215 |
. . . . . . . 8
 
       
             |
139 | 84 | mulid1d 9678 |
. . . . . . . . 9
     |
140 | 139 | adantr 472 |
. . . . . . . 8
 
       
   |
141 | 138, 140 | breqtrd 4420 |
. . . . . . 7
 
       
           |
142 | 39, 57, 40, 141 | fsumle 13936 |
. . . . . 6
                  
          |
143 | | fsumconst 13928 |
. . . . . . . 8
       
                       |
144 | 39, 84, 143 | syl2anc 673 |
. . . . . . 7
                       |
145 | | 0z 10972 |
. . . . . . . . . . 11
 |
146 | | 1e0p1 11102 |
. . . . . . . . . . . . 13
   |
147 | 146 | fveq2i 5882 |
. . . . . . . . . . . 12
           |
148 | 17, 147 | syl6eleq 2559 |
. . . . . . . . . . 11
         |
149 | | eluzp1m1 11206 |
. . . . . . . . . . 11
 
               |
150 | 145, 148,
149 | sylancr 676 |
. . . . . . . . . 10
         |
151 | | hashfz 12640 |
. . . . . . . . . 10
      
                  |
152 | 150, 151 | syl 17 |
. . . . . . . . 9
                   |
153 | 79, 65 | subcld 10005 |
. . . . . . . . . . 11
     |
154 | 153 | subid1d 9994 |
. . . . . . . . . 10
         |
155 | 154 | oveq1d 6323 |
. . . . . . . . 9
             |
156 | 152, 155,
80 | 3eqtrd 2509 |
. . . . . . . 8
             |
157 | 156 | oveq1d 6323 |
. . . . . . 7
                 |
158 | 79, 84 | mulcomd 9682 |
. . . . . . 7
       |
159 | 144, 157,
158 | 3eqtrd 2509 |
. . . . . 6
             |
160 | 142, 159 | breqtrd 4420 |
. . . . 5
                  
    |
161 | 58, 22, 30, 160 | leadd1dd 10248 |
. . . 4
                          
            
       |
162 | 14, 59, 31, 131, 161 | ltletrd 9812 |
. . 3
                
 
              |
163 | 8, 8 | remulcld 9689 |
. . . . 5
     |
164 | 22, 163 | readdcld 9688 |
. . . 4
         |
165 | 64, 79 | subcld 10005 |
. . . . . . . 8
     |
166 | 165, 65 | addcld 9680 |
. . . . . . 7
       |
167 | 84, 166, 121 | mul12d 9860 |
. . . . . 6
                 
     |
168 | 167 | oveq2d 6324 |
. . . . 5
                               |
169 | 27, 28 | remulcld 9689 |
. . . . . . 7
           |
170 | 8, 169 | remulcld 9689 |
. . . . . 6
             |
171 | 166, 84, 64, 120 | div12d 10441 |
. . . . . . . 8
                   |
172 | 26, 21 | resubcld 10068 |
. . . . . . . . . . . . . 14
     |
173 | | elfzle1 11828 |
. . . . . . . . . . . . . . . 16
       |
174 | 15, 173 | syl 17 |
. . . . . . . . . . . . . . 15

  |
175 | 26, 21 | suble0d 10225 |
. . . . . . . . . . . . . . 15
       |
176 | 174, 175 | mpbird 240 |
. . . . . . . . . . . . . 14
  
  |
177 | 172, 92, 24, 176 | leadd2dd 10249 |
. . . . . . . . . . . . 13
    
    |
178 | 64, 65, 79 | addsub12d 10028 |
. . . . . . . . . . . . . 14
           |
179 | 65, 165 | addcomd 9853 |
. . . . . . . . . . . . . 14
           |
180 | 178, 179 | eqtrd 2505 |
. . . . . . . . . . . . 13
           |
181 | 64 | addid1d 9851 |
. . . . . . . . . . . . 13
     |
182 | 177, 180,
181 | 3brtr3d 4425 |
. . . . . . . . . . . 12
    
  |
183 | 23 | nngt0d 10675 |
. . . . . . . . . . . . 13
   |
184 | | lediv1 10492 |
. . . . . . . . . . . . 13
     

                  |
185 | 27, 24, 24, 183, 184 | syl112anc 1296 |
. . . . . . . . . . . 12
                 |
186 | 182, 185 | mpbid 215 |
. . . . . . . . . . 11
      
    |
187 | 64, 120 | dividd 10403 |
. . . . . . . . . . 11
     |
188 | 186, 187 | breqtrd 4420 |
. . . . . . . . . 10
      
  |
189 | 27, 23 | nndivred 10680 |
. . . . . . . . . . 11
         |
190 | 189, 26, 7 | lemul2d 11405 |
. . . . . . . . . 10
                     |
191 | 188, 190 | mpbid 215 |
. . . . . . . . 9
        
    |
192 | 191, 139 | breqtrd 4420 |
. . . . . . . 8
        
  |
193 | 171, 192 | eqbrtrd 4416 |
. . . . . . 7
           |
194 | 169, 8, 7 | lemul2d 11405 |
. . . . . . 7
                         |
195 | 193, 194 | mpbid 215 |
. . . . . 6
          
    |
196 | 170, 163,
22, 195 | leadd2dd 10249 |
. . . . 5
              
 
      |
197 | 168, 196 | eqbrtrrd 4418 |
. . . 4
              
 
      |
198 | 84, 79 | mulcomd 9682 |
. . . . . . 7
       |
199 | 198 | oveq1d 6323 |
. . . . . 6
               |
200 | 79, 84, 84 | adddird 9686 |
. . . . . 6
             |
201 | 199, 200 | eqtr4d 2508 |
. . . . 5
             |
202 | 21, 8 | readdcld 9688 |
. . . . . 6
     |
203 | | stoweidlem11.8 |
. . . . . . 7
     |
204 | 8, 36, 21, 203 | ltadd2dd 9811 |
. . . . . 6
  
      |
205 | 202, 37, 7, 204 | ltmul1dd 11416 |
. . . . 5
    
        |
206 | 201, 205 | eqbrtrd 4416 |
. . . 4
               |
207 | 31, 164, 38, 197, 206 | lelttrd 9810 |
. . 3
                       |
208 | 14, 31, 38, 162, 207 | lttrd 9813 |
. 2
                
        |
209 | 5, 208 | eqbrtrd 4416 |
1
                      
        |