Proof of Theorem axlowdimlem16
Step | Hyp | Ref
| Expression |
1 | | elfz1eq 11807 |
. . . . . 6
       |
2 | | oveq1 6295 |
. . . . . . . . . . 11
       |
3 | | df-3 10666 |
. . . . . . . . . . 11
   |
4 | 2, 3 | syl6reqr 2503 |
. . . . . . . . . 10
     |
5 | 4, 4 | oveq12d 6306 |
. . . . . . . . 9
               |
6 | 5 | sumeq1d 13760 |
. . . . . . . 8
               
                   |
7 | 2, 3 | syl6eqr 2502 |
. . . . . . . . . 10
     |
8 | | 3z 10967 |
. . . . . . . . . 10
 |
9 | 7, 8 | syl6eqel 2536 |
. . . . . . . . 9
     |
10 | | ax-1cn 9594 |
. . . . . . . . . 10
 |
11 | 10 | sqcli 12352 |
. . . . . . . . 9
     |
12 | | fveq2 5863 |
. . . . . . . . . . . 12
          
    |
13 | | axlowdimlem16.2 |
. . . . . . . . . . . . 13
                        |
14 | 13 | axlowdimlem11 24975 |
. . . . . . . . . . . 12
       |
15 | 12, 14 | syl6eq 2500 |
. . . . . . . . . . 11
         |
16 | 15 | oveq1d 6303 |
. . . . . . . . . 10
                 |
17 | 16 | fsum1 13801 |
. . . . . . . . 9
                                 |
18 | 9, 11, 17 | sylancl 667 |
. . . . . . . 8
                         |
19 | 6, 18 | eqtrd 2484 |
. . . . . . 7
                     |
20 | | fveq2 5863 |
. . . . . . . . . . . 12
           |
21 | | axlowdimlem16.1 |
. . . . . . . . . . . . 13
                     |
22 | 21 | axlowdimlem8 24972 |
. . . . . . . . . . . 12
      |
23 | 20, 22 | syl6eq 2500 |
. . . . . . . . . . 11
        |
24 | 23 | oveq1d 6303 |
. . . . . . . . . 10
                |
25 | | sqneg 12332 |
. . . . . . . . . . 11
            |
26 | 10, 25 | ax-mp 5 |
. . . . . . . . . 10
          |
27 | 24, 26 | syl6eq 2500 |
. . . . . . . . 9
               |
28 | 27 | fsum1 13801 |
. . . . . . . 8
                           |
29 | 8, 11, 28 | mp2an 677 |
. . . . . . 7
                   |
30 | 19, 29 | syl6reqr 2503 |
. . . . . 6
               
               |
31 | 1, 30 | syl 17 |
. . . . 5
                   
               |
32 | 31 | a1i 11 |
. . . 4
                                     |
33 | | oveq1 6295 |
. . . . . . 7
 
     |
34 | | 3m1e2 10723 |
. . . . . . 7
   |
35 | 33, 34 | syl6eq 2500 |
. . . . . 6
 
   |
36 | 35 | oveq2d 6304 |
. . . . 5
             |
37 | 36 | eleq2d 2513 |
. . . 4
       
       |
38 | | oveq2 6296 |
. . . . . 6
           |
39 | 38 | sumeq1d 13760 |
. . . . 5
               
               |
40 | 38 | sumeq1d 13760 |
. . . . 5
               
               |
41 | 39, 40 | eqeq12d 2465 |
. . . 4
                                                             |
42 | 32, 37, 41 | 3imtr4d 272 |
. . 3
                                       |
43 | 42 | adantld 469 |
. 2
      
                                      |
44 | | simprl 763 |
. . . 4
      
       
      |
45 | | eluzle 11168 |
. . . . . . 7
    
  |
46 | 45 | adantl 468 |
. . . . . 6
      
  |
47 | | simpl 459 |
. . . . . 6
         |
48 | | 3re 10680 |
. . . . . . 7
 |
49 | | eluzelre 11166 |
. . . . . . . 8
    
  |
50 | 49 | adantl 468 |
. . . . . . 7
      
  |
51 | | ltlen 9732 |
. . . . . . 7
 
  
    |
52 | 48, 50, 51 | sylancr 668 |
. . . . . 6
        
    |
53 | 46, 47, 52 | mpbir2and 932 |
. . . . 5
      
  |
54 | 53 | adantrr 722 |
. . . 4
      
       
  |
55 | | simprr 765 |
. . . 4
      
       
   
    |
56 | | fzssp1 11838 |
. . . . . . . . . . . . 13
               |
57 | | simp3 1009 |
. . . . . . . . . . . . 13
         
      
    |
58 | 56, 57 | sseldi 3429 |
. . . . . . . . . . . 12
         
             |
59 | | eluzelz 11165 |
. . . . . . . . . . . . . . . 16
    
  |
60 | 59 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . 15
         
     |
61 | 60 | zcnd 11038 |
. . . . . . . . . . . . . 14
         
     |
62 | | npcan 9881 |
. . . . . . . . . . . . . 14
 
       |
63 | 61, 10, 62 | sylancl 667 |
. . . . . . . . . . . . 13
         
         |
64 | 63 | oveq2d 6304 |
. . . . . . . . . . . 12
         
                 |
65 | 58, 64 | eleqtrd 2530 |
. . . . . . . . . . 11
         
         |
66 | | elfzelz 11797 |
. . . . . . . . . . 11
       |
67 | 65, 66 | syl 17 |
. . . . . . . . . 10
         
     |
68 | 67 | zred 11037 |
. . . . . . . . 9
         
     |
69 | 68 | ltp1d 10534 |
. . . . . . . 8
         
       |
70 | | fzdisj 11823 |
. . . . . . . 8
       
         |
71 | 69, 70 | syl 17 |
. . . . . . 7
         
       
         |
72 | | fzsplit 11822 |
. . . . . . . 8
                       |
73 | 65, 72 | syl 17 |
. . . . . . 7
         
                     |
74 | | fzfid 12183 |
. . . . . . 7
         
         |
75 | | eluzge3nn 11197 |
. . . . . . . . . . 11
    
  |
76 | | 2eluzge1 11202 |
. . . . . . . . . . . . 13
     |
77 | | fzss1 11834 |
. . . . . . . . . . . . 13
    
         
    |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . . 12
         
   |
79 | 78 | sseli 3427 |
. . . . . . . . . . 11
          
    |
80 | 13 | axlowdimlem10 24974 |
. . . . . . . . . . 11
 
             |
81 | 75, 79, 80 | syl2an 480 |
. . . . . . . . . 10
         
         |
82 | | fzss1 11834 |
. . . . . . . . . . . 12
    
          |
83 | 76, 82 | ax-mp 5 |
. . . . . . . . . . 11
         |
84 | 83 | sseli 3427 |
. . . . . . . . . 10
           |
85 | | fveecn 24925 |
. . . . . . . . . 10
     
           |
86 | 81, 84, 85 | syl2an 480 |
. . . . . . . . 9
      
           
      |
87 | 86 | sqcld 12411 |
. . . . . . . 8
      
           
          |
88 | 87 | 3adantl2 1164 |
. . . . . . 7
          
                  |
89 | 71, 73, 74, 88 | fsumsplit 13799 |
. . . . . 6
         
                                                   |
90 | | fzss1 11834 |
. . . . . . . . . . . . . . . 16
    
          |
91 | 76, 90 | ax-mp 5 |
. . . . . . . . . . . . . . 15
         |
92 | 91 | sseli 3427 |
. . . . . . . . . . . . . 14
           |
93 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . 20
         |
94 | 93 | zred 11037 |
. . . . . . . . . . . . . . . . . . 19
         |
95 | 94 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . 18
         
     |
96 | 49 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . 18
         
     |
97 | | peano2rem 9938 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
         
   
   |
99 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . 20
           |
100 | 99 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . 19
         
       |
101 | 96 | ltm1d 10536 |
. . . . . . . . . . . . . . . . . . 19
         
   
   |
102 | 95, 98, 96, 100, 101 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . 18
         
     |
103 | 95, 96, 102 | ltled 9780 |
. . . . . . . . . . . . . . . . 17
         
     |
104 | 93 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . 18
         
     |
105 | | eluz 11169 |
. . . . . . . . . . . . . . . . . 18
 
     
   |
106 | 104, 60, 105 | syl2anc 666 |
. . . . . . . . . . . . . . . . 17
         
   
   
   |
107 | 103, 106 | mpbird 236 |
. . . . . . . . . . . . . . . 16
         
         |
108 | | fzss2 11835 |
. . . . . . . . . . . . . . . 16
    
          |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . 15
         
             |
110 | 109 | sseld 3430 |
. . . . . . . . . . . . . 14
         
               |
111 | 92, 110 | syl5 33 |
. . . . . . . . . . . . 13
         
               |
112 | 111 | imp 431 |
. . . . . . . . . . . 12
          
              |
113 | | elfzelz 11797 |
. . . . . . . . . . . . . . 15
       |
114 | 113 | zred 11037 |
. . . . . . . . . . . . . 14
       |
115 | 114 | adantl 468 |
. . . . . . . . . . . . 13
          
          |
116 | 95 | adantr 467 |
. . . . . . . . . . . . . 14
          
          |
117 | | peano2re 9803 |
. . . . . . . . . . . . . . . . 17
     |
118 | 94, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
           |
119 | 118 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . 15
         
       |
120 | 119 | adantr 467 |
. . . . . . . . . . . . . 14
          
            |
121 | | elfzle2 11800 |
. . . . . . . . . . . . . . 15
       |
122 | 121 | adantl 468 |
. . . . . . . . . . . . . 14
          
          |
123 | 116 | ltp1d 10534 |
. . . . . . . . . . . . . 14
          
            |
124 | 115, 116,
120, 122, 123 | lelttrd 9790 |
. . . . . . . . . . . . 13
          
            |
125 | 115, 124 | ltned 9768 |
. . . . . . . . . . . 12
          
            |
126 | 13 | axlowdimlem12 24976 |
. . . . . . . . . . . 12
               |
127 | 112, 125,
126 | syl2anc 666 |
. . . . . . . . . . 11
          
              |
128 | 127 | sq0id 12365 |
. . . . . . . . . 10
          
                  |
129 | 128 | sumeq2dv 13762 |
. . . . . . . . 9
         
                 
       |
130 | | fzfi 12182 |
. . . . . . . . . . 11
     |
131 | 130 | olci 393 |
. . . . . . . . . 10
               |
132 | | sumz 13781 |
. . . . . . . . . 10
     
                 |
133 | 131, 132 | ax-mp 5 |
. . . . . . . . 9
       |
134 | 129, 133 | syl6eq 2500 |
. . . . . . . 8
         
                   |
135 | 104 | peano2zd 11040 |
. . . . . . . . . . 11
         
       |
136 | | sq1 12366 |
. . . . . . . . . . . . 13
     |
137 | 16, 136 | syl6eq 2500 |
. . . . . . . . . . . 12
             |
138 | 137 | fsum1 13801 |
. . . . . . . . . . 11
   
                     |
139 | 135, 10, 138 | sylancl 667 |
. . . . . . . . . 10
         
                       |
140 | | oveq2 6296 |
. . . . . . . . . . . 12
                   |
141 | 140 | sumeq1d 13760 |
. . . . . . . . . . 11
                     
                 |
142 | 141 | eqeq1d 2452 |
. . . . . . . . . 10
                     
                   |
143 | 139, 142 | syl5ib 223 |
. . . . . . . . 9
            
                      |
144 | 104 | adantl 468 |
. . . . . . . . . . . . . . . 16
    
       
   
  |
145 | 144 | zred 11037 |
. . . . . . . . . . . . . . 15
    
       
   
  |
146 | 60 | adantl 468 |
. . . . . . . . . . . . . . . . 17
    
       
   
  |
147 | 146 | zred 11037 |
. . . . . . . . . . . . . . . 16
    
       
   
  |
148 | 147, 97 | syl 17 |
. . . . . . . . . . . . . . 15
    
       
        |
149 | 100 | adantl 468 |
. . . . . . . . . . . . . . 15
    
       
        |
150 | 147 | ltm1d 10536 |
. . . . . . . . . . . . . . 15
    
       
        |
151 | 145, 148,
147, 149, 150 | lelttrd 9790 |
. . . . . . . . . . . . . 14
    
       
      |
152 | | 1red 9655 |
. . . . . . . . . . . . . . . . . . 19
         |
153 | | 2re 10676 |
. . . . . . . . . . . . . . . . . . . 20
 |
154 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
         |
155 | | 1le2 10820 |
. . . . . . . . . . . . . . . . . . . 20
 |
156 | 155 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
         |
157 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . 19
         |
158 | 152, 154,
94, 156, 157 | letrd 9789 |
. . . . . . . . . . . . . . . . . 18
         |
159 | 158 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . 17
         
     |
160 | 159 | adantl 468 |
. . . . . . . . . . . . . . . 16
    
       
   
  |
161 | | elnnz1 10960 |
. . . . . . . . . . . . . . . 16

    |
162 | 144, 160,
161 | sylanbrc 669 |
. . . . . . . . . . . . . . 15
    
       
   
  |
163 | 75 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . 16
         
     |
164 | 163 | adantl 468 |
. . . . . . . . . . . . . . 15
    
       
   
  |
165 | | nnltp1le 10989 |
. . . . . . . . . . . . . . 15
 
       |
166 | 162, 164,
165 | syl2anc 666 |
. . . . . . . . . . . . . 14
    
       
          |
167 | 151, 166 | mpbid 214 |
. . . . . . . . . . . . 13
    
       
     
  |
168 | 135 | adantl 468 |
. . . . . . . . . . . . . 14
    
       
        |
169 | | eluz 11169 |
. . . . . . . . . . . . . 14
   
       
     |
170 | 168, 146,
169 | syl2anc 666 |
. . . . . . . . . . . . 13
    
       
          
     |
171 | 167, 170 | mpbird 236 |
. . . . . . . . . . . 12
    
       
   
   
    |
172 | | simpr1 1013 |
. . . . . . . . . . . . . . . 16
    
       
   
      |
173 | | simpr3 1015 |
. . . . . . . . . . . . . . . 16
    
       
   
        |
174 | 172, 173,
81 | syl2anc 666 |
. . . . . . . . . . . . . . 15
    
       
   
      |
175 | 174 | adantr 467 |
. . . . . . . . . . . . . 14
             
   
             |
176 | 162 | peano2nnd 10623 |
. . . . . . . . . . . . . . . . 17
    
       
        |
177 | | nnuz 11191 |
. . . . . . . . . . . . . . . . 17
     |
178 | 176, 177 | syl6eleq 2538 |
. . . . . . . . . . . . . . . 16
    
       
            |
179 | | fzss1 11834 |
. . . . . . . . . . . . . . . 16
      
            |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . 15
    
       
         
      |
181 | 180 | sselda 3431 |
. . . . . . . . . . . . . 14
             
   
             |
182 | 175, 181,
85 | syl2anc 666 |
. . . . . . . . . . . . 13
             
   
             |
183 | 182 | sqcld 12411 |
. . . . . . . . . . . 12
             
   
                 |
184 | 12 | oveq1d 6303 |
. . . . . . . . . . . . 13
                       |
185 | 14 | oveq1i 6298 |
. . . . . . . . . . . . . 14
               |
186 | 185, 136 | eqtri 2472 |
. . . . . . . . . . . . 13
           |
187 | 184, 186 | syl6eq 2500 |
. . . . . . . . . . . 12
             |
188 | 171, 183,
187 | fsum1p 13807 |
. . . . . . . . . . 11
    
       
                                          |
189 | 176 | peano2nnd 10623 |
. . . . . . . . . . . . . . . . . . . 20
    
       
          |
190 | 189, 177 | syl6eleq 2538 |
. . . . . . . . . . . . . . . . . . 19
    
       
              |
191 | | fzss1 11834 |
. . . . . . . . . . . . . . . . . . 19
        
              |
192 | 190, 191 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    
       
           
      |
193 | 192 | sselda 3431 |
. . . . . . . . . . . . . . . . 17
             
   
               |
194 | 145, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    
       
        |
195 | 194 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
             
   
             |
196 | | peano2re 9803 |
. . . . . . . . . . . . . . . . . . . 20
         |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
             
   
               |
198 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . 21
           |
199 | 198 | zred 11037 |
. . . . . . . . . . . . . . . . . . . 20
           |
200 | 199 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
             
   
           |
201 | 195 | ltp1d 10534 |
. . . . . . . . . . . . . . . . . . 19
             
   
                 |
202 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . . 20
               |
203 | 202 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
             
   
               |
204 | 195, 197,
200, 201, 203 | ltletrd 9792 |
. . . . . . . . . . . . . . . . . 18
             
   
             |
205 | 195, 204 | gtned 9767 |
. . . . . . . . . . . . . . . . 17
             
   
             |
206 | 193, 205,
126 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
             
   
               |
207 | 206 | sq0id 12365 |
. . . . . . . . . . . . . . 15
             
   
                   |
208 | 207 | sumeq2dv 13762 |
. . . . . . . . . . . . . 14
    
       
                                  |
209 | | fzfi 12182 |
. . . . . . . . . . . . . . . 16
         |
210 | 209 | olci 393 |
. . . . . . . . . . . . . . 15
                       |
211 | | sumz 13781 |
. . . . . . . . . . . . . . 15
         
                         |
212 | 210, 211 | ax-mp 5 |
. . . . . . . . . . . . . 14
           |
213 | 208, 212 | syl6eq 2500 |
. . . . . . . . . . . . 13
    
       
                        |
214 | 213 | oveq2d 6304 |
. . . . . . . . . . . 12
    
       
     
                      |
215 | | 1p0e1 10719 |
. . . . . . . . . . . 12
   |
216 | 214, 215 | syl6eq 2500 |
. . . . . . . . . . 11
    
       
     
                    |
217 | 188, 216 | eqtrd 2484 |
. . . . . . . . . 10
    
       
                      |
218 | 217 | ex 436 |
. . . . . . . . 9
            
                      |
219 | 143, 218 | pm2.61ine 2706 |
. . . . . . . 8
         
                     |
220 | 134, 219 | oveq12d 6306 |
. . . . . . 7
         
                                       |
221 | | 0p1e1 10718 |
. . . . . . 7
   |
222 | 220, 221 | syl6eq 2500 |
. . . . . 6
         
                                     |
223 | 89, 222 | eqtrd 2484 |
. . . . 5
         
                   |
224 | | simp1 1007 |
. . . . . . . 8
         
         |
225 | | 2lt3 10774 |
. . . . . . . . . 10
 |
226 | 153, 48, 225 | ltleii 9754 |
. . . . . . . . 9
 |
227 | | 2z 10966 |
. . . . . . . . . 10
 |
228 | 227 | eluz1i 11163 |
. . . . . . . . 9
         |
229 | 8, 226, 228 | mpbir2an 930 |
. . . . . . . 8
     |
230 | | uztrn 11172 |
. . . . . . . 8
          
      |
231 | 224, 229,
230 | sylancl 667 |
. . . . . . 7
         
         |
232 | | fveq2 5863 |
. . . . . . . 8
           |
233 | 232 | oveq1d 6303 |
. . . . . . 7
                   |
234 | 231, 88, 233 | fsum1p 13807 |
. . . . . 6
         
                                             |
235 | 59 | adantr 467 |
. . . . . . . . . . . . . . 15
         |
236 | 235 | zred 11037 |
. . . . . . . . . . . . . 14
         |
237 | | lttr 9707 |
. . . . . . . . . . . . . . . . . 18
 
  
    |
238 | 153, 48, 237 | mp3an12 1353 |
. . . . . . . . . . . . . . . . 17
  
    |
239 | 225, 238 | mpani 681 |
. . . . . . . . . . . . . . . 16
 
   |
240 | 49, 239 | syl 17 |
. . . . . . . . . . . . . . 15
    
    |
241 | 240 | imp 431 |
. . . . . . . . . . . . . 14
         |
242 | | ltle 9719 |
. . . . . . . . . . . . . . 15
 
 
   |
243 | 153, 242 | mpan 675 |
. . . . . . . . . . . . . 14
 
   |
244 | 236, 241,
243 | sylc 62 |
. . . . . . . . . . . . 13
         |
245 | 244, 155 | jctil 540 |
. . . . . . . . . . . 12
       
   |
246 | | 1z 10964 |
. . . . . . . . . . . . . 14
 |
247 | | elfz 11787 |
. . . . . . . . . . . . . 14
 
     
     |
248 | 227, 246,
247 | mp3an12 1353 |
. . . . . . . . . . . . 13
     
     |
249 | 235, 248 | syl 17 |
. . . . . . . . . . . 12
           
     |
250 | 245, 249 | mpbird 236 |
. . . . . . . . . . 11
             |
251 | 250 | 3adant3 1027 |
. . . . . . . . . 10
         
         |
252 | 94 | ltp1d 10534 |
. . . . . . . . . . . . . 14
           |
253 | 154, 94, 118, 157, 252 | lelttrd 9790 |
. . . . . . . . . . . . 13
           |
254 | 253 | 3ad2ant3 1030 |
. . . . . . . . . . . 12
         
       |
255 | | ltne 9727 |
. . . . . . . . . . . 12
         |
256 | 153, 254,
255 | sylancr 668 |
. . . . . . . . . . 11
         
       |
257 | 256 | necomd 2678 |
. . . . . . . . . 10
         
       |
258 | 13 | axlowdimlem12 24976 |
. . . . . . . . . 10
               |
259 | 251, 257,
258 | syl2anc 666 |
. . . . . . . . 9
         
         |
260 | 259 | sq0id 12365 |
. . . . . . . 8
         
             |
261 | 260 | oveq1d 6303 |
. . . . . . 7
         
                              
                  |
262 | 3 | oveq1i 6298 |
. . . . . . . . 9
           |
263 | 262 | sumeq1i 13757 |
. . . . . . . 8
              
                |
264 | 263 | oveq2i 6299 |
. . . . . . 7
                                   |
265 | 261, 264 | syl6eqr 2502 |
. . . . . 6
         
                              
                |
266 | | fzfid 12183 |
. . . . . . . 8
         
         |
267 | | 3nn 10765 |
. . . . . . . . . . . . . 14
 |
268 | 267, 177 | eleqtri 2526 |
. . . . . . . . . . . . 13
     |
269 | | fzss1 11834 |
. . . . . . . . . . . . 13
    
          |
270 | 268, 269 | ax-mp 5 |
. . . . . . . . . . . 12
         |
271 | 270 | sseli 3427 |
. . . . . . . . . . 11
           |
272 | 81, 271, 85 | syl2an 480 |
. . . . . . . . . 10
      
           
      |
273 | 272 | sqcld 12411 |
. . . . . . . . 9
      
           
          |
274 | 273 | 3adantl2 1164 |
. . . . . . . 8
          
                  |
275 | 266, 274 | fsumcl 13792 |
. . . . . . 7
         
                   |
276 | 275 | addid2d 9831 |
. . . . . 6
         
                                   |
277 | 234, 265,
276 | 3eqtrrd 2489 |
. . . . 5
         
                 
               |
278 | | simpl 459 |
. . . . . . . . 9
             |
279 | 21 | axlowdimlem7 24971 |
. . . . . . . . . . . 12
    
      |
280 | 279 | ad2antrr 731 |
. . . . . . . . . . 11
       
           |
281 | 271 | adantl 468 |
. . . . . . . . . . 11
       
           |
282 | | fveecn 24925 |
. . . . . . . . . . 11
     
           |
283 | 280, 281,
282 | syl2anc 666 |
. . . . . . . . . 10
       
           |
284 | 283 | sqcld 12411 |
. . . . . . . . 9
       
               |
285 | | neg1sqe1 12367 |
. . . . . . . . . 10
      |
286 | 24, 285 | syl6eq 2500 |
. . . . . . . . 9
           |
287 | 278, 284,
286 | fsum1p 13807 |
. . . . . . . 8
                                         |
288 | | 1re 9639 |
. . . . . . . . . . . . . . . . . 18
 |
289 | | zaddcl 10974 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
290 | 8, 246, 289 | mp2an 677 |
. . . . . . . . . . . . . . . . . . 19
   |
291 | 290 | zrei 10940 |
. . . . . . . . . . . . . . . . . 18
   |
292 | | 1lt3 10775 |
. . . . . . . . . . . . . . . . . . 19
 |
293 | 48 | ltp1i 10507 |
. . . . . . . . . . . . . . . . . . 19
   |
294 | 288, 48, 291 | lttri 9757 |
. . . . . . . . . . . . . . . . . . 19
         |
295 | 292, 293,
294 | mp2an 677 |
. . . . . . . . . . . . . . . . . 18
   |
296 | 288, 291,
295 | ltleii 9754 |
. . . . . . . . . . . . . . . . 17
   |
297 | | eluz 11169 |
. . . . . . . . . . . . . . . . . 18
                 |
298 | 246, 290,
297 | mp2an 677 |
. . . . . . . . . . . . . . . . 17
           |
299 | 296, 298 | mpbir 213 |
. . . . . . . . . . . . . . . 16
       |
300 | | fzss1 11834 |
. . . . . . . . . . . . . . . 16
      
            |
301 | 299, 300 | ax-mp 5 |
. . . . . . . . . . . . . . 15
           |
302 | 301 | sseli 3427 |
. . . . . . . . . . . . . 14
             |
303 | 302 | adantl 468 |
. . . . . . . . . . . . 13
       
             |
304 | 48, 291 | ltnlei 9752 |
. . . . . . . . . . . . . . . . . . 19
  
    |
305 | 293, 304 | mpbi 212 |
. . . . . . . . . . . . . . . . . 18
   |
306 | 305 | intnanr 925 |
. . . . . . . . . . . . . . . . 17
  
  |
307 | | elfz 11787 |
. . . . . . . . . . . . . . . . . . 19
   
          
    |
308 | 8, 290, 307 | mp3an12 1353 |
. . . . . . . . . . . . . . . . . 18
       
       |
309 | 235, 308 | syl 17 |
. . . . . . . . . . . . . . . . 17
             
       |
310 | 306, 309 | mtbiri 305 |
. . . . . . . . . . . . . . . 16
      
        |
311 | | eleq1 2516 |
. . . . . . . . . . . . . . . . 17
       
         |
312 | 311 | notbid 296 |
. . . . . . . . . . . . . . . 16
 
     
         |
313 | 310, 312 | syl5ibrcom 226 |
. . . . . . . . . . . . . . 15
       
         |
314 | 313 | necon2ad 2638 |
. . . . . . . . . . . . . 14
                 |
315 | 314 | imp 431 |
. . . . . . . . . . . . 13
       
         |
316 | 21 | axlowdimlem9 24973 |
. . . . . . . . . . . . 13
             |
317 | 303, 315,
316 | syl2anc 666 |
. . . . . . . . . . . 12
       
             |
318 | 317 | sq0id 12365 |
. . . . . . . . . . 11
       
                 |
319 | 318 | sumeq2dv 13762 |
. . . . . . . . . 10
                       
         |
320 | | fzfi 12182 |
. . . . . . . . . . . 12
       |
321 | 320 | olci 393 |
. . . . . . . . . . 11
                   |
322 | | sumz 13781 |
. . . . . . . . . . 11
       
                     |
323 | 321, 322 | ax-mp 5 |
. . . . . . . . . 10
         |
324 | 319, 323 | syl6eq 2500 |
. . . . . . . . 9
                         |
325 | 324 | oveq2d 6304 |
. . . . . . . 8
                             |
326 | 287, 325 | eqtrd 2484 |
. . . . . . 7
                         |
327 | 326, 215 | syl6eq 2500 |
. . . . . 6
                       |
328 | 327 | 3adant3 1027 |
. . . . 5
         
                   |
329 | 223, 277,
328 | 3eqtr4rd 2495 |
. . . 4
         
                 
               |
330 | 44, 54, 55, 329 | syl3anc 1267 |
. . 3
      
       
              
               |
331 | 330 | ex 436 |
. 2
      
                                      |
332 | 43, 331 | pm2.61ine 2706 |
1
         
                 
               |