Step | Hyp | Ref
| Expression |
1 | | limccl 22909 |
. . . 4
 lim   |
2 | | mullimcf.b |
. . . 4
  lim    |
3 | 1, 2 | sseldi 3416 |
. . 3
   |
4 | | limccl 22909 |
. . . 4
 lim   |
5 | | mullimcf.c |
. . . 4
  lim    |
6 | 4, 5 | sseldi 3416 |
. . 3
   |
7 | 3, 6 | mulcld 9681 |
. 2
     |
8 | | simpr 468 |
. . . . 5
 

  |
9 | 3 | adantr 472 |
. . . . 5
 

  |
10 | 6 | adantr 472 |
. . . . 5
 

  |
11 | | mulcn2 13736 |
. . . . 5
                                   |
12 | 8, 9, 10, 11 | syl3anc 1292 |
. . . 4
 

                                |
13 | | mullimcf.f |
. . . . . . . . . . . . . . . 16
       |
14 | | fdm 5745 |
. . . . . . . . . . . . . . . . . 18
       |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
16 | | limcrcl 22908 |
. . . . . . . . . . . . . . . . . . 19
  lim      
   |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
18 | 17 | simp2d 1043 |
. . . . . . . . . . . . . . . . 17
   |
19 | 15, 18 | eqsstr3d 3453 |
. . . . . . . . . . . . . . . 16

  |
20 | 17 | simp3d 1044 |
. . . . . . . . . . . . . . . 16
   |
21 | 13, 19, 20 | ellimc3 22913 |
. . . . . . . . . . . . . . 15
   lim     
                        |
22 | 2, 21 | mpbid 215 |
. . . . . . . . . . . . . 14
    
                       |
23 | 22 | simprd 470 |
. . . . . . . . . . . . 13
   
                      |
24 | 23 | r19.21bi 2776 |
. . . . . . . . . . . 12
 

                        |
25 | 24 | adantrr 731 |
. . . . . . . . . . 11
 
                           |
26 | | mullimcf.g |
. . . . . . . . . . . . . . . 16
       |
27 | 26, 19, 20 | ellimc3 22913 |
. . . . . . . . . . . . . . 15
   lim     
                        |
28 | 5, 27 | mpbid 215 |
. . . . . . . . . . . . . 14
    
                       |
29 | 28 | simprd 470 |
. . . . . . . . . . . . 13
   
                      |
30 | 29 | r19.21bi 2776 |
. . . . . . . . . . . 12
 

                        |
31 | 30 | adantrl 730 |
. . . . . . . . . . 11
 
                           |
32 | | reeanv 2944 |
. . . . . . . . . . 11
    
                                         
 

                       
      
              |
33 | 25, 31, 32 | sylanbrc 677 |
. . . . . . . . . 10
 
                           
                       |
34 | | ifcl 3914 |
. . . . . . . . . . . . . 14
          |
35 | 34 | 3ad2ant2 1052 |
. . . . . . . . . . . . 13
                              
                             |
36 | | nfv 1769 |
. . . . . . . . . . . . . . 15
       |
37 | | nfv 1769 |
. . . . . . . . . . . . . . 15
     |
38 | | nfra1 2785 |
. . . . . . . . . . . . . . . 16
    
      
            |
39 | | nfra1 2785 |
. . . . . . . . . . . . . . . 16
    
      
            |
40 | 38, 39 | nfan 2031 |
. . . . . . . . . . . . . . 15
                        
                      |
41 | 36, 37, 40 | nf3an 2033 |
. . . . . . . . . . . . . 14
      
 
 
 
      
          

                       |
42 | | simp11l 1141 |
. . . . . . . . . . . . . . . . . . 19
      
 
 
 
      
          

                     
             
  |
43 | | simp1rl 1095 |
. . . . . . . . . . . . . . . . . . . 20
                              
                        |
44 | 43 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . 19
      
 
 
 
      
          

                     
             
  |
45 | 42, 44 | jca 541 |
. . . . . . . . . . . . . . . . . 18
      
 
 
 
      
          

                     
             
    |
46 | | simp12 1061 |
. . . . . . . . . . . . . . . . . 18
      
 
 
 
      
          

                     
             
    |
47 | | simp13l 1145 |
. . . . . . . . . . . . . . . . . 18
      
 
 
 
      
          

                     
             

                      |
48 | 45, 46, 47 | jca31 543 |
. . . . . . . . . . . . . . . . 17
      
 
 
 
      
          

                     
             
  
                            |
49 | | simp1r 1055 |
. . . . . . . . . . . . . . . . . 18
        

                                     
      
             |
50 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
        

                                     |
51 | | simp3l 1058 |
. . . . . . . . . . . . . . . . . . 19
        

                                     |
52 | | simplll 776 |
. . . . . . . . . . . . . . . . . . . . 21
   
   

                    
  |
53 | 52 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . 20
        

                                     |
54 | | simp1lr 1094 |
. . . . . . . . . . . . . . . . . . . 20
        

                                       |
55 | | simp3r 1059 |
. . . . . . . . . . . . . . . . . . . 20
        

                                          
     |
56 | | simp1l 1054 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
              |
57 | | simp2 1031 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
              |
58 | 19 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
59 | 56, 57, 58 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
              |
60 | 56, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
              |
61 | 59, 60 | subcld 10005 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                |
62 | 61 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . . 21
     
                    |
63 | | rpre 11331 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
64 | 63 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
65 | 64 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . 22
     
              |
66 | | rpre 11331 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
67 | 66 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
68 | 67 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . 22
     
              |
69 | 65, 68 | ifcld 3915 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   |
70 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   
     |
71 | | min1 11506 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        |
72 | 65, 68, 71 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   |
73 | 62, 69, 65, 70, 72 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . 20
     
                    |
74 | 53, 54, 50, 55, 73 | syl211anc 1298 |
. . . . . . . . . . . . . . . . . . 19
        

                                           |
75 | 51, 74 | jca 541 |
. . . . . . . . . . . . . . . . . 18
        

                                   
         |
76 | | rsp 2773 |
. . . . . . . . . . . . . . . . . 18
 
                    
                       |
77 | 49, 50, 75, 76 | syl3c 62 |
. . . . . . . . . . . . . . . . 17
        

                                               |
78 | 48, 77 | syld3an1 1338 |
. . . . . . . . . . . . . . . 16
      
 
 
 
      
          

                     
             
            |
79 | | simp1l 1054 |
. . . . . . . . . . . . . . . . . . 19
                              
                        |
80 | 79, 43 | jca 541 |
. . . . . . . . . . . . . . . . . 18
                              
                          |
81 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
                              
                          |
82 | | simp3r 1059 |
. . . . . . . . . . . . . . . . . 18
                              
                      
                      |
83 | 80, 81, 82 | jca31 543 |
. . . . . . . . . . . . . . . . 17
                              
                        
   

                       |
84 | | simp1r 1055 |
. . . . . . . . . . . . . . . . . 18
        

                                     
      
             |
85 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
        

                                     |
86 | | simp3l 1058 |
. . . . . . . . . . . . . . . . . . 19
        

                                     |
87 | | simplll 776 |
. . . . . . . . . . . . . . . . . . . . 21
   
   

                    
  |
88 | 87 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . 20
        

                                     |
89 | | simp1lr 1094 |
. . . . . . . . . . . . . . . . . . . 20
        

                                       |
90 | | simp3r 1059 |
. . . . . . . . . . . . . . . . . . . 20
        

                                          
     |
91 | | min2 11507 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        |
92 | 65, 68, 91 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   |
93 | 62, 69, 68, 70, 92 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . 20
     
                    |
94 | 88, 89, 85, 90, 93 | syl211anc 1298 |
. . . . . . . . . . . . . . . . . . 19
        

                                           |
95 | 86, 94 | jca 541 |
. . . . . . . . . . . . . . . . . 18
        

                                   
         |
96 | | rsp 2773 |
. . . . . . . . . . . . . . . . . 18
 
                    
                       |
97 | 84, 85, 95, 96 | syl3c 62 |
. . . . . . . . . . . . . . . . 17
        

                                               |
98 | 83, 97 | syl3an1 1325 |
. . . . . . . . . . . . . . . 16
      
 
 
 
      
          

                     
             
            |
99 | 78, 98 | jca 541 |
. . . . . . . . . . . . . . 15
      
 
 
 
      
          

                     
             
          
             |
100 | 99 | 3exp 1230 |
. . . . . . . . . . . . . 14
                              
                        
                                      |
101 | 41, 100 | ralrimi 2800 |
. . . . . . . . . . . . 13
                              
                      
                                       |
102 | | breq2 4399 |
. . . . . . . . . . . . . . . . 17
            
              |
103 | 102 | anbi2d 718 |
. . . . . . . . . . . . . . . 16
       
       
               |
104 | 103 | imbi1d 324 |
. . . . . . . . . . . . . . 15
                                        
                                      |
105 | 104 | ralbidv 2829 |
. . . . . . . . . . . . . 14
                                        
 
                                      |
106 | 105 | rspcev 3136 |
. . . . . . . . . . . . 13
         
                                   
                                    |
107 | 35, 101, 106 | syl2anc 673 |
. . . . . . . . . . . 12
                              
                                                          |
108 | 107 | 3exp 1230 |
. . . . . . . . . . 11
 
        
                                          

                                    |
109 | 108 | rexlimdvv 2877 |
. . . . . . . . . 10
 
    
  
                                          

                                   |
110 | 33, 109 | mpd 15 |
. . . . . . . . 9
 
                                       |
111 | 110 | adantlr 729 |
. . . . . . . 8
       

                                  |
112 | 111 | 3adant3 1050 |
. . . . . . 7
      
                      
     

                                  |
113 | | nfv 1769 |
. . . . . . . . . . 11
                                       |
114 | | nfra1 2785 |
. . . . . . . . . . 11
    
      
          
             |
115 | 113, 114 | nfan 2031 |
. . . . . . . . . 10
     
 
 
                      
    
                                    |
116 | | simp1l 1054 |
. . . . . . . . . . . . . . 15
      
                      
       |
117 | 116 | ad2antrr 740 |
. . . . . . . . . . . . . 14
                                     

                                
  |
118 | 117 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
           |
119 | | simp2 1031 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
           |
120 | | mullimcf.h |
. . . . . . . . . . . . . . . . 17
             |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
               |
122 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
           |
123 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
           |
124 | 122, 123 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
                       |
125 | 124 | adantl 473 |
. . . . . . . . . . . . . . . 16
                           |
126 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 
   |
127 | 13 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . 17
 
       |
128 | 26 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . 17
 
       |
129 | 127, 128 | mulcld 9681 |
. . . . . . . . . . . . . . . 16
 
             |
130 | 121, 125,
126, 129 | fvmptd 5969 |
. . . . . . . . . . . . . . 15
 
                 |
131 | 130 | oveq1d 6323 |
. . . . . . . . . . . . . 14
 
                    
    |
132 | 131 | fveq2d 5883 |
. . . . . . . . . . . . 13
 
         
                       |
133 | 118, 119,
132 | syl2anc 673 |
. . . . . . . . . . . 12
     
 
 
                      
    
                                  
                                   
     |
134 | 127, 128 | jca 541 |
. . . . . . . . . . . . . 14
 
             |
135 | 118, 119,
134 | syl2anc 673 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
                     |
136 | | simpll3 1071 |
. . . . . . . . . . . . . 14
                                     

                                
                       
      |
137 | 136 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
                                       |
138 | | rsp 2773 |
. . . . . . . . . . . . . . 15
 
                               

                                   |
139 | 138 | 3imp 1224 |
. . . . . . . . . . . . . 14
    
      
          
           
                                 |
140 | 139 | 3adant1l 1284 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
                                 |
141 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
               |
142 | 141 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
                       |
143 | 142 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
           
             |
144 | 143 | anbi1d 719 |
. . . . . . . . . . . . . . 15
                   
          
          |
145 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
               |
146 | 145 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                  
    |
147 | 146 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
           
                   |
148 | 147 | breq1d 4405 |
. . . . . . . . . . . . . . 15
               
          
      |
149 | 144, 148 | imbi12d 327 |
. . . . . . . . . . . . . 14
                                                                     |
150 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
               |
151 | 150 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
                       |
152 | 151 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
           
             |
153 | 152 | anbi2d 718 |
. . . . . . . . . . . . . . 15
                       
          
              |
154 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
                       |
155 | 154 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                          
    |
156 | 155 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
               
                       |
157 | 156 | breq1d 4405 |
. . . . . . . . . . . . . . 15
                   
              
      |
158 | 153, 157 | imbi12d 327 |
. . . . . . . . . . . . . 14
                                                                                     |
159 | 149, 158 | rspc2v 3147 |
. . . . . . . . . . . . 13
                                   
                                                 |
160 | 135, 137,
140, 159 | syl3c 62 |
. . . . . . . . . . . 12
     
 
 
                      
    
                                  
                             |
161 | 133, 160 | eqbrtrd 4416 |
. . . . . . . . . . 11
     
 
 
                      
    
                                  
                       |
162 | 161 | 3exp 1230 |
. . . . . . . . . 10
                                     

                                

                         |
163 | 115, 162 | ralrimi 2800 |
. . . . . . . . 9
                                     

                                

                        |
164 | 163 | ex 441 |
. . . . . . . 8
   
                                
 
                               

                         |
165 | 164 | reximdva 2858 |
. . . . . . 7
      
                      
         
      
          
                               
       |
166 | 112, 165 | mpd 15 |
. . . . . 6
      
                      
     

                        |
167 | 166 | 3exp 1230 |
. . . . 5
 

    
                                                       |
168 | 167 | rexlimdvv 2877 |
. . . 4
 

 
                        
                       
       |
169 | 12, 168 | mpd 15 |
. . 3
 

                   
      |
170 | 169 | ralrimiva 2809 |
. 2
   
                        |
171 | 13 | ffvelrnda 6037 |
. . . . 5
 
       |
172 | 26 | ffvelrnda 6037 |
. . . . 5
 
       |
173 | 171, 172 | mulcld 9681 |
. . . 4
 
             |
174 | 173, 120 | fmptd 6061 |
. . 3
       |
175 | 174, 19, 20 | ellimc3 22913 |
. 2
     lim       
                          |
176 | 7, 170, 175 | mpbir2and 936 |
1
    lim    |