Step | Hyp | Ref
| Expression |
1 | | limccl 22909 |
. . . 4
 lim   |
2 | | mullimc.x |
. . . 4
  lim    |
3 | 1, 2 | sseldi 3416 |
. . 3
   |
4 | | limccl 22909 |
. . . 4
 lim   |
5 | | mullimc.y |
. . . 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 | | mullimc.b |
. . . . . . . . . . . . . . . . 17
 
   |
14 | | mullimc.f |
. . . . . . . . . . . . . . . . 17
   |
15 | 13, 14 | fmptd 6061 |
. . . . . . . . . . . . . . . 16
       |
16 | 14, 13 | dmmptd 5718 |
. . . . . . . . . . . . . . . . 17
   |
17 | | limcrcl 22908 |
. . . . . . . . . . . . . . . . . . 19
  lim      
   |
18 | 2, 17 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
19 | 18 | simp2d 1043 |
. . . . . . . . . . . . . . . . 17
   |
20 | 16, 19 | eqsstr3d 3453 |
. . . . . . . . . . . . . . . 16

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

                        |
26 | 25 | adantrr 731 |
. . . . . . . . . . 11
 
                           |
27 | | mullimc.c |
. . . . . . . . . . . . . . . . 17
 
   |
28 | | mullimc.g |
. . . . . . . . . . . . . . . . 17
   |
29 | 27, 28 | fmptd 6061 |
. . . . . . . . . . . . . . . 16
       |
30 | 29, 20, 21 | ellimc3 22913 |
. . . . . . . . . . . . . . 15
   lim     
                        |
31 | 5, 30 | mpbid 215 |
. . . . . . . . . . . . . 14
    
                       |
32 | 31 | simprd 470 |
. . . . . . . . . . . . 13
   
                      |
33 | 32 | r19.21bi 2776 |
. . . . . . . . . . . 12
 

                        |
34 | 33 | adantrl 730 |
. . . . . . . . . . 11
 
                           |
35 | | reeanv 2944 |
. . . . . . . . . . 11
    
                                         
 

                       
      
              |
36 | 26, 34, 35 | sylanbrc 677 |
. . . . . . . . . 10
 
                           
                       |
37 | | ifcl 3914 |
. . . . . . . . . . . . . 14
          |
38 | 37 | 3ad2ant2 1052 |
. . . . . . . . . . . . 13
                              
                             |
39 | | nfv 1769 |
. . . . . . . . . . . . . . 15
       |
40 | | nfv 1769 |
. . . . . . . . . . . . . . 15
     |
41 | | nfra1 2785 |
. . . . . . . . . . . . . . . 16
    
      
            |
42 | | nfra1 2785 |
. . . . . . . . . . . . . . . 16
    
      
            |
43 | 41, 42 | nfan 2031 |
. . . . . . . . . . . . . . 15
                        
                      |
44 | 39, 40, 43 | nf3an 2033 |
. . . . . . . . . . . . . 14
      
 
 
 
      
          

                       |
45 | | simp11l 1141 |
. . . . . . . . . . . . . . . . . . 19
      
 
 
 
      
          

                     
             
  |
46 | | simp1rl 1095 |
. . . . . . . . . . . . . . . . . . . 20
                              
                        |
47 | 46 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . 19
      
 
 
 
      
          

                     
             
  |
48 | 45, 47 | jca 541 |
. . . . . . . . . . . . . . . . . 18
      
 
 
 
      
          

                     
             
    |
49 | | simp12 1061 |
. . . . . . . . . . . . . . . . . 18
      
 
 
 
      
          

                     
             
    |
50 | | simp13l 1145 |
. . . . . . . . . . . . . . . . . 18
      
 
 
 
      
          

                     
             

                      |
51 | 48, 49, 50 | jca31 543 |
. . . . . . . . . . . . . . . . 17
      
 
 
 
      
          

                     
             
  
                            |
52 | | simp1r 1055 |
. . . . . . . . . . . . . . . . . 18
        

                                     
      
             |
53 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
        

                                     |
54 | | simp3l 1058 |
. . . . . . . . . . . . . . . . . . 19
        

                                     |
55 | | simplll 776 |
. . . . . . . . . . . . . . . . . . . . 21
   
   

                    
  |
56 | 55 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . 20
        

                                     |
57 | | simp1lr 1094 |
. . . . . . . . . . . . . . . . . . . 20
        

                                       |
58 | | simp3r 1059 |
. . . . . . . . . . . . . . . . . . . 20
        

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

  |
67 | 66 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
68 | 67 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . 22
     
              |
69 | | rpre 11331 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
70 | 69 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
71 | 70 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . 22
     
              |
72 | 68, 71 | ifcld 3915 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   |
73 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   
     |
74 | | min1 11506 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        |
75 | 68, 71, 74 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   |
76 | 65, 72, 68, 73, 75 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . 20
     
                    |
77 | 56, 57, 53, 58, 76 | syl211anc 1298 |
. . . . . . . . . . . . . . . . . . 19
        

                                           |
78 | 54, 77 | jca 541 |
. . . . . . . . . . . . . . . . . 18
        

                                   
         |
79 | | rsp 2773 |
. . . . . . . . . . . . . . . . . 18
 
                    
                       |
80 | 52, 53, 78, 79 | syl3c 62 |
. . . . . . . . . . . . . . . . 17
        

                                               |
81 | 51, 80 | syld3an1 1338 |
. . . . . . . . . . . . . . . 16
      
 
 
 
      
          

                     
             
            |
82 | | simp1l 1054 |
. . . . . . . . . . . . . . . . . . 19
                              
                        |
83 | 82, 46 | jca 541 |
. . . . . . . . . . . . . . . . . 18
                              
                          |
84 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
                              
                          |
85 | | simp3r 1059 |
. . . . . . . . . . . . . . . . . 18
                              
                      
                      |
86 | 83, 84, 85 | jca31 543 |
. . . . . . . . . . . . . . . . 17
                              
                        
   

                       |
87 | | simp1r 1055 |
. . . . . . . . . . . . . . . . . 18
        

                                     
      
             |
88 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
        

                                     |
89 | | simp3l 1058 |
. . . . . . . . . . . . . . . . . . 19
        

                                     |
90 | | simplll 776 |
. . . . . . . . . . . . . . . . . . . . 21
   
   

                    
  |
91 | 90 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . 20
        

                                     |
92 | | simp1lr 1094 |
. . . . . . . . . . . . . . . . . . . 20
        

                                       |
93 | | simp3r 1059 |
. . . . . . . . . . . . . . . . . . . 20
        

                                          
     |
94 | | min2 11507 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        |
95 | 68, 71, 94 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
     
                   |
96 | 65, 72, 71, 73, 95 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . 20
     
                    |
97 | 91, 92, 88, 93, 96 | syl211anc 1298 |
. . . . . . . . . . . . . . . . . . 19
        

                                           |
98 | 89, 97 | jca 541 |
. . . . . . . . . . . . . . . . . 18
        

                                   
         |
99 | | rsp 2773 |
. . . . . . . . . . . . . . . . . 18
 
                    
                       |
100 | 87, 88, 98, 99 | syl3c 62 |
. . . . . . . . . . . . . . . . 17
        

                                               |
101 | 86, 100 | syl3an1 1325 |
. . . . . . . . . . . . . . . 16
      
 
 
 
      
          

                     
             
            |
102 | 81, 101 | jca 541 |
. . . . . . . . . . . . . . 15
      
 
 
 
      
          

                     
             
          
             |
103 | 102 | 3exp 1230 |
. . . . . . . . . . . . . 14
                              
                        
                                      |
104 | 44, 103 | ralrimi 2800 |
. . . . . . . . . . . . 13
                              
                      
                                       |
105 | | breq2 4399 |
. . . . . . . . . . . . . . . . 17
            
              |
106 | 105 | anbi2d 718 |
. . . . . . . . . . . . . . . 16
       
       
               |
107 | 106 | imbi1d 324 |
. . . . . . . . . . . . . . 15
                                        
                                      |
108 | 107 | ralbidv 2829 |
. . . . . . . . . . . . . 14
                                        
 
                                      |
109 | 108 | rspcev 3136 |
. . . . . . . . . . . . 13
         
                                   
                                    |
110 | 38, 104, 109 | syl2anc 673 |
. . . . . . . . . . . 12
                              
                                                          |
111 | 110 | 3exp 1230 |
. . . . . . . . . . 11
 
        
                                          

                                    |
112 | 111 | rexlimdvv 2877 |
. . . . . . . . . 10
 
    
  
                                          

                                   |
113 | 36, 112 | mpd 15 |
. . . . . . . . 9
 
                                       |
114 | 113 | adantlr 729 |
. . . . . . . 8
       

                                  |
115 | 114 | 3adant3 1050 |
. . . . . . 7
      
                      
     

                                  |
116 | | nfv 1769 |
. . . . . . . . . . 11
                                       |
117 | | nfra1 2785 |
. . . . . . . . . . 11
    
      
          
             |
118 | 116, 117 | nfan 2031 |
. . . . . . . . . 10
     
 
 
                      
    
                                    |
119 | | simp1l 1054 |
. . . . . . . . . . . . . . 15
      
                      
       |
120 | 119 | ad2antrr 740 |
. . . . . . . . . . . . . 14
                                     

                                
  |
121 | 120 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
           |
122 | | simp2 1031 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
           |
123 | | nfv 1769 |
. . . . . . . . . . . . . . . . 17
  
  |
124 | | mullimc.h |
. . . . . . . . . . . . . . . . . . . 20
     |
125 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . 20
       |
126 | 124, 125 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . 19
   |
127 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
128 | 126, 127 | nffv 5886 |
. . . . . . . . . . . . . . . . . 18
       |
129 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . . 21
     |
130 | 14, 129 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . . 20
   |
131 | 130, 127 | nffv 5886 |
. . . . . . . . . . . . . . . . . . 19
       |
132 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
  |
133 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . . . . . 21
     |
134 | 28, 133 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . . 20
   |
135 | 134, 127 | nffv 5886 |
. . . . . . . . . . . . . . . . . . 19
       |
136 | 131, 132,
135 | nfov 6334 |
. . . . . . . . . . . . . . . . . 18
             |
137 | 128, 136 | nfeq 2623 |
. . . . . . . . . . . . . . . . 17
                 |
138 | 123, 137 | nfim 2023 |
. . . . . . . . . . . . . . . 16
   
                 |
139 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
 
   |
140 | 139 | anbi2d 718 |
. . . . . . . . . . . . . . . . 17
  

     |
141 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
           |
142 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
143 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
144 | 142, 143 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
                       |
145 | 141, 144 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . 17
               
                 |
146 | 140, 145 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
   
                 
                   |
147 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
 
   |
148 | 13, 27 | mulcld 9681 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
149 | 124 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . 18
  
          |
150 | 147, 148,
149 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
         |
151 | 14 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
152 | 147, 13, 151 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
 
       |
153 | 152 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . 18
 
       |
154 | 28 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
155 | 147, 27, 154 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
 
       |
156 | 155 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . 18
 
       |
157 | 153, 156 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
 
 
             |
158 | 150, 157 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
 
                 |
159 | 138, 146,
158 | chvar 2119 |
. . . . . . . . . . . . . . 15
 
                 |
160 | 159 | oveq1d 6323 |
. . . . . . . . . . . . . 14
 
                    
    |
161 | 160 | fveq2d 5883 |
. . . . . . . . . . . . 13
 
         
                       |
162 | 121, 122,
161 | syl2anc 673 |
. . . . . . . . . . . 12
     
 
 
                      
    
                                  
                                   
     |
163 | 15 | ffvelrnda 6037 |
. . . . . . . . . . . . . . 15
 
       |
164 | 29 | ffvelrnda 6037 |
. . . . . . . . . . . . . . 15
 
       |
165 | 163, 164 | jca 541 |
. . . . . . . . . . . . . 14
 
             |
166 | 121, 122,
165 | syl2anc 673 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
                     |
167 | | simpll3 1071 |
. . . . . . . . . . . . . 14
                                     

                                
                       
      |
168 | 167 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
                                       |
169 | | rsp 2773 |
. . . . . . . . . . . . . . 15
 
                               

                                   |
170 | 169 | 3imp 1224 |
. . . . . . . . . . . . . 14
    
      
          
           
                                 |
171 | 170 | 3adant1l 1284 |
. . . . . . . . . . . . 13
     
 
 
                      
    
                                  
                                 |
172 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
               |
173 | 172 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
                       |
174 | 173 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
           
             |
175 | 174 | anbi1d 719 |
. . . . . . . . . . . . . . 15
                   
          
          |
176 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
               |
177 | 176 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                  
    |
178 | 177 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
           
                   |
179 | 178 | breq1d 4405 |
. . . . . . . . . . . . . . 15
               
          
      |
180 | 175, 179 | imbi12d 327 |
. . . . . . . . . . . . . 14
                                                                     |
181 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
               |
182 | 181 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
                       |
183 | 182 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
           
             |
184 | 183 | anbi2d 718 |
. . . . . . . . . . . . . . 15
                       
          
              |
185 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
                       |
186 | 185 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                          
    |
187 | 186 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
               
                       |
188 | 187 | breq1d 4405 |
. . . . . . . . . . . . . . 15
                   
              
      |
189 | 184, 188 | imbi12d 327 |
. . . . . . . . . . . . . 14
                                                                                     |
190 | 180, 189 | rspc2v 3147 |
. . . . . . . . . . . . 13
                                   
                                                 |
191 | 166, 168,
171, 190 | syl3c 62 |
. . . . . . . . . . . 12
     
 
 
                      
    
                                  
                             |
192 | 162, 191 | eqbrtrd 4416 |
. . . . . . . . . . 11
     
 
 
                      
    
                                  
                       |
193 | 192 | 3exp 1230 |
. . . . . . . . . 10
                                     

                                

                         |
194 | 118, 193 | ralrimi 2800 |
. . . . . . . . 9
                                     

                                

                        |
195 | 194 | ex 441 |
. . . . . . . 8
   
                                
 
                               

                         |
196 | 195 | reximdva 2858 |
. . . . . . 7
      
                      
         
      
          
                               
       |
197 | 115, 196 | mpd 15 |
. . . . . 6
      
                      
     

                        |
198 | 197 | 3exp 1230 |
. . . . 5
 

    
                                                       |
199 | 198 | rexlimdvv 2877 |
. . . 4
 

 
                        
                       
       |
200 | 12, 199 | mpd 15 |
. . 3
 

                   
      |
201 | 200 | ralrimiva 2809 |
. 2
   
                        |
202 | 148, 124 | fmptd 6061 |
. . 3
       |
203 | 202, 20, 21 | ellimc3 22913 |
. 2
     lim       
                          |
204 | 7, 201, 203 | mpbir2and 936 |
1
    lim    |