Step | Hyp | Ref
| Expression |
1 | | limccl 22909 |
. . . 4
 lim   |
2 | | addlimc.e |
. . . 4
  lim    |
3 | 1, 2 | sseldi 3416 |
. . 3
   |
4 | | limccl 22909 |
. . . 4
 lim   |
5 | | addlimc.i |
. . . 4
  lim    |
6 | 4, 5 | sseldi 3416 |
. . 3
   |
7 | 3, 6 | addcld 9680 |
. 2
     |
8 | | addlimc.b |
. . . . . . . . . 10
 
   |
9 | | addlimc.f |
. . . . . . . . . 10
   |
10 | 8, 9 | fmptd 6061 |
. . . . . . . . 9
       |
11 | 9, 8, 2 | limcmptdm 37812 |
. . . . . . . . 9

  |
12 | | limcrcl 22908 |
. . . . . . . . . . 11
  lim      
   |
13 | 2, 12 | syl 17 |
. . . . . . . . . 10
         |
14 | 13 | simp3d 1044 |
. . . . . . . . 9
   |
15 | 10, 11, 14 | ellimc3 22913 |
. . . . . . . 8
   lim     
                        |
16 | 2, 15 | mpbid 215 |
. . . . . . 7
    
                       |
17 | 16 | simprd 470 |
. . . . . 6
   
                      |
18 | | rphalfcl 11350 |
. . . . . 6

    |
19 | | breq2 4399 |
. . . . . . . . 9
             
               |
20 | 19 | imbi2d 323 |
. . . . . . . 8
     
      
                                    |
21 | 20 | rexralbidv 2898 |
. . . . . . 7
    

                    

                         |
22 | 21 | rspccva 3135 |
. . . . . 6
    
                                                 |
23 | 17, 18, 22 | syl2an 485 |
. . . . 5
 

                          |
24 | | addlimc.c |
. . . . . . . . . 10
 
   |
25 | | addlimc.g |
. . . . . . . . . 10
   |
26 | 24, 25 | fmptd 6061 |
. . . . . . . . 9
       |
27 | 26, 11, 14 | ellimc3 22913 |
. . . . . . . 8
   lim     
                        |
28 | 5, 27 | mpbid 215 |
. . . . . . 7
    
                       |
29 | 28 | simprd 470 |
. . . . . 6
   
                      |
30 | | breq2 4399 |
. . . . . . . . 9
             
               |
31 | 30 | imbi2d 323 |
. . . . . . . 8
     
      
                                    |
32 | 31 | rexralbidv 2898 |
. . . . . . 7
    

                    

                         |
33 | 32 | rspccva 3135 |
. . . . . 6
    
                                                 |
34 | 29, 18, 33 | syl2an 485 |
. . . . 5
 

                          |
35 | | reeanv 2944 |
. . . . 5
    
                                             
 

                         
      
                |
36 | 23, 34, 35 | sylanbrc 677 |
. . . 4
 

                          
                         |
37 | | ifcl 3914 |
. . . . . . . 8
          |
38 | 37 | 3ad2ant2 1052 |
. . . . . . 7
       
 
      
             
                               |
39 | | nfv 1769 |
. . . . . . . . 9
     |
40 | | nfv 1769 |
. . . . . . . . 9
     |
41 | | nfra1 2785 |
. . . . . . . . . 10
    
      
              |
42 | | nfra1 2785 |
. . . . . . . . . 10
    
      
              |
43 | 41, 42 | nfan 2031 |
. . . . . . . . 9
                          
                        |
44 | 39, 40, 43 | nf3an 2033 |
. . . . . . . 8
   
                           
                         |
45 | | simp11l 1141 |
. . . . . . . . . . . 12
   
                           
                       
             
  |
46 | | simp2 1031 |
. . . . . . . . . . . 12
   
                           
                       
             
  |
47 | 45, 46 | jca 541 |
. . . . . . . . . . 11
   
                           
                       
             
    |
48 | | rpre 11331 |
. . . . . . . . . . . . . 14

  |
49 | 48 | adantl 473 |
. . . . . . . . . . . . 13
 

  |
50 | 49 | 3ad2ant1 1051 |
. . . . . . . . . . . 12
       
 
      
             
                          |
51 | 50 | 3ad2ant1 1051 |
. . . . . . . . . . 11
   
                           
                       
             
  |
52 | | simp13l 1145 |
. . . . . . . . . . . 12
   
                           
                       
             

                        |
53 | | simp3l 1058 |
. . . . . . . . . . . . 13
   
                           
                       
             
  |
54 | 11 | sselda 3418 |
. . . . . . . . . . . . . . . . 17
 
   |
55 | 45, 46, 54 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
   
                           
                       
             
  |
56 | 45, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
   
                           
                       
             
  |
57 | 55, 56 | subcld 10005 |
. . . . . . . . . . . . . . 15
   
                           
                       
             
    |
58 | 57 | abscld 13575 |
. . . . . . . . . . . . . 14
   
                           
                       
             
        |
59 | 38 | rpred 11364 |
. . . . . . . . . . . . . . 15
       
 
      
             
                               |
60 | 59 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
   
                           
                       
             
 
     |
61 | | simpl 464 |
. . . . . . . . . . . . . . . . 17
     |
62 | 61 | rpred 11364 |
. . . . . . . . . . . . . . . 16
     |
63 | 62 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . 15
       
 
      
             
                          |
64 | 63 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
   
                           
                       
             
  |
65 | | simp3r 1059 |
. . . . . . . . . . . . . 14
   
                           
                       
             
             |
66 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
     |
67 | 66 | rpred 11364 |
. . . . . . . . . . . . . . . . 17
     |
68 | | min1 11506 |
. . . . . . . . . . . . . . . . 17
 
        |
69 | 62, 67, 68 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
       
  |
70 | 69 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . 15
       
 
      
             
                            
  |
71 | 70 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
   
                           
                       
             
 
     |
72 | 58, 60, 64, 65, 71 | ltletrd 9812 |
. . . . . . . . . . . . 13
   
                           
                       
             
        |
73 | 53, 72 | jca 541 |
. . . . . . . . . . . 12
   
                           
                       
             
          |
74 | | rsp 2773 |
. . . . . . . . . . . 12
 
                      
                         |
75 | 52, 46, 73, 74 | syl3c 62 |
. . . . . . . . . . 11
   
                           
                       
             
              |
76 | 47, 51, 75 | jca31 543 |
. . . . . . . . . 10
   
                           
                       
             
  
                 |
77 | | simp13r 1146 |
. . . . . . . . . . 11
   
                           
                       
             

                        |
78 | 67 | 3ad2ant2 1052 |
. . . . . . . . . . . . . 14
       
 
      
             
                          |
79 | 78 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
   
                           
                       
             
  |
80 | | min2 11507 |
. . . . . . . . . . . . . . . 16
 
        |
81 | 62, 67, 80 | syl2anc 673 |
. . . . . . . . . . . . . . 15
       
  |
82 | 81 | 3ad2ant2 1052 |
. . . . . . . . . . . . . 14
       
 
      
             
                            
  |
83 | 82 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
   
                           
                       
             
 
     |
84 | 58, 60, 79, 65, 83 | ltletrd 9812 |
. . . . . . . . . . . 12
   
                           
                       
             
        |
85 | 53, 84 | jca 541 |
. . . . . . . . . . 11
   
                           
                       
             
          |
86 | | rsp 2773 |
. . . . . . . . . . 11
 
                      
                         |
87 | 77, 46, 85, 86 | syl3c 62 |
. . . . . . . . . 10
   
                           
                       
             
              |
88 | 8, 24 | addcld 9680 |
. . . . . . . . . . . . . . . 16
 
 
   |
89 | | addlimc.h |
. . . . . . . . . . . . . . . 16
     |
90 | 88, 89 | fmptd 6061 |
. . . . . . . . . . . . . . 15
       |
91 | 90 | ffvelrnda 6037 |
. . . . . . . . . . . . . 14
 
       |
92 | 91 | ad3antrrr 744 |
. . . . . . . . . . . . 13
                                       |
93 | | simp-4l 784 |
. . . . . . . . . . . . . 14
                                   |
94 | 93, 7 | syl 17 |
. . . . . . . . . . . . 13
                                     |
95 | 92, 94 | subcld 10005 |
. . . . . . . . . . . 12
                                      
    |
96 | 95 | abscld 13575 |
. . . . . . . . . . 11
                                               |
97 | 10 | ffvelrnda 6037 |
. . . . . . . . . . . . . . 15
 
       |
98 | 97 | ad3antrrr 744 |
. . . . . . . . . . . . . 14
                                       |
99 | 93, 3 | syl 17 |
. . . . . . . . . . . . . 14
                                   |
100 | 98, 99 | subcld 10005 |
. . . . . . . . . . . . 13
                                         |
101 | 100 | abscld 13575 |
. . . . . . . . . . . 12
                                             |
102 | 26 | ffvelrnda 6037 |
. . . . . . . . . . . . . . 15
 
       |
103 | 102 | ad3antrrr 744 |
. . . . . . . . . . . . . 14
                                       |
104 | 93, 6 | syl 17 |
. . . . . . . . . . . . . 14
                                   |
105 | 103, 104 | subcld 10005 |
. . . . . . . . . . . . 13
                                         |
106 | 105 | abscld 13575 |
. . . . . . . . . . . 12
                                             |
107 | 101, 106 | readdcld 9688 |
. . . . . . . . . . 11
                                                         |
108 | | simpllr 777 |
. . . . . . . . . . 11
                                   |
109 | | nfv 1769 |
. . . . . . . . . . . . . . . . . 18
  
  |
110 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . . 21
       |
111 | 89, 110 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . . 20
   |
112 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . 20
   |
113 | 111, 112 | nffv 5886 |
. . . . . . . . . . . . . . . . . . 19
       |
114 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
115 | 9, 114 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . . . 21
   |
116 | 115, 112 | nffv 5886 |
. . . . . . . . . . . . . . . . . . . 20
       |
117 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . 20
  |
118 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
119 | 25, 118 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . . . 21
   |
120 | 119, 112 | nffv 5886 |
. . . . . . . . . . . . . . . . . . . 20
       |
121 | 116, 117,
120 | nfov 6334 |
. . . . . . . . . . . . . . . . . . 19
             |
122 | 113, 121 | nfeq 2623 |
. . . . . . . . . . . . . . . . . 18
                 |
123 | 109, 122 | nfim 2023 |
. . . . . . . . . . . . . . . . 17
   
                 |
124 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . 19
 
   |
125 | 124 | anbi2d 718 |
. . . . . . . . . . . . . . . . . 18
  

     |
126 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
127 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
128 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
129 | 127, 128 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . 19
                       |
130 | 126, 129 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . 18
               
                 |
131 | 125, 130 | imbi12d 327 |
. . . . . . . . . . . . . . . . 17
   
                 
                   |
132 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
 
   |
133 | 89 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . 19
  
          |
134 | 132, 88, 133 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 
         |
135 | 9 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
136 | 132, 8, 135 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
137 | 136 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . 19
 
       |
138 | 25 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
139 | 132, 24, 138 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
140 | 139 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . 19
 
       |
141 | 137, 140 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
 
 
             |
142 | 134, 141 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
 
                 |
143 | 123, 131,
142 | chvar 2119 |
. . . . . . . . . . . . . . . 16
 
                 |
144 | 143 | ad3antrrr 744 |
. . . . . . . . . . . . . . 15
                                                 |
145 | 144 | oveq1d 6323 |
. . . . . . . . . . . . . 14
                                      
                  |
146 | 98, 103, 99, 104 | addsub4d 10052 |
. . . . . . . . . . . . . 14
                                            
                  |
147 | 145, 146 | eqtrd 2505 |
. . . . . . . . . . . . 13
                                      
                  |
148 | 147 | fveq2d 5883 |
. . . . . . . . . . . 12
                                                                 |
149 | 100, 105 | abstrid 13595 |
. . . . . . . . . . . 12
                                                  
                        |
150 | 148, 149 | eqbrtrd 4416 |
. . . . . . . . . . 11
                                            
                        |
151 | | simplr 770 |
. . . . . . . . . . . 12
                                               |
152 | | simpr 468 |
. . . . . . . . . . . 12
                                               |
153 | 101, 106,
108, 151, 152 | lt2halvesd 10883 |
. . . . . . . . . . 11
                                                         |
154 | 96, 107, 108, 150, 153 | lelttrd 9810 |
. . . . . . . . . 10
                                               |
155 | 76, 87, 154 | syl2anc 673 |
. . . . . . . . 9
   
                           
                       
             
        
     |
156 | 155 | 3exp 1230 |
. . . . . . . 8
       
 
      
             
                          
                    
       |
157 | 44, 156 | ralrimi 2800 |
. . . . . . 7
       
 
      
             
                        
                             |
158 | | breq2 4399 |
. . . . . . . . . . 11
            
              |
159 | 158 | anbi2d 718 |
. . . . . . . . . 10
       
       
               |
160 | 159 | imbi1d 324 |
. . . . . . . . 9
                        
   
                              |
161 | 160 | ralbidv 2829 |
. . . . . . . 8
                         
   

                              |
162 | 161 | rspcev 3136 |
. . . . . . 7
         
                    
     

                        |
163 | 38, 157, 162 | syl2anc 673 |
. . . . . 6
       
 
      
             
                                           
      |
164 | 163 | 3exp 1230 |
. . . . 5
 

                            
                      
                   
        |
165 | 164 | rexlimdvv 2877 |
. . . 4
 

 
  
                                              

                         |
166 | 36, 165 | mpd 15 |
. . 3
 

                   
      |
167 | 166 | ralrimiva 2809 |
. 2
   
                        |
168 | 90, 11, 14 | ellimc3 22913 |
. 2
     lim       
                          |
169 | 7, 167, 168 | mpbir2and 936 |
1
    lim    |