Step | Hyp | Ref
| Expression |
1 | | cncfiooicclem1.x |
. . . 4
   |
2 | | limccl 22909 |
. . . . . . 7
 lim   |
3 | | cncfiooicclem1.r |
. . . . . . 7
  lim    |
4 | 2, 3 | sseldi 3416 |
. . . . . 6
   |
5 | 4 | ad2antrr 740 |
. . . . 5
     ![[,] [,]](_icc.gif)      |
6 | | limccl 22909 |
. . . . . . . 8
 lim   |
7 | | cncfiooicclem1.l |
. . . . . . . 8
  lim    |
8 | 6, 7 | sseldi 3416 |
. . . . . . 7
   |
9 | 8 | ad3antrrr 744 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)  

   |
10 | | simplll 776 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)  

   |
11 | | orel1 389 |
. . . . . . . . . . 11
       |
12 | 11 | con3dimp 448 |
. . . . . . . . . 10
   
   |
13 | | vex 3034 |
. . . . . . . . . . 11
 |
14 | 13 | elpr 3977 |
. . . . . . . . . 10
   
    |
15 | 12, 14 | sylnibr 312 |
. . . . . . . . 9
  
     |
16 | 15 | adantll 728 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)  


     |
17 | | simpllr 777 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)  

   ![[,] [,]](_icc.gif)    |
18 | | cncfiooicclem1.a |
. . . . . . . . . . . . 13
   |
19 | 18 | rexrd 9708 |
. . . . . . . . . . . 12
   |
20 | 10, 19 | syl 17 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)  

   |
21 | | cncfiooicclem1.b |
. . . . . . . . . . . . 13
   |
22 | 21 | rexrd 9708 |
. . . . . . . . . . . 12
   |
23 | 10, 22 | syl 17 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)  

   |
24 | | cncfiooicclem1.altb |
. . . . . . . . . . . . 13
   |
25 | 18, 21, 24 | ltled 9800 |
. . . . . . . . . . . 12

  |
26 | 10, 25 | syl 17 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)  

   |
27 | | prunioo 11787 |
. . . . . . . . . . 11
              ![[,] [,]](_icc.gif)    |
28 | 20, 23, 26, 27 | syl3anc 1292 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)  

            ![[,] [,]](_icc.gif)    |
29 | 17, 28 | eleqtrrd 2552 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)  

       
    |
30 | | elun 3565 |
. . . . . . . . 9
         
           |
31 | 29, 30 | sylib 201 |
. . . . . . . 8
   
  ![[,] [,]](_icc.gif)  

            |
32 | | orel2 390 |
. . . . . . . 8
           
 
       |
33 | 16, 31, 32 | sylc 61 |
. . . . . . 7
   
  ![[,] [,]](_icc.gif)  

       |
34 | | cncfiooicclem1.f |
. . . . . . . . 9
           |
35 | | cncff 22003 |
. . . . . . . . 9
        
          |
36 | 34, 35 | syl 17 |
. . . . . . . 8
           |
37 | 36 | ffvelrnda 6037 |
. . . . . . 7
 
    
      |
38 | 10, 33, 37 | syl2anc 673 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)  

       |
39 | 9, 38 | ifclda 3904 |
. . . . 5
     ![[,] [,]](_icc.gif)  
            |
40 | 5, 39 | ifclda 3904 |
. . . 4
 
  ![[,] [,]](_icc.gif)  
   
   
        |
41 | | cncfiooicclem1.g |
. . . 4
   ![[,] [,]](_icc.gif)                  |
42 | 1, 40, 41 | fmptdf 6063 |
. . 3
     ![[,] [,]](_icc.gif)      |
43 | | elun 3565 |
. . . . . . 7
         
           |
44 | 19, 22, 25, 27 | syl3anc 1292 |
. . . . . . . 8
       
    ![[,] [,]](_icc.gif)    |
45 | 44 | eleq2d 2534 |
. . . . . . 7
          
  ![[,] [,]](_icc.gif)     |
46 | 43, 45 | syl5bbr 267 |
. . . . . 6
          
  ![[,] [,]](_icc.gif)     |
47 | 46 | biimpar 493 |
. . . . 5
 
  ![[,] [,]](_icc.gif)  
           |
48 | | ioossicc 11745 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)   |
49 | | fssres 5761 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                   |
50 | 42, 48, 49 | sylancl 675 |
. . . . . . . . . . . 12
                 |
51 | 50 | feqmptd 5932 |
. . . . . . . . . . 11
                         |
52 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)                  |
53 | 41, 52 | nfcxfr 2610 |
. . . . . . . . . . . . . . 15
   |
54 | | nfcv 2612 |
. . . . . . . . . . . . . . 15
       |
55 | 53, 54 | nfres 5113 |
. . . . . . . . . . . . . 14
         |
56 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
57 | 55, 56 | nffv 5886 |
. . . . . . . . . . . . 13
             |
58 | | nfcv 2612 |
. . . . . . . . . . . . . 14
         |
59 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
60 | 58, 59 | nffv 5886 |
. . . . . . . . . . . . 13
             |
61 | | fveq2 5879 |
. . . . . . . . . . . . 13
                       |
62 | 57, 60, 61 | cbvmpt 4487 |
. . . . . . . . . . . 12
      
                          |
63 | 62 | a1i 11 |
. . . . . . . . . . 11
                       
           |
64 | | fvres 5893 |
. . . . . . . . . . . . . 14
                     |
65 | 64 | adantl 473 |
. . . . . . . . . . . . 13
 
    
                |
66 | | simpr 468 |
. . . . . . . . . . . . . . 15
 
    
      |
67 | 48, 66 | sseldi 3416 |
. . . . . . . . . . . . . 14
 
    
  ![[,] [,]](_icc.gif)    |
68 | 4 | adantr 472 |
. . . . . . . . . . . . . . 15
 
    
  |
69 | 8 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
           |
70 | 37 | adantr 472 |
. . . . . . . . . . . . . . . 16
       
       |
71 | 69, 70 | ifclda 3904 |
. . . . . . . . . . . . . . 15
 
    
   
       |
72 | 68, 71 | ifcld 3915 |
. . . . . . . . . . . . . 14
 
    
   
   
        |
73 | 41 | fvmpt2 5972 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)       
                  
          |
74 | 67, 72, 73 | syl2anc 673 |
. . . . . . . . . . . . 13
 
    
         
          |
75 | | elioo4g 11720 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
      |
76 | 75 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . 20
             |
77 | 76 | simpld 466 |
. . . . . . . . . . . . . . . . . . 19
     
   |
78 | 77 | simp1d 1042 |
. . . . . . . . . . . . . . . . . 18
       |
79 | | elioore 11691 |
. . . . . . . . . . . . . . . . . . 19
       |
80 | 79 | rexrd 9708 |
. . . . . . . . . . . . . . . . . 18
       |
81 | | eliooord 11719 |
. . . . . . . . . . . . . . . . . . 19
         |
82 | 81 | simpld 466 |
. . . . . . . . . . . . . . . . . 18
       |
83 | | xrltne 11483 |
. . . . . . . . . . . . . . . . . 18
     |
84 | 78, 80, 82, 83 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
       |
85 | 84 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
    
  |
86 | 85 | neneqd 2648 |
. . . . . . . . . . . . . . 15
 
    
  |
87 | 86 | iffalsed 3883 |
. . . . . . . . . . . . . 14
 
    
   
   
                 |
88 | 81 | simprd 470 |
. . . . . . . . . . . . . . . . . 18
       |
89 | 79, 88 | ltned 9788 |
. . . . . . . . . . . . . . . . 17
       |
90 | 89 | neneqd 2648 |
. . . . . . . . . . . . . . . 16
    
  |
91 | 90 | iffalsed 3883 |
. . . . . . . . . . . . . . 15
      
             |
92 | 91 | adantl 473 |
. . . . . . . . . . . . . 14
 
    
   
           |
93 | 87, 92 | eqtrd 2505 |
. . . . . . . . . . . . 13
 
    
   
   
            |
94 | 65, 74, 93 | 3eqtrd 2509 |
. . . . . . . . . . . 12
 
    
                |
95 | 1, 94 | mpteq2da 4481 |
. . . . . . . . . . 11
                             |
96 | 51, 63, 95 | 3eqtrd 2509 |
. . . . . . . . . 10
                   |
97 | 36 | feqmptd 5932 |
. . . . . . . . . . 11
             |
98 | | ioosscn 37687 |
. . . . . . . . . . . . 13
     |
99 | 98 | a1i 11 |
. . . . . . . . . . . 12
    
  |
100 | | ssid 3437 |
. . . . . . . . . . . 12
 |
101 | | eqid 2471 |
. . . . . . . . . . . . 13
  ℂfld   ℂfld |
102 | | eqid 2471 |
. . . . . . . . . . . . 13
   ℂfld ↾t         ℂfld
↾t       |
103 | 101 | cnfldtop 21882 |
. . . . . . . . . . . . . . 15
  ℂfld  |
104 | | unicntop 37433 |
. . . . . . . . . . . . . . . 16
   ℂfld |
105 | 104 | restid 15410 |
. . . . . . . . . . . . . . 15
   ℂfld    ℂfld
↾t    ℂfld  |
106 | 103, 105 | ax-mp 5 |
. . . . . . . . . . . . . 14
   ℂfld ↾t    ℂfld |
107 | 106 | eqcomi 2480 |
. . . . . . . . . . . . 13
  ℂfld    ℂfld ↾t   |
108 | 101, 102,
107 | cncfcn 22019 |
. . . . . . . . . . . 12
     
             ℂfld
↾t        ℂfld   |
109 | 99, 100, 108 | sylancl 675 |
. . . . . . . . . . 11
             ℂfld ↾t        ℂfld   |
110 | 34, 97, 109 | 3eltr3d 2563 |
. . . . . . . . . 10
               ℂfld
↾t        ℂfld   |
111 | 96, 110 | eqeltrd 2549 |
. . . . . . . . 9
           ℂfld ↾t        ℂfld   |
112 | 104 | restuni 20255 |
. . . . . . . . . . 11
    ℂfld
   
         ℂfld
↾t        |
113 | 103, 98, 112 | mp2an 686 |
. . . . . . . . . 10
        ℂfld ↾t       |
114 | 113 | cncnpi 20371 |
. . . . . . . . 9
            ℂfld ↾t        ℂfld                 ℂfld ↾t        ℂfld      |
115 | 111, 114 | sylan 479 |
. . . . . . . 8
 
    
           ℂfld ↾t        ℂfld      |
116 | 103 | a1i 11 |
. . . . . . . . . . . 12
 
    
  ℂfld   |
117 | 48 | a1i 11 |
. . . . . . . . . . . 12
 
    
      ![[,] [,]](_icc.gif)    |
118 | | ovex 6336 |
. . . . . . . . . . . . 13
  ![[,] [,]](_icc.gif)   |
119 | 118 | a1i 11 |
. . . . . . . . . . . 12
 
    
  ![[,] [,]](_icc.gif)    |
120 | | restabs 20258 |
. . . . . . . . . . . 12
    ℂfld
   
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ℂfld
↾t   ![[,] [,]](_icc.gif)   ↾t         ℂfld ↾t        |
121 | 116, 117,
119, 120 | syl3anc 1292 |
. . . . . . . . . . 11
 
    
    ℂfld
↾t   ![[,] [,]](_icc.gif)   ↾t         ℂfld ↾t        |
122 | 121 | eqcomd 2477 |
. . . . . . . . . 10
 
    
   ℂfld ↾t          ℂfld
↾t   ![[,] [,]](_icc.gif)   ↾t        |
123 | 122 | oveq1d 6323 |
. . . . . . . . 9
 
    
    ℂfld
↾t        ℂfld      ℂfld ↾t   ![[,] [,]](_icc.gif)   ↾t        ℂfld   |
124 | 123 | fveq1d 5881 |
. . . . . . . 8
 
    
     ℂfld
↾t        ℂfld          ℂfld ↾t   ![[,] [,]](_icc.gif)   ↾t        ℂfld      |
125 | 115, 124 | eleqtrd 2551 |
. . . . . . 7
 
    
            ℂfld ↾t   ![[,] [,]](_icc.gif)  
↾t        ℂfld      |
126 | | resttop 20253 |
. . . . . . . . . 10
    ℂfld
  ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)     |
127 | 103, 118,
126 | mp2an 686 |
. . . . . . . . 9
   ℂfld ↾t   ![[,] [,]](_icc.gif)    |
128 | 127 | a1i 11 |
. . . . . . . 8
 
    
   ℂfld ↾t   ![[,] [,]](_icc.gif)     |
129 | 48 | a1i 11 |
. . . . . . . . . 10
    
  ![[,] [,]](_icc.gif)    |
130 | 18, 21 | iccssred 37698 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif) 
  |
131 | | ax-resscn 9614 |
. . . . . . . . . . . 12
 |
132 | 130, 131 | syl6ss 3430 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
  |
133 | 104 | restuni 20255 |
. . . . . . . . . . 11
    ℂfld
  ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)     |
134 | 103, 132,
133 | sylancr 676 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)     |
135 | 129, 134 | sseqtrd 3454 |
. . . . . . . . 9
    
    ℂfld
↾t   ![[,] [,]](_icc.gif)     |
136 | 135 | adantr 472 |
. . . . . . . 8
 
    
        ℂfld
↾t   ![[,] [,]](_icc.gif)     |
137 | | retop 21860 |
. . . . . . . . . . . . . 14
     |
138 | 137 | a1i 11 |
. . . . . . . . . . . . 13
 
    
      |
139 | | ioossre 11721 |
. . . . . . . . . . . . . . 15
     |
140 | | difss 3549 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
141 | 139, 140 | unssi 3600 |
. . . . . . . . . . . . . 14
        ![[,] [,]](_icc.gif)     |
142 | 141 | a1i 11 |
. . . . . . . . . . . . 13
 
    
        ![[,] [,]](_icc.gif)   
  |
143 | | ssun1 3588 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)     |
144 | 143 | a1i 11 |
. . . . . . . . . . . . 13
 
    
            ![[,] [,]](_icc.gif)      |
145 | | uniretop 21861 |
. . . . . . . . . . . . . 14
      |
146 | 145 | ntrss 20147 |
. . . . . . . . . . . . 13
              ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)    
                                   ![[,] [,]](_icc.gif)       |
147 | 138, 142,
144, 146 | syl3anc 1292 |
. . . . . . . . . . . 12
 
    
                                   ![[,] [,]](_icc.gif)       |
148 | | simpr 468 |
. . . . . . . . . . . . 13
 
    
      |
149 | | ioontr 37707 |
. . . . . . . . . . . . 13
                     |
150 | 148, 149 | syl6eleqr 2560 |
. . . . . . . . . . . 12
 
    
      
           |
151 | 147, 150 | sseldd 3419 |
. . . . . . . . . . 11
 
    
      
            ![[,] [,]](_icc.gif)       |
152 | 48, 148 | sseldi 3416 |
. . . . . . . . . . 11
 
    
  ![[,] [,]](_icc.gif)    |
153 | 151, 152 | elind 3609 |
. . . . . . . . . 10
 
    
                    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
154 | 130 | adantr 472 |
. . . . . . . . . . 11
 
    
  ![[,] [,]](_icc.gif)    |
155 | | eqid 2471 |
. . . . . . . . . . . 12
     ↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)    |
156 | 145, 155 | restntr 20275 |
. . . . . . . . . . 11
        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)            ↾t   ![[,] [,]](_icc.gif)                  
            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
157 | 138, 154,
117, 156 | syl3anc 1292 |
. . . . . . . . . 10
 
    
        
↾t   ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
158 | 153, 157 | eleqtrrd 2552 |
. . . . . . . . 9
 
    
         ↾t   ![[,] [,]](_icc.gif)             |
159 | 101 | tgioo2 21899 |
. . . . . . . . . . . . . . 15
       ℂfld
↾t   |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . 14
        ℂfld ↾t    |
161 | 160 | oveq1d 6323 |
. . . . . . . . . . . . 13
      ↾t   ![[,] [,]](_icc.gif)       ℂfld
↾t 
↾t   ![[,] [,]](_icc.gif)     |
162 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
   ℂfld
  |
163 | | reex 9648 |
. . . . . . . . . . . . . . 15
 |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
   |
165 | | restabs 20258 |
. . . . . . . . . . . . . 14
    ℂfld
  ![[,] [,]](_icc.gif) 
     ℂfld
↾t 
↾t   ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)     |
166 | 162, 130,
164, 165 | syl3anc 1292 |
. . . . . . . . . . . . 13
     ℂfld ↾t  ↾t   ![[,] [,]](_icc.gif)      ℂfld ↾t   ![[,] [,]](_icc.gif)     |
167 | 161, 166 | eqtrd 2505 |
. . . . . . . . . . . 12
      ↾t   ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)     |
168 | 167 | fveq2d 5883 |
. . . . . . . . . . 11
         ↾t   ![[,] [,]](_icc.gif)          ℂfld
↾t   ![[,] [,]](_icc.gif)      |
169 | 168 | fveq1d 5881 |
. . . . . . . . . 10
          ↾t   ![[,] [,]](_icc.gif)                  ℂfld
↾t   ![[,] [,]](_icc.gif)             |
170 | 169 | adantr 472 |
. . . . . . . . 9
 
    
        
↾t   ![[,] [,]](_icc.gif)                  ℂfld
↾t   ![[,] [,]](_icc.gif)             |
171 | 158, 170 | eleqtrd 2551 |
. . . . . . . 8
 
    
       ℂfld
↾t   ![[,] [,]](_icc.gif)             |
172 | 134 | feq2d 5725 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)          ℂfld
↾t   ![[,] [,]](_icc.gif)        |
173 | 42, 172 | mpbid 215 |
. . . . . . . . 9
       ℂfld
↾t   ![[,] [,]](_icc.gif)       |
174 | 173 | adantr 472 |
. . . . . . . 8
 
    
      ℂfld
↾t   ![[,] [,]](_icc.gif)       |
175 | | eqid 2471 |
. . . . . . . . 9
    ℂfld
↾t   ![[,] [,]](_icc.gif)       ℂfld ↾t   ![[,] [,]](_icc.gif)    |
176 | 175, 104 | cnprest 20382 |
. . . . . . . 8
      ℂfld ↾t   ![[,] [,]](_icc.gif)           ℂfld
↾t   ![[,] [,]](_icc.gif)            ℂfld
↾t   ![[,] [,]](_icc.gif)                 ℂfld ↾t   ![[,] [,]](_icc.gif)      
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld                ℂfld ↾t   ![[,] [,]](_icc.gif)   ↾t        ℂfld       |
177 | 128, 136,
171, 174, 176 | syl22anc 1293 |
. . . . . . 7
 
    
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld                ℂfld ↾t   ![[,] [,]](_icc.gif)   ↾t        ℂfld       |
178 | 125, 177 | mpbird 240 |
. . . . . 6
 
    
     ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld      |
179 | | elpri 3976 |
. . . . . . 7
   
    |
180 | | lbicc2 11774 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)    |
181 | 19, 22, 25, 180 | syl3anc 1292 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)    |
182 | | iftrue 3878 |
. . . . . . . . . . . . . 14
  
     
        |
183 | 182, 41 | fvmptg 5961 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 
 lim         |
184 | 181, 3, 183 | syl2anc 673 |
. . . . . . . . . . . 12
       |
185 | 97 | eqcomd 2477 |
. . . . . . . . . . . . . . . 16
             |
186 | 96, 185 | eqtr2d 2506 |
. . . . . . . . . . . . . . 15
         |
187 | 186 | oveq1d 6323 |
. . . . . . . . . . . . . 14
  lim   
     lim    |
188 | 3, 187 | eleqtrd 2551 |
. . . . . . . . . . . . 13
  
     lim    |
189 | 18, 21, 24, 42 | limciccioolb 37798 |
. . . . . . . . . . . . 13
        lim   lim    |
190 | 188, 189 | eleqtrd 2551 |
. . . . . . . . . . . 12
  lim    |
191 | 184, 190 | eqeltrd 2549 |
. . . . . . . . . . 11
      lim    |
192 | | eqid 2471 |
. . . . . . . . . . . . 13
   ℂfld ↾t   ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)    |
193 | 101, 192 | cnplimc 22921 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)   
     ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld         ![[,] [,]](_icc.gif)         lim      |
194 | 132, 181,
193 | syl2anc 673 |
. . . . . . . . . . 11
       ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ![[,] [,]](_icc.gif)         lim      |
195 | 42, 191, 194 | mpbir2and 936 |
. . . . . . . . . 10
      ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
196 | 195 | adantr 472 |
. . . . . . . . 9
 
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld      |
197 | | fveq2 5879 |
. . . . . . . . . . 11
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
198 | 197 | eqcomd 2477 |
. . . . . . . . . 10
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
199 | 198 | adantl 473 |
. . . . . . . . 9
 
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
200 | 196, 199 | eleqtrd 2551 |
. . . . . . . 8
 
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld      |
201 | 21 | leidd 10201 |
. . . . . . . . . . . . . . 15

  |
202 | 18, 21, 21, 25, 201 | eliccd 37697 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)    |
203 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
 |
204 | 203 | iftruei 3879 |
. . . . . . . . . . . . . . . . 17
   
      |
205 | 204, 8 | syl5eqel 2553 |
. . . . . . . . . . . . . . . 16
            |
206 | 4, 205 | ifcld 3915 |
. . . . . . . . . . . . . . 15
                 |
207 | 202, 206 | jca 541 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)                   |
208 | | nfv 1769 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)                  |
209 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . 18
   |
210 | 53, 209 | nffv 5886 |
. . . . . . . . . . . . . . . . 17
       |
211 | 210 | nfeq1 2625 |
. . . . . . . . . . . . . . . 16
         
 
 
       |
212 | 208, 211 | nfim 2023 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
 
 
 
 
              
 
 
        |
213 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
214 | 182 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
 
                 |
215 | | eqtr2 2491 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
216 | | iftrue 3878 |
. . . . . . . . . . . . . . . . . . . . . 22
  
     
        |
217 | 216 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
218 | 215, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
    
 
 
        |
219 | 214, 218 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
 
                    
          |
220 | | iffalse 3881 |
. . . . . . . . . . . . . . . . . . . . 21
      
           
       |
221 | 220 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
 

   
   
                 |
222 | | iftrue 3878 |
. . . . . . . . . . . . . . . . . . . . 21
  
         |
223 | 222 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 

   
       |
224 | | df-ne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
225 | | pm13.18 2724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
226 | 224, 225 | sylan2br 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
227 | 226 | neneqd 2648 |
. . . . . . . . . . . . . . . . . . . . . 22
 

  |
228 | 227 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . . . . 21
 

 
 
 
 
                 |
229 | 228, 204 | syl6req 2522 |
. . . . . . . . . . . . . . . . . . . 20
 

     
          |
230 | 221, 223,
229 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . 19
 

   
   
                      |
231 | 219, 230 | pm2.61dan 808 |
. . . . . . . . . . . . . . . . . 18
  
     
                      |
232 | 231 | eleq1d 2533 |
. . . . . . . . . . . . . . . . 17
       
       
 
 
 
 
         |
233 | 213, 232 | anbi12d 725 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif) 
 
 
 
 
          |
234 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
           |
235 | 234, 231 | eqeq12d 2486 |
. . . . . . . . . . . . . . . 16
         
   
             
 
 
         |
236 | 233, 235 | imbi12d 327 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
   
   
              
   
           ![[,] [,]](_icc.gif)   
     
              
 
 
          |
237 | 212, 236,
73 | vtoclg1f 3092 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                                      |
238 | 202, 207,
237 | sylc 61 |
. . . . . . . . . . . . 13
        
 
 
        |
239 | 18, 24 | gtned 9787 |
. . . . . . . . . . . . . . 15
   |
240 | 239 | neneqd 2648 |
. . . . . . . . . . . . . 14
   |
241 | 240 | iffalsed 3883 |
. . . . . . . . . . . . 13
                          |
242 | 204 | a1i 11 |
. . . . . . . . . . . . 13
            |
243 | 238, 241,
242 | 3eqtrd 2509 |
. . . . . . . . . . . 12
       |
244 | 186 | oveq1d 6323 |
. . . . . . . . . . . . . 14
  lim   
     lim    |
245 | 7, 244 | eleqtrd 2551 |
. . . . . . . . . . . . 13
  
     lim    |
246 | 18, 21, 24, 42 | limcicciooub 37814 |
. . . . . . . . . . . . 13
        lim   lim    |
247 | 245, 246 | eleqtrd 2551 |
. . . . . . . . . . . 12
  lim    |
248 | 243, 247 | eqeltrd 2549 |
. . . . . . . . . . 11
      lim    |
249 | 101, 192 | cnplimc 22921 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)   
     ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld         ![[,] [,]](_icc.gif)         lim      |
250 | 132, 202,
249 | syl2anc 673 |
. . . . . . . . . . 11
       ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ![[,] [,]](_icc.gif)         lim      |
251 | 42, 248, 250 | mpbir2and 936 |
. . . . . . . . . 10
      ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
252 | 251 | adantr 472 |
. . . . . . . . 9
 
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld      |
253 | | fveq2 5879 |
. . . . . . . . . . 11
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
254 | 253 | eqcomd 2477 |
. . . . . . . . . 10
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
255 | 254 | adantl 473 |
. . . . . . . . 9
 
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld         ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
256 | 252, 255 | eleqtrd 2551 |
. . . . . . . 8
 
      ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld      |
257 | 200, 256 | jaodan 802 |
. . . . . . 7
 

 
     ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
258 | 179, 257 | sylan2 482 |
. . . . . 6
 
   
     ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld      |
259 | 178, 258 | jaodan 802 |
. . . . 5
 
         
     ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
260 | 47, 259 | syldan 478 |
. . . 4
 
  ![[,] [,]](_icc.gif)  
     ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld      |
261 | 260 | ralrimiva 2809 |
. . 3
    ![[,] [,]](_icc.gif)        ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld      |
262 | 101 | cnfldtopon 21881 |
. . . . 5
  ℂfld TopOn   |
263 | | resttopon 20254 |
. . . . 5
    ℂfld
TopOn    ![[,] [,]](_icc.gif)  
   ℂfld ↾t   ![[,] [,]](_icc.gif)   TopOn   ![[,] [,]](_icc.gif)     |
264 | 262, 132,
263 | sylancr 676 |
. . . 4
    ℂfld
↾t   ![[,] [,]](_icc.gif)   TopOn   ![[,] [,]](_icc.gif)     |
265 | | cncnp 20373 |
. . . 4
     ℂfld
↾t   ![[,] [,]](_icc.gif)   TopOn   ![[,] [,]](_icc.gif)     ℂfld
TopOn        ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld        |
266 | 264, 262,
265 | sylancl 675 |
. . 3
      ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld        |
267 | 42, 261, 266 | mpbir2and 936 |
. 2
     ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld   |
268 | 101, 192,
107 | cncfcn 22019 |
. . 3
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)         ℂfld
↾t   ![[,] [,]](_icc.gif)     ℂfld   |
269 | 132, 100,
268 | sylancl 675 |
. 2
    ![[,] [,]](_icc.gif)         ℂfld ↾t   ![[,] [,]](_icc.gif)     ℂfld   |
270 | 267, 269 | eleqtrrd 2552 |
1
    ![[,] [,]](_icc.gif)       |