Step | Hyp | Ref
| Expression |
1 | | uzssz 11178 |
. . . . . 6
     |
2 | | zssre 10944 |
. . . . . 6
 |
3 | 1, 2 | sstri 3441 |
. . . . 5
     |
4 | 3 | a1i 11 |
. . . 4
       |
5 | | ioodvbdlimc2lem.m |
. . . . . . 7
     
     |
6 | | ioodvbdlimc2lem.b |
. . . . . . . . . . 11
   |
7 | | ioodvbdlimc2lem.a |
. . . . . . . . . . 11
   |
8 | 6, 7 | resubcld 10047 |
. . . . . . . . . 10
     |
9 | | ioodvbdlimc2lem.altb |
. . . . . . . . . . . 12
   |
10 | 7, 6 | posdifd 10200 |
. . . . . . . . . . . 12
       |
11 | 9, 10 | mpbid 214 |
. . . . . . . . . . 11
     |
12 | 11 | gt0ne0d 10178 |
. . . . . . . . . 10
     |
13 | 8, 12 | rereccld 10434 |
. . . . . . . . 9
  
    |
14 | | 0red 9644 |
. . . . . . . . . 10
   |
15 | 8, 11 | recgt0d 10541 |
. . . . . . . . . 10
       |
16 | 14, 13, 15 | ltled 9783 |
. . . . . . . . 9

      |
17 | | flge0nn0 12054 |
. . . . . . . . 9
   
                 |
18 | 13, 16, 17 | syl2anc 667 |
. . . . . . . 8
           |
19 | | peano2nn0 10910 |
. . . . . . . 8
        
            |
20 | 18, 19 | syl 17 |
. . . . . . 7
      
      |
21 | 5, 20 | syl5eqel 2533 |
. . . . . 6
   |
22 | 21 | nn0zd 11038 |
. . . . 5
   |
23 | | eqid 2451 |
. . . . . 6
         |
24 | 23 | uzsup 12090 |
. . . . 5
           |
25 | 22, 24 | syl 17 |
. . . 4
           |
26 | | ioodvbdlimc2lem.f |
. . . . . . 7
           |
27 | 26 | adantr 467 |
. . . . . 6
 
    
          |
28 | 7 | rexrd 9690 |
. . . . . . . 8
   |
29 | 28 | adantr 467 |
. . . . . . 7
 
    
  |
30 | 6 | rexrd 9690 |
. . . . . . . 8
   |
31 | 30 | adantr 467 |
. . . . . . 7
 
    
  |
32 | 6 | adantr 467 |
. . . . . . . 8
 
    
  |
33 | | eluzelre 11169 |
. . . . . . . . . 10
    
  |
34 | 33 | adantl 468 |
. . . . . . . . 9
 
    
  |
35 | | 0red 9644 |
. . . . . . . . . . 11
 
    
  |
36 | | 0red 9644 |
. . . . . . . . . . . . 13
    
  |
37 | | 1red 9658 |
. . . . . . . . . . . . 13
    
  |
38 | 36, 37 | readdcld 9670 |
. . . . . . . . . . . 12
    
    |
39 | 38 | adantl 468 |
. . . . . . . . . . 11
 
    
    |
40 | 36 | ltp1d 10537 |
. . . . . . . . . . . 12
    
    |
41 | 40 | adantl 468 |
. . . . . . . . . . 11
 
    
    |
42 | | eluzel2 11164 |
. . . . . . . . . . . . . 14
    
  |
43 | 42 | zred 11040 |
. . . . . . . . . . . . 13
    
  |
44 | 43 | adantl 468 |
. . . . . . . . . . . 12
 
    
  |
45 | 13 | flcld 12034 |
. . . . . . . . . . . . . . . 16
           |
46 | 45 | zred 11040 |
. . . . . . . . . . . . . . 15
           |
47 | | 1red 9658 |
. . . . . . . . . . . . . . 15
   |
48 | 18 | nn0ge0d 10928 |
. . . . . . . . . . . . . . 15

    
     |
49 | 14, 46, 47, 48 | leadd1dd 10227 |
. . . . . . . . . . . . . 14
  
            |
50 | 49, 5 | syl6breqr 4443 |
. . . . . . . . . . . . 13
  
  |
51 | 50 | adantr 467 |
. . . . . . . . . . . 12
 
    
    |
52 | | eluzle 11171 |
. . . . . . . . . . . . 13
    
  |
53 | 52 | adantl 468 |
. . . . . . . . . . . 12
 
    
  |
54 | 39, 44, 34, 51, 53 | letrd 9792 |
. . . . . . . . . . 11
 
    
    |
55 | 35, 39, 34, 41, 54 | ltletrd 9795 |
. . . . . . . . . 10
 
    
  |
56 | 55 | gt0ne0d 10178 |
. . . . . . . . 9
 
    
  |
57 | 34, 56 | rereccld 10434 |
. . . . . . . 8
 
    
    |
58 | 32, 57 | resubcld 10047 |
. . . . . . 7
 
    
      |
59 | 7 | adantr 467 |
. . . . . . . 8
 
    
  |
60 | 21 | nn0red 10926 |
. . . . . . . . . . 11
   |
61 | 14, 47 | readdcld 9670 |
. . . . . . . . . . . . . 14
     |
62 | 46, 47 | readdcld 9670 |
. . . . . . . . . . . . . 14
      
      |
63 | 14 | ltp1d 10537 |
. . . . . . . . . . . . . 14
     |
64 | 14, 61, 62, 63, 49 | ltletrd 9795 |
. . . . . . . . . . . . 13
             |
65 | 64, 5 | syl6breqr 4443 |
. . . . . . . . . . . 12
   |
66 | 65 | gt0ne0d 10178 |
. . . . . . . . . . 11
   |
67 | 60, 66 | rereccld 10434 |
. . . . . . . . . 10
     |
68 | 67 | adantr 467 |
. . . . . . . . 9
 
    
    |
69 | 32, 68 | resubcld 10047 |
. . . . . . . 8
 
    
      |
70 | 5 | eqcomi 2460 |
. . . . . . . . . . . . 13
           |
71 | 70 | oveq2i 6301 |
. . . . . . . . . . . 12
               |
72 | 71, 67 | syl5eqel 2533 |
. . . . . . . . . . 11
               |
73 | 13, 15 | elrpd 11338 |
. . . . . . . . . . . . 13
  
    |
74 | 62, 64 | elrpd 11338 |
. . . . . . . . . . . . 13
      
      |
75 | | 1rp 11306 |
. . . . . . . . . . . . . 14
 |
76 | 75 | a1i 11 |
. . . . . . . . . . . . 13
   |
77 | | fllelt 12033 |
. . . . . . . . . . . . . . 15
             
     
 
             |
78 | 13, 77 | syl 17 |
. . . . . . . . . . . . . 14
      
                        |
79 | 78 | simprd 465 |
. . . . . . . . . . . . 13
  
 
            |
80 | 73, 74, 76, 79 | ltdiv2dd 37509 |
. . . . . . . . . . . 12
                     |
81 | 8 | recnd 9669 |
. . . . . . . . . . . . 13
     |
82 | 81, 12 | recrecd 10380 |
. . . . . . . . . . . 12
           |
83 | 80, 82 | breqtrd 4427 |
. . . . . . . . . . 11
                 |
84 | 72, 8, 6, 83 | ltsub2dd 10226 |
. . . . . . . . . 10
  
 
       
        |
85 | 6 | recnd 9669 |
. . . . . . . . . . 11
   |
86 | 7 | recnd 9669 |
. . . . . . . . . . 11
   |
87 | 85, 86 | nncand 9991 |
. . . . . . . . . 10
  
    |
88 | 71 | oveq2i 6301 |
. . . . . . . . . . 11
       
           |
89 | 88 | a1i 11 |
. . . . . . . . . 10
                     |
90 | 84, 87, 89 | 3brtr3d 4432 |
. . . . . . . . 9
       |
91 | 90 | adantr 467 |
. . . . . . . 8
 
    
      |
92 | 60, 65 | elrpd 11338 |
. . . . . . . . . . 11
   |
93 | 92 | adantr 467 |
. . . . . . . . . 10
 
    
  |
94 | 34, 55 | elrpd 11338 |
. . . . . . . . . 10
 
    
  |
95 | | 1red 9658 |
. . . . . . . . . 10
 
    
  |
96 | | 0le1 10137 |
. . . . . . . . . . 11
 |
97 | 96 | a1i 11 |
. . . . . . . . . 10
 
    
  |
98 | 93, 94, 95, 97, 53 | lediv2ad 11363 |
. . . . . . . . 9
 
    
      |
99 | 57, 68, 32, 98 | lesub2dd 10230 |
. . . . . . . 8
 
    
          |
100 | 59, 69, 58, 91, 99 | ltletrd 9795 |
. . . . . . 7
 
    
      |
101 | 94 | rpreccld 11351 |
. . . . . . . 8
 
    
    |
102 | 32, 101 | ltsubrpd 11370 |
. . . . . . 7
 
    
      |
103 | 29, 31, 58, 100, 102 | eliood 37595 |
. . . . . 6
 
    
          |
104 | 27, 103 | ffvelrnd 6023 |
. . . . 5
 
    
          |
105 | | ioodvbdlimc2lem.s |
. . . . 5
               |
106 | 104, 105 | fmptd 6046 |
. . . 4
           |
107 | | ioodvbdlimc2lem.dmdv |
. . . . . 6
         |
108 | | ioodvbdlimc2lem.dvbd |
. . . . . 6
                    |
109 | 7, 6, 9, 26, 107, 108 | dvbdfbdioo 37802 |
. . . . 5
                  |
110 | 60 | adantr 467 |
. . . . . . . 8
 
             
   |
111 | | simpr 463 |
. . . . . . . . . . . . . 14
 
    
      |
112 | 105 | fvmpt2 5957 |
. . . . . . . . . . . . . 14
                             |
113 | 111, 104,
112 | syl2anc 667 |
. . . . . . . . . . . . 13
 
    
              |
114 | 113 | fveq2d 5869 |
. . . . . . . . . . . 12
 
    
                      |
115 | 114 | adantlr 721 |
. . . . . . . . . . 11
   
             
    
                      |
116 | | simplr 762 |
. . . . . . . . . . . 12
   
             
    
             
  |
117 | 103 | adantlr 721 |
. . . . . . . . . . . 12
   
             
    
          |
118 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
            
      |
119 | 118 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                           |
120 | 119 | breq1d 4412 |
. . . . . . . . . . . . 13
             
      
        |
121 | 120 | rspccva 3149 |
. . . . . . . . . . . 12
               

                   
  |
122 | 116, 117,
121 | syl2anc 667 |
. . . . . . . . . . 11
   
             
    
      
       |
123 | 115, 122 | eqbrtrd 4423 |
. . . . . . . . . 10
   
             
    
          |
124 | 123 | a1d 26 |
. . . . . . . . 9
   
             
    

           |
125 | 124 | ralrimiva 2802 |
. . . . . . . 8
 
             
       
           |
126 | | breq1 4405 |
. . . . . . . . . . 11
 
   |
127 | 126 | imbi1d 319 |
. . . . . . . . . 10
          
 
            |
128 | 127 | ralbidv 2827 |
. . . . . . . . 9
  
     
        
              
    |
129 | 128 | rspcev 3150 |
. . . . . . . 8
                   
                  |
130 | 110, 125,
129 | syl2anc 667 |
. . . . . . 7
 
             
                    |
131 | 130 | ex 436 |
. . . . . 6
               
 
                  |
132 | 131 | reximdv 2861 |
. . . . 5
                
 
              
    |
133 | 109, 132 | mpd 15 |
. . . 4
   
                 |
134 | 4, 25, 106, 133 | limsupre 37721 |
. . 3
       |
135 | 134 | recnd 9669 |
. 2
       |
136 | | eluzelre 11169 |
. . . . . . . . 9
    
  |
137 | 136 | adantl 468 |
. . . . . . . 8
        
  |
138 | | 0red 9644 |
. . . . . . . . . 10
        
  |
139 | 45 | peano2zd 11043 |
. . . . . . . . . . . . . 14
      
      |
140 | 5, 139 | syl5eqel 2533 |
. . . . . . . . . . . . 13
   |
141 | 140 | adantr 467 |
. . . . . . . . . . . 12
 

  |
142 | 141 | zred 11040 |
. . . . . . . . . . 11
 

  |
143 | 142 | adantr 467 |
. . . . . . . . . 10
        
  |
144 | 65 | ad2antrr 732 |
. . . . . . . . . 10
        
  |
145 | | ioodvbdlimc2lem.n |
. . . . . . . . . . . . . 14
      
                   |
146 | | ioodvbdlimc2lem.y |
. . . . . . . . . . . . . . . . . . . 20
                     |
147 | | ioomidp 37615 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
           |
148 | 7, 6, 9, 147 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
149 | | ne0i 3737 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
151 | | ioossre 11696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
152 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
  |
153 | | dvfre 22905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   
     |
154 | 26, 152, 153 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
155 | 107 | feq2d 5715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
  
             |
156 | 154, 155 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
157 | 156 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
        |
158 | 157 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
        |
159 | 158 | abscld 13498 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
            |
160 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 |
161 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . 22
                                         |
162 | 150, 159,
108, 160, 161 | suprnmpt 37439 |
. . . . . . . . . . . . . . . . . . . . 21
                                     
                       |
163 | 162 | simpld 461 |
. . . . . . . . . . . . . . . . . . . 20
                       |
164 | 146, 163 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . . 19
   |
165 | 164 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 

  |
166 | | rpre 11308 |
. . . . . . . . . . . . . . . . . . . 20

  |
167 | 166 | rehalfcld 10859 |
. . . . . . . . . . . . . . . . . . 19

    |
168 | 167 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 

    |
169 | 166 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . 20

  |
170 | 169 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 

  |
171 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . 19
 

  |
172 | | rpne0 11317 |
. . . . . . . . . . . . . . . . . . . 20

  |
173 | 172 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 

  |
174 | | 2ne0 10702 |
. . . . . . . . . . . . . . . . . . . 20
 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 

  |
176 | 170, 171,
173, 175 | divne0d 10399 |
. . . . . . . . . . . . . . . . . 18
 

    |
177 | 165, 168,
176 | redivcld 10435 |
. . . . . . . . . . . . . . . . 17
 

      |
178 | 177 | flcld 12034 |
. . . . . . . . . . . . . . . 16
 

          |
179 | 178 | peano2zd 11043 |
. . . . . . . . . . . . . . 15
 

            |
180 | 179, 141 | ifcld 3924 |
. . . . . . . . . . . . . 14
 

                           |
181 | 145, 180 | syl5eqel 2533 |
. . . . . . . . . . . . 13
 

  |
182 | 181 | zred 11040 |
. . . . . . . . . . . 12
 

  |
183 | 182 | adantr 467 |
. . . . . . . . . . 11
        
  |
184 | 179 | zred 11040 |
. . . . . . . . . . . . . 14
 

            |
185 | | max1 11480 |
. . . . . . . . . . . . . 14
      
       
               
         |
186 | 142, 184,
185 | syl2anc 667 |
. . . . . . . . . . . . 13
 

                 
         |
187 | 186, 145 | syl6breqr 4443 |
. . . . . . . . . . . 12
 

  |
188 | 187 | adantr 467 |
. . . . . . . . . . 11
        
  |
189 | | eluzle 11171 |
. . . . . . . . . . . 12
    
  |
190 | 189 | adantl 468 |
. . . . . . . . . . 11
        
  |
191 | 143, 183,
137, 188, 190 | letrd 9792 |
. . . . . . . . . 10
        
  |
192 | 138, 143,
137, 144, 191 | ltletrd 9795 |
. . . . . . . . 9
        
  |
193 | 192 | gt0ne0d 10178 |
. . . . . . . 8
        
  |
194 | 137, 193 | rereccld 10434 |
. . . . . . 7
        
    |
195 | 137, 192 | recgt0d 10541 |
. . . . . . 7
        
    |
196 | 194, 195 | elrpd 11338 |
. . . . . 6
        
    |
197 | 196 | adantr 467 |
. . . . 5
   

                          |
198 | | ioodvbdlimc2lem.ch |
. . . . . . . . 9
     
     
                                 |
199 | 198 | biimpi 198 |
. . . . . . . . . . . . . . . . 17
           
                                 |
200 | | simp-5l 778 |
. . . . . . . . . . . . . . . . 17
     
     
                              
  |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
202 | 201, 26 | syl 17 |
. . . . . . . . . . . . . . 15
           |
203 | 199 | simplrd 763 |
. . . . . . . . . . . . . . 15

      |
204 | 202, 203 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
       |
205 | 204 | recnd 9669 |
. . . . . . . . . . . . 13
       |
206 | 201, 106 | syl 17 |
. . . . . . . . . . . . . . 15
           |
207 | | simp-5r 779 |
. . . . . . . . . . . . . . . . . . 19
     
     
                              
  |
208 | 199, 207 | syl 17 |
. . . . . . . . . . . . . . . . . 18

  |
209 | | eluz2 11165 |
. . . . . . . . . . . . . . . . . . 19
         |
210 | 141, 181,
187, 209 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . . . 18
 

      |
211 | 201, 208,
210 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17

      |
212 | | uzss 11179 |
. . . . . . . . . . . . . . . . 17
    
          |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . . . 16
           |
214 | | simp-4r 777 |
. . . . . . . . . . . . . . . . 17
     
     
                              
      |
215 | 199, 214 | syl 17 |
. . . . . . . . . . . . . . . 16

      |
216 | 213, 215 | sseldd 3433 |
. . . . . . . . . . . . . . 15

      |
217 | 206, 216 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
       |
218 | 217 | recnd 9669 |
. . . . . . . . . . . . 13
       |
219 | 201, 135 | syl 17 |
. . . . . . . . . . . . 13
       |
220 | 205, 218,
219 | npncand 10010 |
. . . . . . . . . . . 12
                                   |
221 | 220 | eqcomd 2457 |
. . . . . . . . . . 11
                                   |
222 | 221 | fveq2d 5869 |
. . . . . . . . . 10
                                           |
223 | 204, 217 | resubcld 10047 |
. . . . . . . . . . . . . 14
             |
224 | 201, 134 | syl 17 |
. . . . . . . . . . . . . . 15
       |
225 | 217, 224 | resubcld 10047 |
. . . . . . . . . . . . . 14
             |
226 | 223, 225 | readdcld 9670 |
. . . . . . . . . . . . 13
                         |
227 | 226 | recnd 9669 |
. . . . . . . . . . . 12
                         |
228 | 227 | abscld 13498 |
. . . . . . . . . . 11
                             |
229 | 223 | recnd 9669 |
. . . . . . . . . . . . 13
             |
230 | 229 | abscld 13498 |
. . . . . . . . . . . 12
                 |
231 | 225 | recnd 9669 |
. . . . . . . . . . . . 13
             |
232 | 231 | abscld 13498 |
. . . . . . . . . . . 12
                 |
233 | 230, 232 | readdcld 9670 |
. . . . . . . . . . 11
                                 |
234 | 208 | rpred 11341 |
. . . . . . . . . . 11

  |
235 | 229, 231 | abstrid 13518 |
. . . . . . . . . . 11
                                                           |
236 | 234 | rehalfcld 10859 |
. . . . . . . . . . . . 13
     |
237 | 201, 216,
113 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
               |
238 | 237 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
                   
       |
239 | 238 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                                   |
240 | 239, 230 | eqeltrrd 2530 |
. . . . . . . . . . . . . . 15
                     |
241 | 201, 164 | syl 17 |
. . . . . . . . . . . . . . . 16

  |
242 | 151, 203 | sseldi 3430 |
. . . . . . . . . . . . . . . . 17

  |
243 | 201, 216,
58 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
       |
244 | 242, 243 | resubcld 10047 |
. . . . . . . . . . . . . . . 16
  
      |
245 | 241, 244 | remulcld 9671 |
. . . . . . . . . . . . . . 15
           |
246 | 201, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17

  |
247 | 201, 6 | syl 17 |
. . . . . . . . . . . . . . . . 17

  |
248 | 201, 107 | syl 17 |
. . . . . . . . . . . . . . . . 17
         |
249 | 162 | simprd 465 |
. . . . . . . . . . . . . . . . . . . 20
                
                      |
250 | 146 | breq2i 4410 |
. . . . . . . . . . . . . . . . . . . . 21
          
                                |
251 | 250 | ralbii 2819 |
. . . . . . . . . . . . . . . . . . . 20
 
                                                     |
252 | 249, 251 | sylibr 216 |
. . . . . . . . . . . . . . . . . . 19
                
  |
253 | 201, 252 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                
  |
254 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . 21
               |
255 | 254 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . 20
                       |
256 | 255 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . 19
           
             |
257 | 256 | cbvralv 3019 |
. . . . . . . . . . . . . . . . . 18
 
                                 |
258 | 253, 257 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
                
  |
259 | 201, 216,
103 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
           |
260 | 243 | rexrd 9690 |
. . . . . . . . . . . . . . . . . 18
       |
261 | 201, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18

  |
262 | 3, 216 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . 20

  |
263 | 201, 216,
56 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20

  |
264 | 262, 263 | rereccld 10434 |
. . . . . . . . . . . . . . . . . . 19
     |
265 | 247, 242 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . 20
     |
266 | 242, 247 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
267 | 266 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . 21
     |
268 | 267 | abscld 13498 |
. . . . . . . . . . . . . . . . . . . 20
         |
269 | 265 | leabsd 13476 |
. . . . . . . . . . . . . . . . . . . . 21
  
        |
270 | 201, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
271 | 242 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
272 | 270, 271 | abssubd 13515 |
. . . . . . . . . . . . . . . . . . . . 21
    
          |
273 | 269, 272 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . 20
  
        |
274 | 199 | simprd 465 |
. . . . . . . . . . . . . . . . . . . 20
           |
275 | 265, 268,
264, 273, 274 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . . 19
  
    |
276 | 247, 242,
264, 275 | ltsub23d 10218 |
. . . . . . . . . . . . . . . . . 18
       |
277 | 201, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . 19

  |
278 | | iooltub 37610 |
. . . . . . . . . . . . . . . . . . 19
         |
279 | 277, 261,
203, 278 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . 18

  |
280 | 260, 261,
242, 276, 279 | eliood 37595 |
. . . . . . . . . . . . . . . . 17

          |
281 | 246, 247,
202, 248, 241, 258, 259, 280 | dvbdfbdioolem1 37800 |
. . . . . . . . . . . . . . . 16
                   
  
                       
      |
282 | 281 | simpld 461 |
. . . . . . . . . . . . . . 15
                  
  
       |
283 | 201, 216,
57 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
     |
284 | 241, 283 | remulcld 9671 |
. . . . . . . . . . . . . . . 16
       |
285 | 156, 148 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . 21
             |
286 | 285 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . 20
             |
287 | 286 | abscld 13498 |
. . . . . . . . . . . . . . . . . . 19
          
      |
288 | 286 | absge0d 13506 |
. . . . . . . . . . . . . . . . . . 19

                |
289 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
290 | 289 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                        
      |
291 | 146 | eqcomi 2460 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     |
292 | 291 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
293 | 290, 292 | breq12d 4415 |
. . . . . . . . . . . . . . . . . . . . 21
               
                   
                 |
294 | 293 | rspcva 3148 |
. . . . . . . . . . . . . . . . . . . 20
                                                               |
295 | 148, 249,
294 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
          
   
  |
296 | 14, 287, 164, 288, 295 | letrd 9792 |
. . . . . . . . . . . . . . . . . 18

  |
297 | 201, 296 | syl 17 |
. . . . . . . . . . . . . . . . 17

  |
298 | 283 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . 20
     |
299 | | sub31 37504 |
. . . . . . . . . . . . . . . . . . . 20
 
    
            |
300 | 271, 270,
298, 299 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . 19
  
            |
301 | 242, 247 | posdifd 10200 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
302 | 279, 301 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . 21

    |
303 | 265, 302 | elrpd 11338 |
. . . . . . . . . . . . . . . . . . . 20
     |
304 | 283, 303 | ltsubrpd 11370 |
. . . . . . . . . . . . . . . . . . 19
    
 
    |
305 | 300, 304 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . 18
  
        |
306 | 244, 283,
305 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
  
   
    |
307 | 244, 283,
241, 297, 306 | lemul2ad 10547 |
. . . . . . . . . . . . . . . 16
        
      |
308 | 284 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
     |
309 | 236 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
       |
310 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
311 | 298 | mul02d 9831 |
. . . . . . . . . . . . . . . . . . . 20
       |
312 | 310, 311 | sylan9eqr 2507 |
. . . . . . . . . . . . . . . . . . 19
   
     |
313 | 208 | rphalfcld 11353 |
. . . . . . . . . . . . . . . . . . . . 21
     |
314 | 313 | rpgt0d 11344 |
. . . . . . . . . . . . . . . . . . . 20

    |
315 | 314 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
       |
316 | 312, 315 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . 18
   
       |
317 | 308, 309,
316 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
   
       |
318 | 241 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
  
  |
319 | 297 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
  
  |
320 | | neqne 37374 |
. . . . . . . . . . . . . . . . . . . 20
   |
321 | 320 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
     |
322 | 318, 319,
321 | ne0gt0d 9772 |
. . . . . . . . . . . . . . . . . 18
  
  |
323 | 284 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
     |
324 | 3, 211 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
325 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
326 | 201, 208,
142 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
327 | 201, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
328 | 201, 208,
187 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
329 | 325, 326,
324, 327, 328 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
330 | 329 | gt0ne0d 10178 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
331 | 324, 330 | rereccld 10434 |
. . . . . . . . . . . . . . . . . . . . 21
     |
332 | 241, 331 | remulcld 9671 |
. . . . . . . . . . . . . . . . . . . 20
       |
333 | 332 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
     |
334 | 236 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
       |
335 | 283 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
       |
336 | 331 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
       |
337 | 241 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     |
338 | 297 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     |
339 | 324, 329 | elrpd 11338 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
340 | 201, 216,
94 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
341 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
342 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
343 | 215, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
344 | 339, 340,
341, 342, 343 | lediv2ad 11363 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
345 | 344 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
         |
346 | 335, 336,
337, 338, 345 | lemul2ad 10547 |
. . . . . . . . . . . . . . . . . . 19
   
         |
347 | 234 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
348 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
349 | 208 | rpne0d 11346 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
350 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
351 | 347, 348,
349, 350 | divne0d 10399 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
352 | 241, 236,
351 | redivcld 10435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
353 | 352 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
354 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
355 | 314 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
356 | 337, 334,
354, 355 | divgt0d 10542 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
357 | 353, 356 | elrpd 11338 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
358 | 357 | rprecred 11352 |
. . . . . . . . . . . . . . . . . . . . 21
           |
359 | 339 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
360 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
361 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
362 | 352 | flcld 12034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
363 | 362 | peano2zd 11043 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
       |
364 | 363 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
365 | 201, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
366 | 363, 365 | ifcld 3924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
                    |
367 | 145, 366 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
368 | 367 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
369 | | flltp1 12036 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
       |
370 | 352, 369 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
371 | 201, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
372 | | max2 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
                 
               
         |
373 | 371, 364,
372 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
    
                           |
374 | 373, 145 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
    
  |
375 | 352, 364,
368, 370, 374 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
376 | 352, 324,
375 | ltled 9783 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
  |
377 | 376 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
378 | 357, 359,
360, 361, 377 | lediv2ad 11363 |
. . . . . . . . . . . . . . . . . . . . 21
             |
379 | 336, 358,
337, 338, 378 | lemul2ad 10547 |
. . . . . . . . . . . . . . . . . . . 20
   
             |
380 | 337 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
381 | 353 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
382 | 356 | gt0ne0d 10178 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
383 | 380, 381,
382 | divrecd 10386 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
384 | 334 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
385 | 354 | gt0ne0d 10178 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
386 | 351 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
387 | 380, 384,
385, 386 | ddcand 10403 |
. . . . . . . . . . . . . . . . . . . . 21
             |
388 | 383, 387 | eqtr3d 2487 |
. . . . . . . . . . . . . . . . . . . 20
   
           |
389 | 379, 388 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . 19
   
       |
390 | 323, 333,
334, 346, 389 | letrd 9792 |
. . . . . . . . . . . . . . . . . 18
   
       |
391 | 322, 390 | syldan 473 |
. . . . . . . . . . . . . . . . 17
      
    |
392 | 317, 391 | pm2.61dan 800 |
. . . . . . . . . . . . . . . 16
    
    |
393 | 245, 284,
236, 307, 392 | letrd 9792 |
. . . . . . . . . . . . . . 15
        
    |
394 | 240, 245,
236, 282, 393 | letrd 9792 |
. . . . . . . . . . . . . 14
                  
    |
395 | 239, 394 | eqbrtrd 4423 |
. . . . . . . . . . . . 13
              
    |
396 | | simpllr 769 |
. . . . . . . . . . . . . 14
     
     
                              
                  |
397 | 199, 396 | syl 17 |
. . . . . . . . . . . . 13
                   |
398 | 230, 232,
236, 236, 395, 397 | leltaddd 10235 |
. . . . . . . . . . . 12
                                       |
399 | 347 | 2halvesd 10858 |
. . . . . . . . . . . 12
         |
400 | 398, 399 | breqtrd 4427 |
. . . . . . . . . . 11
                                 |
401 | 228, 233,
234, 235, 400 | lelttrd 9793 |
. . . . . . . . . 10
                             |
402 | 222, 401 | eqbrtrd 4423 |
. . . . . . . . 9
                 |
403 | 198, 402 | sylbir 217 |
. . . . . . . 8
     
     
                              
                |
404 | 403 | adantrl 722 |
. . . . . . 7
     
     
                                                 |
405 | 404 | ex 436 |
. . . . . 6
     
                     
      
        
                 |
406 | 405 | ralrimiva 2802 |
. . . . 5
   

                                                        |
407 | | breq2 4406 |
. . . . . . . . 9
         
           |
408 | 407 | anbi2d 710 |
. . . . . . . 8
                         |
409 | 408 | imbi1d 319 |
. . . . . . 7
     
      
                
        
                  |
410 | 409 | ralbidv 2827 |
. . . . . 6
    
                            
                                   |
411 | 410 | rspcev 3150 |
. . . . 5
    
                                                                 |
412 | 197, 406,
411 | syl2anc 667 |
. . . 4
   

                                                       |
413 | | simpr 463 |
. . . . . . . . . . 11
       |
414 | 413 | iftrued 3889 |
. . . . . . . . . 10
            |
415 | | uzid 11173 |
. . . . . . . . . . . 12
       |
416 | 181, 415 | syl 17 |
. . . . . . . . . . 11
 

      |
417 | 416 | adantr 467 |
. . . . . . . . . 10
           |
418 | 414, 417 | eqeltrd 2529 |
. . . . . . . . 9
                |
419 | 418 | adantlr 721 |
. . . . . . . 8
   


            |
420 | | iffalse 3890 |
. . . . . . . . . 10

       |
421 | 420 | adantl 468 |
. . . . . . . . 9
   

 
 
 
   |
422 | 181 | ad2antrr 732 |
. . . . . . . . . 10
   

 
  |
423 | | simplr 762 |
. . . . . . . . . 10
   

 
  |
424 | 422 | zred 11040 |
. . . . . . . . . . 11
   

 
  |
425 | 423 | zred 11040 |
. . . . . . . . . . 11
   

 
  |
426 | | simpr 463 |
. . . . . . . . . . . 12
   

 
  |
427 | 424, 425 | ltnled 9782 |
. . . . . . . . . . . 12
   

 

   |
428 | 426, 427 | mpbird 236 |
. . . . . . . . . . 11
   

 
  |
429 | 424, 425,
428 | ltled 9783 |
. . . . . . . . . 10
   

 
  |
430 | | eluz2 11165 |
. . . . . . . . . 10
         |
431 | 422, 423,
429, 430 | syl3anbrc 1192 |
. . . . . . . . 9
   

 
      |
432 | 421, 431 | eqeltrd 2529 |
. . . . . . . 8
   

 
 
 
       |
433 | 419, 432 | pm2.61dan 800 |
. . . . . . 7
                |
434 | 433 | adantr 467 |
. . . . . 6
   

                                         |
435 | | simpr 463 |
. . . . . . . 8
   

                              
                             |
436 | | simpr 463 |
. . . . . . . . . 10
       |
437 | 181 | adantr 467 |
. . . . . . . . . . 11
       |
438 | 437, 436 | ifcld 3924 |
. . . . . . . . . 10
            |
439 | 436 | zred 11040 |
. . . . . . . . . . 11
       |
440 | 437 | zred 11040 |
. . . . . . . . . . 11
       |
441 | | max1 11480 |
. . . . . . . . . . 11
 

 
 
   |
442 | 439, 440,
441 | syl2anc 667 |
. . . . . . . . . 10
       
    |
443 | | eluz2 11165 |
. . . . . . . . . 10
            
 
         |
444 | 436, 438,
442, 443 | syl3anbrc 1192 |
. . . . . . . . 9
                |
445 | 444 | adantr 467 |
. . . . . . . 8
   

                                         |
446 | | fveq2 5865 |
. . . . . . . . . . 11
                     |
447 | 446 | eleq1d 2513 |
. . . . . . . . . 10
               
 
     |
448 | 446 | oveq1d 6305 |
. . . . . . . . . . . 12
                                 |
449 | 448 | fveq2d 5869 |
. . . . . . . . . . 11
                                         |
450 | 449 | breq1d 4412 |
. . . . . . . . . 10
                      
                        |
451 | 447, 450 | anbi12d 717 |
. . . . . . . . 9
                                               
 
              |
452 | 451 | rspccva 3149 |
. . . . . . . 8
                                                          
 
             |
453 | 435, 445,
452 | syl2anc 667 |
. . . . . . 7
   

                                                
 
             |
454 | 453 | simprd 465 |
. . . . . 6
   

                                                     |
455 | | fveq2 5865 |
. . . . . . . . . 10
                     |
456 | 455 | oveq1d 6305 |
. . . . . . . . 9
                                 |
457 | 456 | fveq2d 5869 |
. . . . . . . 8
                                         |
458 | 457 | breq1d 4412 |
. . . . . . 7
                      
                        |
459 | 458 | rspcev 3150 |
. . . . . 6
    
              
 
           
                       |
460 | 434, 454,
459 | syl2anc 667 |
. . . . 5
   

                              
                       |
461 | | ax-resscn 9596 |
. . . . . . . . . . . . . 14
 |
462 | 461 | a1i 11 |
. . . . . . . . . . . . 13

  |
463 | 26, 462 | fssd 5738 |
. . . . . . . . . . . . . 14
           |
464 | | dvcn 22875 |
. . . . . . . . . . . . . 14
                                 |
465 | 462, 463,
152, 107, 464 | syl31anc 1271 |
. . . . . . . . . . . . 13
           |
466 | | cncffvrn 21930 |
. . . . . . . . . . . . 13
 
        
                    |
467 | 462, 465,
466 | syl2anc 667 |
. . . . . . . . . . . 12
         
           |
468 | 26, 467 | mpbird 236 |
. . . . . . . . . . 11
           |
469 | | ioodvbdlimc2lem.r |
. . . . . . . . . . . 12
           |
470 | 103, 469 | fmptd 6046 |
. . . . . . . . . . 11
               |
471 | | eqid 2451 |
. . . . . . . . . . 11
                             |
472 | | climrel 13556 |
. . . . . . . . . . . . 13
 |
473 | 472 | a1i 11 |
. . . . . . . . . . . 12
  |
474 | | fvex 5875 |
. . . . . . . . . . . . . . . . 17
     |
475 | 474 | mptex 6136 |
. . . . . . . . . . . . . . . 16
       |
476 | 475 | a1i 11 |
. . . . . . . . . . . . . . 15
         |
477 | | eqidd 2452 |
. . . . . . . . . . . . . . . 16
 
    
              |
478 | | eqidd 2452 |
. . . . . . . . . . . . . . . 16
       
   |
479 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
    
      |
480 | 6 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
  |
481 | 477, 478,
479, 480 | fvmptd 5954 |
. . . . . . . . . . . . . . 15
 
    
            |
482 | 23, 22, 476, 85, 481 | climconst 13607 |
. . . . . . . . . . . . . 14
         |
483 | 474 | mptex 6136 |
. . . . . . . . . . . . . . . 16
           |
484 | 469, 483 | eqeltri 2525 |
. . . . . . . . . . . . . . 15
 |
485 | 484 | a1i 11 |
. . . . . . . . . . . . . 14
   |
486 | | 1cnd 9659 |
. . . . . . . . . . . . . . 15
   |
487 | | elnnnn0b 10914 |
. . . . . . . . . . . . . . . 16

    |
488 | 21, 65, 487 | sylanbrc 670 |
. . . . . . . . . . . . . . 15
   |
489 | | divcnvg 37707 |
. . . . . . . . . . . . . . 15
 
           |
490 | 486, 488,
489 | syl2anc 667 |
. . . . . . . . . . . . . 14
           |
491 | | eqidd 2452 |
. . . . . . . . . . . . . . . . 17
 
    
              |
492 | | eqidd 2452 |
. . . . . . . . . . . . . . . . 17
       
   |
493 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
    
      |
494 | 6 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
  |
495 | 491, 492,
493, 494 | fvmptd 5954 |
. . . . . . . . . . . . . . . 16
 
    
            |
496 | 495, 494 | eqeltrd 2529 |
. . . . . . . . . . . . . . 15
 
    
            |
497 | 496 | recnd 9669 |
. . . . . . . . . . . . . 14
 
    
            |
498 | | eqidd 2452 |
. . . . . . . . . . . . . . . 16
 
    
                  |
499 | | oveq2 6298 |
. . . . . . . . . . . . . . . . 17
       |
500 | 499 | adantl 468 |
. . . . . . . . . . . . . . . 16
       
       |
501 | 3, 493 | sseldi 3430 |
. . . . . . . . . . . . . . . . 17
 
    
  |
502 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
503 | 60 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
504 | 65 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
505 | | eluzle 11171 |
. . . . . . . . . . . . . . . . . . . 20
    
  |
506 | 505 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
507 | 502, 503,
501, 504, 506 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
508 | 507 | gt0ne0d 10178 |
. . . . . . . . . . . . . . . . 17
 
    
  |
509 | 501, 508 | rereccld 10434 |
. . . . . . . . . . . . . . . 16
 
    
    |
510 | 498, 500,
493, 509 | fvmptd 5954 |
. . . . . . . . . . . . . . 15
 
    
                |
511 | 501 | recnd 9669 |
. . . . . . . . . . . . . . . 16
 
    
  |
512 | 511, 508 | reccld 10376 |
. . . . . . . . . . . . . . 15
 
    
    |
513 | 510, 512 | eqeltrd 2529 |
. . . . . . . . . . . . . 14
 
    
              |
514 | 499 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
 
         |
515 | | ovex 6318 |
. . . . . . . . . . . . . . . . 17
     |
516 | 514, 469,
515 | fvmpt 5948 |
. . . . . . . . . . . . . . . 16
    
          |
517 | 516 | adantl 468 |
. . . . . . . . . . . . . . 15
 
    
          |
518 | 495, 510 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
 
    
                              |
519 | 517, 518 | eqtr4d 2488 |
. . . . . . . . . . . . . 14
 
    
                              |
520 | 23, 22, 482, 485, 490, 497, 513, 519 | climsub 13697 |
. . . . . . . . . . . . 13
     |
521 | 85 | subid1d 9975 |
. . . . . . . . . . . . 13
     |
522 | 520, 521 | |