Step | Hyp | Ref
| Expression |
1 | | lhop1.c |
. 2
                      lim    |
2 | | simpr 467 |
. . . . . . . 8
 

  |
3 | 2 | rphalfcld 11382 |
. . . . . . 7
 

    |
4 | | breq2 4420 |
. . . . . . . . . 10
                                                                     |
5 | 4 | imbi2d 322 |
. . . . . . . . 9
     
      
                              
                                             |
6 | 5 | rexralbidv 2921 |
. . . . . . . 8
    
                                             
                                                    |
7 | 6 | rspcv 3158 |
. . . . . . 7
  
 
                                               
                                                   |
8 | 3, 7 | syl 17 |
. . . . . 6
 

 
                                               
                                                   |
9 | | rabid 2979 |
. . . . . . . . . . . . . 14
                           |
10 | | eliooord 11723 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
11 | 10 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
   


     
   |
12 | 11 | simprd 469 |
. . . . . . . . . . . . . . . . . . . 20
   


    
  |
13 | 12 | biantrurd 515 |
. . . . . . . . . . . . . . . . . . 19
   


        
      |
14 | | ioossre 11725 |
. . . . . . . . . . . . . . . . . . . . 21
     |
15 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . 21
   


           |
16 | 14, 15 | sseldi 3442 |
. . . . . . . . . . . . . . . . . . . 20
   


       |
17 | | lhop1.a |
. . . . . . . . . . . . . . . . . . . . 21
   |
18 | 17 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . 20
   


    
  |
19 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
20 | 19 | rpred 11370 |
. . . . . . . . . . . . . . . . . . . . 21
       |
21 | 20 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
   


       |
22 | 16, 18, 21 | ltsubaddd 10237 |
. . . . . . . . . . . . . . . . . . 19
   


             |
23 | 16 | rexrd 9716 |
. . . . . . . . . . . . . . . . . . . 20
   


       |
24 | | lhop1.b |
. . . . . . . . . . . . . . . . . . . . 21
   |
25 | 24 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . 20
   


    
  |
26 | 17 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
27 | 20, 26 | readdcld 9696 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
28 | 27 | rexrd 9716 |
. . . . . . . . . . . . . . . . . . . . 21
         |
29 | 28 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
   


         |
30 | | xrltmin 11506 |
. . . . . . . . . . . . . . . . . . . 20
     
        
       |
31 | 23, 25, 29, 30 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . 19
   


       
       
      |
32 | 13, 22, 31 | 3bitr4rd 294 |
. . . . . . . . . . . . . . . . . 18
   


       
        
   |
33 | 18 | rexrd 9716 |
. . . . . . . . . . . . . . . . . . 19
   


    
  |
34 | 25, 29 | ifcld 3936 |
. . . . . . . . . . . . . . . . . . 19
   


                |
35 | 11 | simpld 465 |
. . . . . . . . . . . . . . . . . . 19
   


       |
36 | | elioo5 11721 |
. . . . . . . . . . . . . . . . . . . 20
   
      
               
 
           |
37 | 36 | baibd 925 |
. . . . . . . . . . . . . . . . . . 19
            
      
         
          |
38 | 33, 34, 23, 35, 37 | syl31anc 1279 |
. . . . . . . . . . . . . . . . . 18
   


          
       
            |
39 | 18, 16, 35 | ltled 9809 |
. . . . . . . . . . . . . . . . . . . 20
   


       |
40 | 18, 16, 39 | abssubge0d 13542 |
. . . . . . . . . . . . . . . . . . 19
   


               |
41 | 40 | breq1d 4426 |
. . . . . . . . . . . . . . . . . 18
   


           
     |
42 | 32, 38, 41 | 3bitr4d 293 |
. . . . . . . . . . . . . . . . 17
   


          
                 |
43 | 42 | rabbi2dva 3652 |
. . . . . . . . . . . . . . . 16
         
                            |
44 | 24 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
       |
45 | | xrmin1 11501 |
. . . . . . . . . . . . . . . . . . 19
      
         |
46 | 44, 28, 45 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
      
         |
47 | | iooss2 11701 |
. . . . . . . . . . . . . . . . . 18
   
            
       
      |
48 | 44, 46, 47 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
                        |
49 | | dfss1 3649 |
. . . . . . . . . . . . . . . . 17
     
           
         
             
          |
50 | 48, 49 | sylib 201 |
. . . . . . . . . . . . . . . 16
         
                             |
51 | 43, 50 | eqtr3d 2498 |
. . . . . . . . . . . . . . 15
                     
          |
52 | 51 | eleq2d 2525 |
. . . . . . . . . . . . . 14
                 
    
           |
53 | 9, 52 | syl5bbr 267 |
. . . . . . . . . . . . 13
                                  |
54 | | lbioo 11696 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
55 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
56 | 54, 55 | mtbiri 309 |
. . . . . . . . . . . . . . . . . . . . 21

      |
57 | 56 | necon2ai 2665 |
. . . . . . . . . . . . . . . . . . . 20
       |
58 | 57 | biantrurd 515 |
. . . . . . . . . . . . . . . . . . 19
           
           |
59 | 58 | bicomd 206 |
. . . . . . . . . . . . . . . . . 18
                       |
60 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
61 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
62 | 60, 61 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
63 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . . . 22
                                         |
64 | | ovex 6343 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
65 | 62, 63, 64 | fvmpt3i 5976 |
. . . . . . . . . . . . . . . . . . . . 21
                                             |
66 | 65 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . 20
                                                 |
67 | 66 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . 19
                                                         |
68 | 67 | breq1d 4426 |
. . . . . . . . . . . . . . . . . 18
                                                               |
69 | 59, 68 | imbi12d 326 |
. . . . . . . . . . . . . . . . 17
       
      
                                
      
                          |
70 | 69 | ralbiia 2830 |
. . . . . . . . . . . . . . . 16
 
                                                                                     |
71 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . 19
       |
72 | 71 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . 18
               |
73 | 72 | breq1d 4426 |
. . . . . . . . . . . . . . . . 17
       
         |
74 | 73 | ralrab 3212 |
. . . . . . . . . . . . . . . 16
 
                                 
                                      |
75 | 70, 74 | bitr4i 260 |
. . . . . . . . . . . . . . 15
 
                                                                                    |
76 | 51 | adantrr 728 |
. . . . . . . . . . . . . . . . 17
         
                                     |
77 | 76 | raleqdv 3005 |
. . . . . . . . . . . . . . . 16
         
                                             
     
                                  |
78 | 17 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
  |
79 | 24 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
  |
80 | | lhop1.l |
. . . . . . . . . . . . . . . . . . . 20
   |
81 | 80 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
  |
82 | | lhop1.f |
. . . . . . . . . . . . . . . . . . . 20
           |
83 | 82 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
          |
84 | | lhop1.g |
. . . . . . . . . . . . . . . . . . . 20
           |
85 | 84 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
          |
86 | | lhop1.if |
. . . . . . . . . . . . . . . . . . . 20
         |
87 | 86 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
        |
88 | | lhop1.ig |
. . . . . . . . . . . . . . . . . . . 20
         |
89 | 88 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
        |
90 | | lhop1.f0 |
. . . . . . . . . . . . . . . . . . . 20
  lim    |
91 | 90 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                

lim    |
92 | | lhop1.g0 |
. . . . . . . . . . . . . . . . . . . 20
  lim    |
93 | 92 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                

lim    |
94 | | lhop1.gn0 |
. . . . . . . . . . . . . . . . . . . 20
   |
95 | 94 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
  |
96 | | lhop1.gd0 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
97 | 96 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
    |
98 | 1 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
                     lim    |
99 | 3 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
    |
100 | 78 | rexrd 9716 |
. . . . . . . . . . . . . . . . . . . . 21
                         
                                
  |
101 | | simprll 777 |
. . . . . . . . . . . . . . . . . . . . . . 23
                         
                                
  |
102 | 101 | rpred 11370 |
. . . . . . . . . . . . . . . . . . . . . 22
                         
                                
  |
103 | 102, 78 | readdcld 9696 |
. . . . . . . . . . . . . . . . . . . . 21
                         
                                
    |
104 | | iocssre 11743 |
. . . . . . . . . . . . . . . . . . . . 21
       ![(,] (,]](_ioc.gif)   
  |
105 | 100, 103,
104 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . 20
                         
                                
  ![(,] (,]](_ioc.gif)      |
106 | 79 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       
              
                                      |
107 | 102 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
       
              
                                      |
108 | 78 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
       
              
                                      |
109 | 107, 108 | readdcld 9696 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
       
              
                                        |
110 | 109 | rexrd 9716 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       
              
                                        |
111 | 106, 110 | ifclda 3925 |
. . . . . . . . . . . . . . . . . . . . 21
                         
                                
           |
112 | 78, 101 | ltaddrp2d 11401 |
. . . . . . . . . . . . . . . . . . . . . 22
                         
                                
    |
113 | 103 | rexrd 9716 |
. . . . . . . . . . . . . . . . . . . . . . 23
                         
                                
    |
114 | | xrltmin 11506 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
       |
115 | 100, 79, 113, 114 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . 22
                         
                                
         
       |
116 | 81, 112, 115 | mpbir2and 938 |
. . . . . . . . . . . . . . . . . . . . 21
                         
                                
           |
117 | | xrmin2 11502 |
. . . . . . . . . . . . . . . . . . . . . 22
      
           |
118 | 79, 113, 117 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . 21
                         
                                
             |
119 | | elioc1 11707 |
. . . . . . . . . . . . . . . . . . . . . 22
                 ![(,] (,]](_ioc.gif)   
  
      
          
             |
120 | 100, 113,
119 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . 21
                         
                                
  
         ![(,] (,]](_ioc.gif)   
  
      
          
             |
121 | 111, 116,
118, 120 | mpbir3and 1197 |
. . . . . . . . . . . . . . . . . . . 20
                         
                                
           ![(,] (,]](_ioc.gif)      |
122 | 105, 121 | sseldd 3445 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
           |
123 | 79, 113, 45 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
           |
124 | | simprlr 778 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
    
          |
125 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
                         
                                
     
                                 |
126 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . 19
         |
127 | 78, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 98, 99, 122, 123, 124, 125, 126 | lhop1lem 23014 |
. . . . . . . . . . . . . . . . . 18
                         
                                
                      |
128 | 2 | rpcnd 11372 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
129 | | 2cnd 10710 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
130 | | 2ne0 10730 |
. . . . . . . . . . . . . . . . . . . . 21
 |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
132 | 128, 129,
131 | divcan2d 10413 |
. . . . . . . . . . . . . . . . . . 19
 

      |
133 | 132 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
                         
                                
      |
134 | 127, 133 | breqtrd 4441 |
. . . . . . . . . . . . . . . . 17
                         
                                
                  |
135 | 134 | expr 624 |
. . . . . . . . . . . . . . . 16
         
                
                                                  |
136 | 77, 135 | sylbid 223 |
. . . . . . . . . . . . . . 15
         
                                                                 |
137 | 75, 136 | syl5bi 225 |
. . . . . . . . . . . . . 14
         
                                                                              |
138 | 137 | expr 624 |
. . . . . . . . . . . . 13
                                                                                        |
139 | 53, 138 | sylbid 223 |
. . . . . . . . . . . 12
                                                                                       |
140 | 139 | expdimp 443 |
. . . . . . . . . . 11
   


                                                                                 |
141 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . 18
           |
142 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . 18
           |
143 | 141, 142 | oveq12d 6333 |
. . . . . . . . . . . . . . . . 17
                       |
144 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
                                 |
145 | | ovex 6343 |
. . . . . . . . . . . . . . . . 17
           |
146 | 143, 144,
145 | fvmpt3i 5976 |
. . . . . . . . . . . . . . . 16
                                     |
147 | 146 | oveq1d 6330 |
. . . . . . . . . . . . . . 15
                                         |
148 | 147 | fveq2d 5892 |
. . . . . . . . . . . . . 14
                                                 |
149 | 148 | breq1d 4426 |
. . . . . . . . . . . . 13
                                                   |
150 | 149 | imbi2d 322 |
. . . . . . . . . . . 12
                                                                                                                                                       |
151 | 150 | adantl 472 |
. . . . . . . . . . 11
   


                                                                                                                                                       |
152 | 140, 151 | sylibrd 242 |
. . . . . . . . . 10
   


                                                                                           |
153 | 152 | adantld 473 |
. . . . . . . . 9
   


      
      
 
                                              
                              |
154 | 153 | com23 81 |
. . . . . . . 8
   


                                                       
      
                              |
155 | 154 | ralrimdva 2818 |
. . . . . . 7
      
                                              
                                             |
156 | 155 | reximdva 2874 |
. . . . . 6
 

 
                                                
                                             |
157 | 8, 156 | syld 45 |
. . . . 5
 

 
                                               
                                             |
158 | 157 | ralrimdva 2818 |
. . . 4
                                                 
         
      
                              |
159 | 158 | anim2d 573 |
. . 3
            
      
                                                                                 |
160 | | dvf 22911 |
. . . . . . . 8
         |
161 | 86 | feq2d 5737 |
. . . . . . . 8
      
  
             |
162 | 160, 161 | mpbii 216 |
. . . . . . 7
             |
163 | 162 | ffvelrnda 6045 |
. . . . . 6
 
    
        |
164 | | dvf 22911 |
. . . . . . . 8
         |
165 | 88 | feq2d 5737 |
. . . . . . . 8
      
  
             |
166 | 164, 165 | mpbii 216 |
. . . . . . 7
             |
167 | 166 | ffvelrnda 6045 |
. . . . . 6
 
    
        |
168 | 96 | adantr 471 |
. . . . . . 7
 
    
    |
169 | | ffn 5751 |
. . . . . . . . . . 11
                   |
170 | 166, 169 | syl 17 |
. . . . . . . . . 10
         |
171 | | fnfvelrn 6042 |
. . . . . . . . . 10
       
               |
172 | 170, 171 | sylan 478 |
. . . . . . . . 9
 
    
      
   |
173 | | eleq1 2528 |
. . . . . . . . 9
               
     |
174 | 172, 173 | syl5ibcom 228 |
. . . . . . . 8
 
    
            |
175 | 174 | necon3bd 2650 |
. . . . . . 7
 
    

           |
176 | 168, 175 | mpd 15 |
. . . . . 6
 
    
        |
177 | 163, 167,
176 | divcld 10411 |
. . . . 5
 
    
                |
178 | 177, 63 | fmptd 6069 |
. . . 4
                               |
179 | | ax-resscn 9622 |
. . . . . 6
 |
180 | 14, 179 | sstri 3453 |
. . . . 5
     |
181 | 180 | a1i 11 |
. . . 4
    
  |
182 | 17 | recnd 9695 |
. . . 4
   |
183 | 178, 181,
182 | ellimc3 22883 |
. . 3
                       lim            
      
                                   |
184 | 82 | ffvelrnda 6045 |
. . . . . . 7
 
    
      |
185 | 184 | recnd 9695 |
. . . . . 6
 
    
      |
186 | 84 | ffvelrnda 6045 |
. . . . . . 7
 
    
      |
187 | 186 | recnd 9695 |
. . . . . 6
 
    
      |
188 | 94 | adantr 471 |
. . . . . . 7
 
    
  |
189 | | ffn 5751 |
. . . . . . . . . . 11
               |
190 | 84, 189 | syl 17 |
. . . . . . . . . 10
       |
191 | | fnfvelrn 6042 |
. . . . . . . . . 10
     
           |
192 | 190, 191 | sylan 478 |
. . . . . . . . 9
 
    
      |
193 | | eleq1 2528 |
. . . . . . . . 9
             |
194 | 192, 193 | syl5ibcom 228 |
. . . . . . . 8
 
    
        |
195 | 194 | necon3bd 2650 |
. . . . . . 7
 
    

       |
196 | 188, 195 | mpd 15 |
. . . . . 6
 
    
      |
197 | 185, 187,
196 | divcld 10411 |
. . . . 5
 
    
            |
198 | 197, 144 | fmptd 6069 |
. . . 4
                           |
199 | 198, 181,
182 | ellimc3 22883 |
. . 3
                   lim            
      
                               |
200 | 159, 183,
199 | 3imtr4d 276 |
. 2
                       lim 
                 lim     |
201 | 1, 200 | mpd 15 |
1
                  lim    |