Step | Hyp | Ref
| Expression |
1 | | dvco.bg |
. . . 4
       |
2 | | eqid 2461 |
. . . . 5
 ↾t   ↾t   |
3 | | dvco.j |
. . . . 5
  ℂfld |
4 | | eqid 2461 |
. . . . 5
                                         |
5 | | dvcobr.t |
. . . . 5

  |
6 | | dvco.g |
. . . . . 6
       |
7 | | dvco.x |
. . . . . . 7

  |
8 | | dvcobr.s |
. . . . . . 7

  |
9 | 7, 8 | sstrd 3453 |
. . . . . 6

  |
10 | 6, 9 | fssd 5760 |
. . . . 5
       |
11 | | dvco.y |
. . . . 5

  |
12 | 2, 3, 4, 5, 10, 11 | eldv 22901 |
. . . 4
            ↾t                           lim      |
13 | 1, 12 | mpbid 215 |
. . 3
       ↾t                           lim     |
14 | 13 | simpld 465 |
. 2
      ↾t        |
15 | | dvco.bf |
. . . . . . 7
           |
16 | | dvco.f |
. . . . . . . 8
       |
17 | 8, 16, 7 | dvcl 22902 |
. . . . . . 7
 
        
  |
18 | 15, 17 | mpdan 679 |
. . . . . 6
   |
19 | 18 | ad2antrr 737 |
. . . . 5
                
  |
20 | 16 | adantr 471 |
. . . . . . . . 9
 

          |
21 | | eldifi 3566 |
. . . . . . . . . 10
       |
22 | | ffvelrn 6042 |
. . . . . . . . . 10
     
       |
23 | 6, 21, 22 | syl2an 484 |
. . . . . . . . 9
 

          |
24 | 20, 23 | ffvelrnd 6045 |
. . . . . . . 8
 

              |
25 | 24 | adantr 471 |
. . . . . . 7
                           |
26 | 6 | adantr 471 |
. . . . . . . . . 10
 

          |
27 | 5, 10, 11 | dvbss 22904 |
. . . . . . . . . . . 12
     |
28 | | reldv 22873 |
. . . . . . . . . . . . 13
   |
29 | | releldm 5085 |
. . . . . . . . . . . . 13
        
    |
30 | 28, 1, 29 | sylancr 674 |
. . . . . . . . . . . 12
     |
31 | 27, 30 | sseldd 3444 |
. . . . . . . . . . 11
   |
32 | 31 | adantr 471 |
. . . . . . . . . 10
 

   
  |
33 | 26, 32 | ffvelrnd 6045 |
. . . . . . . . 9
 

          |
34 | 20, 33 | ffvelrnd 6045 |
. . . . . . . 8
 

              |
35 | 34 | adantr 471 |
. . . . . . 7
                           |
36 | 25, 35 | subcld 10011 |
. . . . . 6
                                     |
37 | 10 | ad2antrr 737 |
. . . . . . . 8
                       |
38 | 21 | ad2antlr 738 |
. . . . . . . 8
                   |
39 | 37, 38 | ffvelrnd 6045 |
. . . . . . 7
                       |
40 | 31 | ad2antrr 737 |
. . . . . . . 8
                   |
41 | 37, 40 | ffvelrnd 6045 |
. . . . . . 7
                       |
42 | 39, 41 | subcld 10011 |
. . . . . 6
                             |
43 | | simpr 467 |
. . . . . . 7
                
          |
44 | 39, 41 | subeq0ad 10021 |
. . . . . . . 8
                                       |
45 | 44 | necon3abid 2671 |
. . . . . . 7
                           
           |
46 | 43, 45 | mpbird 240 |
. . . . . 6
                             |
47 | 36, 42, 46 | divcld 10410 |
. . . . 5
                                                 |
48 | 19, 47 | ifclda 3924 |
. . . 4
 

                                                 |
49 | 11, 5 | sstrd 3453 |
. . . . 5

  |
50 | 10, 49, 31 | dvlem 22899 |
. . . 4
 

                    |
51 | | ssid 3462 |
. . . . 5
 |
52 | 51 | a1i 11 |
. . . 4

  |
53 | 3 | cnfldtopon 21851 |
. . . . . . 7
TopOn   |
54 | | txtopon 20654 |
. . . . . . 7
  TopOn 
TopOn  
  TopOn      |
55 | 53, 53, 54 | mp2an 683 |
. . . . . 6
  TopOn     |
56 | 55 | toponunii 19995 |
. . . . . . 7
      |
57 | 56 | restid 15380 |
. . . . . 6
   TopOn       ↾t        |
58 | 55, 57 | ax-mp 5 |
. . . . 5
   ↾t       |
59 | 58 | eqcomi 2470 |
. . . 4
    
↾t     |
60 | 23 | anim1i 576 |
. . . . . . 7
                                 |
61 | | eldifsn 4109 |
. . . . . . 7
                             |
62 | 60, 61 | sylibr 217 |
. . . . . 6
                               |
63 | 62 | anasss 657 |
. . . . 5
 
                             |
64 | | eldifsni 4110 |
. . . . . . . 8
               |
65 | | ifnefalse 3904 |
. . . . . . . 8
                                                            |
66 | 64, 65 | syl 17 |
. . . . . . 7
                                                                |
67 | 66 | adantl 472 |
. . . . . 6
 

                                                               |
68 | 6, 31 | ffvelrnd 6045 |
. . . . . . 7
       |
69 | 16, 9, 68 | dvlem 22899 |
. . . . . 6
 

                                |
70 | 67, 69 | eqeltrd 2539 |
. . . . 5
 

                                         |
71 | | limcresi 22888 |
. . . . . . 7
 lim    
    lim   |
72 | 6 | feqmptd 5940 |
. . . . . . . . . 10
         |
73 | 72 | reseq1d 5122 |
. . . . . . . . 9
                     |
74 | | difss 3571 |
. . . . . . . . . 10
   
 |
75 | | resmpt 5172 |
. . . . . . . . . 10
            
                |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . 9
      
                |
77 | 73, 76 | syl6eq 2511 |
. . . . . . . 8
                   |
78 | 77 | oveq1d 6329 |
. . . . . . 7
   
    lim             lim    |
79 | 71, 78 | syl5sseq 3491 |
. . . . . 6
  lim 
           lim    |
80 | | eqid 2461 |
. . . . . . . . . 10
 ↾t   ↾t   |
81 | 80, 3 | dvcnp2 22922 |
. . . . . . . . 9
       
      ↾t        |
82 | 5, 10, 11, 30, 81 | syl31anc 1279 |
. . . . . . . 8
   
↾t        |
83 | 3, 80 | cnplimc 22890 |
. . . . . . . . 9
 
 
  
↾t                lim      |
84 | 49, 31, 83 | syl2anc 671 |
. . . . . . . 8
     ↾t     
          lim      |
85 | 82, 84 | mpbid 215 |
. . . . . . 7
           lim     |
86 | 85 | simprd 469 |
. . . . . 6
      lim    |
87 | 79, 86 | sseldd 3444 |
. . . . 5
                lim    |
88 | | eqid 2461 |
. . . . . . . . 9
 ↾t   ↾t   |
89 | | eqid 2461 |
. . . . . . . . 9
                                                                 |
90 | 88, 3, 89, 8, 16, 7 | eldv 22901 |
. . . . . . . 8
                    ↾t                                       lim          |
91 | 15, 90 | mpbid 215 |
. . . . . . 7
           ↾t                                       lim         |
92 | 91 | simprd 469 |
. . . . . 6
                                  lim        |
93 | 66 | mpteq2ia 4498 |
. . . . . . 7
                                                                          |
94 | 93 | oveq1i 6324 |
. . . . . 6
                                          lim                                       lim       |
95 | 92, 94 | syl6eleqr 2550 |
. . . . 5
                                           lim        |
96 | | eqeq1 2465 |
. . . . . 6
         
           |
97 | | fveq2 5887 |
. . . . . . . 8
                   |
98 | 97 | oveq1d 6329 |
. . . . . . 7
                                       |
99 | | oveq1 6321 |
. . . . . . 7
                       |
100 | 98, 99 | oveq12d 6332 |
. . . . . 6
                                                           |
101 | 96, 100 | ifbieq2d 3917 |
. . . . 5
                                                                                 |
102 | | iftrue 3898 |
. . . . . 6
                                                      |
103 | 102 | ad2antll 740 |
. . . . 5
 
                                                            |
104 | 63, 70, 87, 95, 101, 103 | limcco 22896 |
. . . 4
                                                   lim    |
105 | 13 | simprd 469 |
. . . 4
                      lim    |
106 | 3 | mulcn 21947 |
. . . . 5
     |
107 | 5, 10, 11 | dvcl 22902 |
. . . . . . 7
 
    
  |
108 | 1, 107 | mpdan 679 |
. . . . . 6
   |
109 | | opelxpi 4884 |
. . . . . 6
 
        |
110 | 18, 108, 109 | syl2anc 671 |
. . . . 5
        |
111 | 56 | cncnpi 20342 |
. . . . 5
      
                 |
112 | 106, 110,
111 | sylancr 674 |
. . . 4
    
         |
113 | 48, 50, 52, 52, 3, 59, 104, 105, 112 | limccnp2 22895 |
. . 3
                                                                     lim    |
114 | | oveq1 6321 |
. . . . . . . 8
                                            
                                                                            |
115 | 114 | eqeq1d 2463 |
. . . . . . 7
                                                                                  
                                                                                    |
116 | | oveq1 6321 |
. . . . . . . 8
                                                                                                                                                                                     |
117 | 116 | eqeq1d 2463 |
. . . . . . 7
                                                                                                                                              
                                                                                    |
118 | 19 | mul01d 9857 |
. . . . . . . 8
                     |
119 | 9 | adantr 471 |
. . . . . . . . . . . . . 14
 

      |
120 | 119, 23 | sseldd 3444 |
. . . . . . . . . . . . 13
 

          |
121 | 119, 33 | sseldd 3444 |
. . . . . . . . . . . . 13
 

          |
122 | 120, 121 | subeq0ad 10021 |
. . . . . . . . . . . 12
 

                          |
123 | 122 | biimpar 492 |
. . . . . . . . . . 11
                             |
124 | 123 | oveq1d 6329 |
. . . . . . . . . 10
                                     |
125 | 49 | adantr 471 |
. . . . . . . . . . . . . 14
 

      |
126 | 21 | adantl 472 |
. . . . . . . . . . . . . 14
 

      |
127 | 125, 126 | sseldd 3444 |
. . . . . . . . . . . . 13
 

      |
128 | 125, 32 | sseldd 3444 |
. . . . . . . . . . . . 13
 

   
  |
129 | 127, 128 | subcld 10011 |
. . . . . . . . . . . 12
 

        |
130 | | eldifsni 4110 |
. . . . . . . . . . . . . 14
       |
131 | 130 | adantl 472 |
. . . . . . . . . . . . 13
 

      |
132 | 127, 128,
131 | subne0d 10020 |
. . . . . . . . . . . 12
 

        |
133 | 129, 132 | div0d 10409 |
. . . . . . . . . . 11
 

          |
134 | 133 | adantr 471 |
. . . . . . . . . 10
                       |
135 | 124, 134 | eqtrd 2495 |
. . . . . . . . 9
                                 |
136 | 135 | oveq2d 6330 |
. . . . . . . 8
                                     |
137 | | fveq2 5887 |
. . . . . . . . . . . 12
                           |
138 | 24, 34 | subeq0ad 10021 |
. . . . . . . . . . . 12
 

                                          |
139 | 137, 138 | syl5ibr 229 |
. . . . . . . . . . 11
 

                                  |
140 | 139 | imp 435 |
. . . . . . . . . 10
                                     |
141 | 140 | oveq1d 6329 |
. . . . . . . . 9
                                             |
142 | 141, 134 | eqtrd 2495 |
. . . . . . . 8
                                         |
143 | 118, 136,
142 | 3eqtr4d 2505 |
. . . . . . 7
                                                         |
144 | 129 | adantr 471 |
. . . . . . . 8
                     |
145 | 132 | adantr 471 |
. . . . . . . 8
                     |
146 | 36, 42, 144, 46, 145 | dmdcan2d 10440 |
. . . . . . 7
                                                                                       |
147 | 115, 117,
143, 146 | ifbothda 3927 |
. . . . . 6
 

                                                                                       |
148 | | fvco3 5964 |
. . . . . . . . 9
     
                 |
149 | 6, 21, 148 | syl2an 484 |
. . . . . . . 8
 

                    |
150 | | fvco3 5964 |
. . . . . . . . . 10
     
                 |
151 | 6, 31, 150 | syl2anc 671 |
. . . . . . . . 9
                 |
152 | 151 | adantr 471 |
. . . . . . . 8
 

                    |
153 | 149, 152 | oveq12d 6332 |
. . . . . . 7
 

                                      |
154 | 153 | oveq1d 6329 |
. . . . . 6
 

                                              |
155 | 147, 154 | eqtr4d 2498 |
. . . . 5
 

                                                                                   |
156 | 155 | mpteq2dva 4502 |
. . . 4
                                                                                            |
157 | 156 | oveq1d 6329 |
. . 3
                                                                   lim                           lim    |
158 | 113, 157 | eleqtrd 2541 |
. 2
                            lim    |
159 | | eqid 2461 |
. . 3
                                                 |
160 | | fco 5761 |
. . . 4
                   |
161 | 16, 6, 160 | syl2anc 671 |
. . 3
         |
162 | 2, 3, 159, 5, 161, 11 | eldv 22901 |
. 2
                ↾t      
                          lim      |
163 | 14, 158, 162 | mpbir2and 938 |
1
   
       |