Step | Hyp | Ref
| Expression |
1 | | limccl 22830 |
. . 3
 
    lim   |
2 | | limcleqr.l |
. . 3
  
    lim    |
3 | 1, 2 | sseldi 3430 |
. 2
   |
4 | | simp-4r 777 |
. . . . . . 7
     
 
        
      
     
           
        
      
                
  |
5 | | simplr 762 |
. . . . . . 7
     
 
        
      
     
           
        
      
                
  |
6 | 4, 5 | ifcld 3924 |
. . . . . 6
     
 
        
      
     
           
        
      
                
 
     |
7 | | nfv 1761 |
. . . . . . . . . . 11
     |
8 | | nfv 1761 |
. . . . . . . . . . 11
  |
9 | 7, 8 | nfan 2011 |
. . . . . . . . . 10
   

  |
10 | | nfra1 2769 |
. . . . . . . . . 10
                                   |
11 | 9, 10 | nfan 2011 |
. . . . . . . . 9
     
                                   |
12 | | nfv 1761 |
. . . . . . . . 9
  |
13 | 11, 12 | nfan 2011 |
. . . . . . . 8
     
 
        
      
     
             |
14 | | nfra1 2769 |
. . . . . . . 8
          
      
                 |
15 | 13, 14 | nfan 2011 |
. . . . . . 7
         

                                        
      
                  |
16 | | simp-6l 780 |
. . . . . . . . . . . . 13
         

                                        
      
                    |
17 | 16 | 3ad2antl1 1170 |
. . . . . . . . . . . 12
       

                                           
      
                               
  |
18 | | simpl2 1012 |
. . . . . . . . . . . 12
       

                                           
      
                               
  |
19 | | simpr 463 |
. . . . . . . . . . . 12
       

                                           
      
                               
  |
20 | | mnfxr 11414 |
. . . . . . . . . . . . . 14
 |
21 | 20 | a1i 11 |
. . . . . . . . . . . . 13
 

  |
22 | | limcleqr.b |
. . . . . . . . . . . . . . 15
   |
23 | 22 | rexrd 9690 |
. . . . . . . . . . . . . 14
   |
24 | 23 | 3ad2ant1 1029 |
. . . . . . . . . . . . 13
 

  |
25 | | limcleqr.a |
. . . . . . . . . . . . . . 15

  |
26 | 25 | sselda 3432 |
. . . . . . . . . . . . . 14
 
   |
27 | 26 | 3adant3 1028 |
. . . . . . . . . . . . 13
 

  |
28 | 27 | mnfltd 11426 |
. . . . . . . . . . . . 13
 

  |
29 | | simp3 1010 |
. . . . . . . . . . . . 13
 

  |
30 | 21, 24, 27, 28, 29 | eliood 37595 |
. . . . . . . . . . . 12
 

     |
31 | 17, 18, 19, 30 | syl3anc 1268 |
. . . . . . . . . . 11
       

                                           
      
                               
     |
32 | | fvres 5879 |
. . . . . . . . . . . . . 14
                   |
33 | 32 | oveq1d 6305 |
. . . . . . . . . . . . 13
                       |
34 | 33 | eqcomd 2457 |
. . . . . . . . . . . 12
            
          |
35 | 34 | fveq2d 5869 |
. . . . . . . . . . 11
                               |
36 | 31, 35 | syl 17 |
. . . . . . . . . 10
       

                                           
      
                               
                           |
37 | | simp-4r 777 |
. . . . . . . . . . . . 13
         

                                        
      
                          
      
     
            |
38 | 37 | 3ad2antl1 1170 |
. . . . . . . . . . . 12
       

                                           
      
                               
        
      
     
            |
39 | 18, 31 | elind 3618 |
. . . . . . . . . . . 12
       

                                           
      
                               

      |
40 | 38, 39 | jca 535 |
. . . . . . . . . . 11
       

                                           
      
                               
 

                             

       |
41 | | simpl3l 1063 |
. . . . . . . . . . . 12
       

                                           
      
                               
  |
42 | 4 | adantr 467 |
. . . . . . . . . . . . . 14
         

                                        
      
                    |
43 | 42 | 3ad2antl1 1170 |
. . . . . . . . . . . . 13
       

                                           
      
                               
  |
44 | 5 | adantr 467 |
. . . . . . . . . . . . . 14
         

                                        
      
                    |
45 | 44 | 3ad2antl1 1170 |
. . . . . . . . . . . . 13
       

                                           
      
                               
  |
46 | | simpl3r 1064 |
. . . . . . . . . . . . 13
       

                                           
      
                               
             |
47 | | simpl1 1011 |
. . . . . . . . . . . . . . 15
   
        
       |
48 | | simprr 766 |
. . . . . . . . . . . . . . 15
   
        
       |
49 | 26 | recnd 9669 |
. . . . . . . . . . . . . . . . 17
 
   |
50 | 22 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18
   |
51 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
   |
52 | 49, 51 | subcld 9986 |
. . . . . . . . . . . . . . . 16
 
     |
53 | 52 | abscld 13498 |
. . . . . . . . . . . . . . 15
 
         |
54 | 47, 48, 53 | syl2anc 667 |
. . . . . . . . . . . . . 14
   
        
             |
55 | | rpre 11308 |
. . . . . . . . . . . . . . . . . 18

  |
56 | 55 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     |
57 | | rpre 11308 |
. . . . . . . . . . . . . . . . . 18

  |
58 | 57 | adantl 468 |
. . . . . . . . . . . . . . . . 17
     |
59 | 56, 58 | ifcld 3924 |
. . . . . . . . . . . . . . . 16
          |
60 | 59 | 3adant1 1026 |
. . . . . . . . . . . . . . 15
 
        |
61 | 60 | adantr 467 |
. . . . . . . . . . . . . 14
   
        
            |
62 | 56 | 3adant1 1026 |
. . . . . . . . . . . . . . 15
 
   |
63 | 62 | adantr 467 |
. . . . . . . . . . . . . 14
   
        
       |
64 | | simprl 764 |
. . . . . . . . . . . . . 14
   
        
                  |
65 | 58 | 3adant1 1026 |
. . . . . . . . . . . . . . . 16
 
   |
66 | | min1 11483 |
. . . . . . . . . . . . . . . 16
 
        |
67 | 62, 65, 66 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
        |
68 | 67 | adantr 467 |
. . . . . . . . . . . . . 14
   
        
         
  |
69 | 54, 61, 63, 64, 68 | ltletrd 9795 |
. . . . . . . . . . . . 13
   
        
             |
70 | 17, 43, 45, 46, 18, 69 | syl32anc 1276 |
. . . . . . . . . . . 12
       

                                           
      
                               
        |
71 | 41, 70 | jca 535 |
. . . . . . . . . . 11
       

                                           
      
                               
          |
72 | | rspa 2755 |
. . . . . . . . . . 11
                                 

      
      
     
            |
73 | 40, 71, 72 | sylc 62 |
. . . . . . . . . 10
       

                                           
      
                               
     
           |
74 | 36, 73 | eqbrtrd 4423 |
. . . . . . . . 9
       

                                           
      
                               
            |
75 | | simp-6l 780 |
. . . . . . . . . . . . 13
         

                                        
      
                    |
76 | 75 | 3ad2antl1 1170 |
. . . . . . . . . . . 12
       

                                           
      
                                  |
77 | 76, 22 | syl 17 |
. . . . . . . . . . 11
       

                                           
      
                                  |
78 | | simpl2 1012 |
. . . . . . . . . . . 12
       

                                           
      
                                  |
79 | 76, 78, 26 | syl2anc 667 |
. . . . . . . . . . 11
       

                                           
      
                                  |
80 | | id 22 |
. . . . . . . . . . . . . 14
   |
81 | 80 | necomd 2679 |
. . . . . . . . . . . . 13
   |
82 | 81 | ad2antrr 732 |
. . . . . . . . . . . 12
          
       |
83 | 82 | 3ad2antl3 1172 |
. . . . . . . . . . 11
       

                                           
      
                                  |
84 | | simpr 463 |
. . . . . . . . . . 11
       

                                           
      
                                  |
85 | 77, 79, 83, 84 | lttri5d 37517 |
. . . . . . . . . 10
       

                                           
      
                                  |
86 | | simp-6l 780 |
. . . . . . . . . . . . . 14
         

                                        
      
                    |
87 | 86 | 3ad2antl1 1170 |
. . . . . . . . . . . . 13
       

                                           
      
                               
  |
88 | | simpl2 1012 |
. . . . . . . . . . . . 13
       

                                           
      
                               
  |
89 | | simpr 463 |
. . . . . . . . . . . . 13
       

                                           
      
                               
  |
90 | 23 | 3ad2ant1 1029 |
. . . . . . . . . . . . . 14
 

  |
91 | | pnfxr 11412 |
. . . . . . . . . . . . . . 15
 |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . 14
 

  |
93 | 26 | 3adant3 1028 |
. . . . . . . . . . . . . 14
 

  |
94 | | simp3 1010 |
. . . . . . . . . . . . . 14
 

  |
95 | 93 | ltpnfd 11423 |
. . . . . . . . . . . . . 14
 

  |
96 | 90, 92, 93, 94, 95 | eliood 37595 |
. . . . . . . . . . . . 13
 

     |
97 | 87, 88, 89, 96 | syl3anc 1268 |
. . . . . . . . . . . 12
       

                                           
      
                               
     |
98 | | fvres 5879 |
. . . . . . . . . . . . . . 15
   
               |
99 | 98 | eqcomd 2457 |
. . . . . . . . . . . . . 14
   
               |
100 | 99 | oveq1d 6305 |
. . . . . . . . . . . . 13
   
                   |
101 | 100 | fveq2d 5869 |
. . . . . . . . . . . 12
   
                           |
102 | 97, 101 | syl 17 |
. . . . . . . . . . 11
       

                                           
      
                               
                           |
103 | | simpl1r 1060 |
. . . . . . . . . . . . 13
       

                                           
      
                               
        
      
                  |
104 | 88, 97 | elind 3618 |
. . . . . . . . . . . . 13
       

                                           
      
                               

      |
105 | 103, 104 | jca 535 |
. . . . . . . . . . . 12
       

                                           
      
                               
 
                                       |
106 | | simpl3l 1063 |
. . . . . . . . . . . . 13
       

                                           
      
                               
  |
107 | 4 | adantr 467 |
. . . . . . . . . . . . . . 15
         

                                        
      
                    |
108 | 107 | 3ad2antl1 1170 |
. . . . . . . . . . . . . 14
       

                                           
      
                               
  |
109 | 5 | adantr 467 |
. . . . . . . . . . . . . . 15
         

                                        
      
                    |
110 | 109 | 3ad2antl1 1170 |
. . . . . . . . . . . . . 14
       

                                           
      
                               
  |
111 | | simpl3r 1064 |
. . . . . . . . . . . . . 14
       

                                           
      
                               
             |
112 | 65 | adantr 467 |
. . . . . . . . . . . . . . 15
   
        
       |
113 | | min2 11484 |
. . . . . . . . . . . . . . . . 17
 
        |
114 | 62, 65, 113 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
        |
115 | 114 | adantr 467 |
. . . . . . . . . . . . . . 15
   
        
         
  |
116 | 54, 61, 112, 64, 115 | ltletrd 9795 |
. . . . . . . . . . . . . 14
   
        
             |
117 | 87, 108, 110, 111, 88, 116 | syl32anc 1276 |
. . . . . . . . . . . . 13
       

                                           
      
                               
        |
118 | 106, 117 | jca 535 |
. . . . . . . . . . . 12
       

                                           
      
                               
          |
119 | | rspa 2755 |
. . . . . . . . . . . 12
          
      
                     
                           |
120 | 105, 118,
119 | sylc 62 |
. . . . . . . . . . 11
       

                                           
      
                               
                 |
121 | 102, 120 | eqbrtrd 4423 |
. . . . . . . . . 10
       

                                           
      
                               
            |
122 | 85, 121 | syldan 473 |
. . . . . . . . 9
       

                                           
      
                                            |
123 | 74, 122 | pm2.61dan 800 |
. . . . . . . 8
         

                                        
      
                                           |
124 | 123 | 3exp 1207 |
. . . . . . 7
     
 
        
      
     
           
        
      
                

                            |
125 | 15, 124 | ralrimi 2788 |
. . . . . 6
     
 
        
      
     
           
        
      
                

                           |
126 | | breq2 4406 |
. . . . . . . . . 10
            
              |
127 | 126 | anbi2d 710 |
. . . . . . . . 9
       
       
               |
128 | 127 | imbi1d 319 |
. . . . . . . 8
                          
                            |
129 | 128 | ralbidv 2827 |
. . . . . . 7
                           

                            |
130 | 129 | rspcev 3150 |
. . . . . 6
         
                        

                      |
131 | 6, 125, 130 | syl2anc 667 |
. . . . 5
     
 
        
      
     
           
        
      
                
                        |
132 | | limcleqr.r |
. . . . . . . . . 10
  
    lim    |
133 | | limcleqr.f |
. . . . . . . . . . . 12
       |
134 | | fresin 5752 |
. . . . . . . . . . . 12
     
               |
135 | 133, 134 | syl 17 |
. . . . . . . . . . 11
                 |
136 | | inss2 3653 |
. . . . . . . . . . . . 13
         |
137 | | ioosscn 37591 |
. . . . . . . . . . . . 13
    |
138 | 136, 137 | sstri 3441 |
. . . . . . . . . . . 12
      |
139 | 138 | a1i 11 |
. . . . . . . . . . 11
        |
140 | 135, 139,
50 | ellimc3 22834 |
. . . . . . . . . 10
        lim 
           
      
                    |
141 | 132, 140 | mpbid 214 |
. . . . . . . . 9
            
      
                   |
142 | 141 | simprd 465 |
. . . . . . . 8
           
      
                  |
143 | 142 | r19.21bi 2757 |
. . . . . . 7
 

         
      
                  |
144 | | limcleqr.leqr |
. . . . . . . . . . . . 13
   |
145 | 144 | oveq2d 6306 |
. . . . . . . . . . . 12
              
          |
146 | 145 | fveq2d 5869 |
. . . . . . . . . . 11
                                 |
147 | 146 | breq1d 4412 |
. . . . . . . . . 10
                                   |
148 | 147 | imbi2d 318 |
. . . . . . . . 9
                
                        
             |
149 | 148 | rexralbidv 2909 |
. . . . . . . 8
           
      
                
        
      
                   |
150 | 149 | adantr 467 |
. . . . . . 7
 

 
        
      
                
        
      
                   |
151 | 143, 150 | mpbird 236 |
. . . . . 6
 

         
      
                  |
152 | 151 | ad2antrr 732 |
. . . . 5
   

                                                                     |
153 | 131, 152 | r19.29a 2932 |
. . . 4
   

                                                          |
154 | | fresin 5752 |
. . . . . . . . 9
     
               |
155 | 133, 154 | syl 17 |
. . . . . . . 8
                 |
156 | | inss2 3653 |
. . . . . . . . . 10
         |
157 | | ioossre 11696 |
. . . . . . . . . 10
    |
158 | 156, 157 | sstri 3441 |
. . . . . . . . 9
      |
159 | | ax-resscn 9596 |
. . . . . . . . . 10
 |
160 | 159 | a1i 11 |
. . . . . . . . 9

  |
161 | 158, 160 | syl5ss 3443 |
. . . . . . . 8
        |
162 | 155, 161,
50 | ellimc3 22834 |
. . . . . . 7
        lim 
                                       |
163 | 2, 162 | mpbid 214 |
. . . . . 6
            
      
     
             |
164 | 163 | simprd 465 |
. . . . 5
           
      
     
            |
165 | 164 | r19.21bi 2757 |
. . . 4
 

         
      
     
            |
166 | 153, 165 | r19.29a 2932 |
. . 3
 

                        |
167 | 166 | ralrimiva 2802 |
. 2
   
                      |
168 | 25, 159 | syl6ss 3444 |
. . 3

  |
169 | 133, 168,
50 | ellimc3 22834 |
. 2
   lim     
                        |
170 | 3, 167, 169 | mpbir2and 933 |
1
  lim    |