Step | Hyp | Ref
| Expression |
1 | | limciccioolb.4 |
. 2
     ![[,] [,]](_icc.gif)      |
2 | | ioossicc 11745 |
. . 3
      ![[,] [,]](_icc.gif)   |
3 | 2 | a1i 11 |
. 2
    
  ![[,] [,]](_icc.gif)    |
4 | | limciccioolb.1 |
. . . 4
   |
5 | | limciccioolb.2 |
. . . 4
   |
6 | 4, 5 | iccssred 37698 |
. . 3
   ![[,] [,]](_icc.gif) 
  |
7 | | ax-resscn 9614 |
. . 3
 |
8 | 6, 7 | syl6ss 3430 |
. 2
   ![[,] [,]](_icc.gif) 
  |
9 | | eqid 2471 |
. 2
  ℂfld   ℂfld |
10 | | eqid 2471 |
. 2
   ℂfld ↾t    ![[,] [,]](_icc.gif)         ℂfld
↾t    ![[,] [,]](_icc.gif)       |
11 | | retop 21860 |
. . . . . . . . 9
     |
12 | 11 | a1i 11 |
. . . . . . . 8
       |
13 | 5 | rexrd 9708 |
. . . . . . . . . . 11
   |
14 | | icossre 11740 |
. . . . . . . . . . 11
 
    
  |
15 | 4, 13, 14 | syl2anc 673 |
. . . . . . . . . 10
    
  |
16 | | difssd 3550 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)     |
17 | 15, 16 | unssd 3601 |
. . . . . . . . 9
         ![[,] [,]](_icc.gif)      |
18 | | uniretop 21861 |
. . . . . . . . 9
      |
19 | 17, 18 | syl6sseq 3464 |
. . . . . . . 8
         ![[,] [,]](_icc.gif)           |
20 | | elioore 11691 |
. . . . . . . . . . . . . . 15
      |
21 | 20 | ad2antlr 741 |
. . . . . . . . . . . . . 14
  
       |
22 | | simpr 468 |
. . . . . . . . . . . . . 14
  
       |
23 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
 
   
     |
24 | | mnfxr 11437 |
. . . . . . . . . . . . . . . . . . 19
 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
   
  |
26 | 13 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
   
  |
27 | | elioo2 11702 |
. . . . . . . . . . . . . . . . . 18
     
     |
28 | 25, 26, 27 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
   

        |
29 | 23, 28 | mpbid 215 |
. . . . . . . . . . . . . . . 16
 
   
    |
30 | 29 | simp3d 1044 |
. . . . . . . . . . . . . . 15
 
   
  |
31 | 30 | adantr 472 |
. . . . . . . . . . . . . 14
  
       |
32 | 4 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
  
       |
33 | 13 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
  
       |
34 | | elico2 11723 |
. . . . . . . . . . . . . . 15
 
      
    |
35 | 32, 33, 34 | syl2anc 673 |
. . . . . . . . . . . . . 14
  
         
     |
36 | 21, 22, 31, 35 | mpbir3and 1213 |
. . . . . . . . . . . . 13
  
           |
37 | 36 | orcd 399 |
. . . . . . . . . . . 12
  
             ![[,] [,]](_icc.gif)      |
38 | 20 | ad2antlr 741 |
. . . . . . . . . . . . . 14
  
    
  |
39 | | simpr 468 |
. . . . . . . . . . . . . . . 16
  
    
  |
40 | 39 | intnanrd 931 |
. . . . . . . . . . . . . . 15
  
     
   |
41 | 4 | rexrd 9708 |
. . . . . . . . . . . . . . . . 17
   |
42 | 41 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
  
    
  |
43 | 13 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
  
    
  |
44 | 38 | rexrd 9708 |
. . . . . . . . . . . . . . . 16
  
    
  |
45 | | elicc4 11726 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif) 
     |
46 | 42, 43, 44, 45 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
  
        ![[,] [,]](_icc.gif)  
    |
47 | 40, 46 | mtbird 308 |
. . . . . . . . . . . . . 14
  
    
  ![[,] [,]](_icc.gif)    |
48 | 38, 47 | eldifd 3401 |
. . . . . . . . . . . . 13
  
    
   ![[,] [,]](_icc.gif)     |
49 | 48 | olcd 400 |
. . . . . . . . . . . 12
  
             ![[,] [,]](_icc.gif)      |
50 | 37, 49 | pm2.61dan 808 |
. . . . . . . . . . 11
 
   
        ![[,] [,]](_icc.gif)      |
51 | | elun 3565 |
. . . . . . . . . . 11
         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      |
52 | 50, 51 | sylibr 217 |
. . . . . . . . . 10
 
   
        ![[,] [,]](_icc.gif)      |
53 | 52 | ralrimiva 2809 |
. . . . . . . . 9
              ![[,] [,]](_icc.gif)      |
54 | | dfss3 3408 |
. . . . . . . . 9
            ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)      |
55 | 53, 54 | sylibr 217 |
. . . . . . . 8
   
        ![[,] [,]](_icc.gif)      |
56 | | eqid 2471 |
. . . . . . . . 9
   
       |
57 | 56 | ntrss 20147 |
. . . . . . . 8
              ![[,] [,]](_icc.gif)        
  
        ![[,] [,]](_icc.gif)           
              
            ![[,] [,]](_icc.gif)       |
58 | 12, 19, 55, 57 | syl3anc 1292 |
. . . . . . 7
       
              
            ![[,] [,]](_icc.gif)       |
59 | 24 | a1i 11 |
. . . . . . . . 9
   |
60 | 4 | mnfltd 11449 |
. . . . . . . . 9

  |
61 | | limciccioolb.3 |
. . . . . . . . 9
   |
62 | 59, 13, 4, 60, 61 | eliood 37691 |
. . . . . . . 8
      |
63 | | iooretop 21864 |
. . . . . . . . . 10
        |
64 | 63 | a1i 11 |
. . . . . . . . 9
          |
65 | | isopn3i 20175 |
. . . . . . . . 9
             
                    |
66 | 12, 64, 65 | syl2anc 673 |
. . . . . . . 8
       
             |
67 | 62, 66 | eleqtrrd 2552 |
. . . . . . 7
                  |
68 | 58, 67 | sseldd 3419 |
. . . . . 6
                    ![[,] [,]](_icc.gif)       |
69 | 4 | leidd 10201 |
. . . . . . 7

  |
70 | 4, 5, 61 | ltled 9800 |
. . . . . . 7

  |
71 | 4, 5, 4, 69, 70 | eliccd 37697 |
. . . . . 6
   ![[,] [,]](_icc.gif)    |
72 | 68, 71 | elind 3609 |
. . . . 5
        
            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
73 | | icossicc 11746 |
. . . . . . 7
      ![[,] [,]](_icc.gif)   |
74 | 73 | a1i 11 |
. . . . . 6
    
  ![[,] [,]](_icc.gif)    |
75 | | eqid 2471 |
. . . . . . 7
     ↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)    |
76 | 18, 75 | restntr 20275 |
. . . . . 6
        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)            ↾t   ![[,] [,]](_icc.gif)                  
            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
77 | 12, 6, 74, 76 | syl3anc 1292 |
. . . . 5
          ↾t   ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
78 | 72, 77 | eleqtrrd 2552 |
. . . 4
          ↾t   ![[,] [,]](_icc.gif)             |
79 | | eqid 2471 |
. . . . . . . . 9
         |
80 | 9, 79 | rerest 21900 |
. . . . . . . 8
   ![[,] [,]](_icc.gif) 
   ℂfld ↾t   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)     |
81 | 6, 80 | syl 17 |
. . . . . . 7
    ℂfld
↾t   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)     |
82 | 81 | eqcomd 2477 |
. . . . . 6
      ↾t   ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)     |
83 | 82 | fveq2d 5883 |
. . . . 5
         ↾t   ![[,] [,]](_icc.gif)          ℂfld
↾t   ![[,] [,]](_icc.gif)      |
84 | 83 | fveq1d 5881 |
. . . 4
          ↾t   ![[,] [,]](_icc.gif)                  ℂfld
↾t   ![[,] [,]](_icc.gif)             |
85 | 78, 84 | eleqtrd 2551 |
. . 3
        ℂfld ↾t   ![[,] [,]](_icc.gif)             |
86 | 71 | snssd 4108 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    |
87 | | ssequn2 3598 |
. . . . . . . 8
     ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
88 | 86, 87 | sylib 201 |
. . . . . . 7
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
89 | 88 | eqcomd 2477 |
. . . . . 6
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       |
90 | 89 | oveq2d 6324 |
. . . . 5
    ℂfld
↾t   ![[,] [,]](_icc.gif)      ℂfld
↾t    ![[,] [,]](_icc.gif)        |
91 | 90 | fveq2d 5883 |
. . . 4
       ℂfld
↾t   ![[,] [,]](_icc.gif)          ℂfld
↾t    ![[,] [,]](_icc.gif)         |
92 | | uncom 3569 |
. . . . 5
                 |
93 | | snunioo 11784 |
. . . . . 6
                 |
94 | 41, 13, 61, 93 | syl3anc 1292 |
. . . . 5
               |
95 | 92, 94 | syl5req 2518 |
. . . 4
               |
96 | 91, 95 | fveq12d 5885 |
. . 3
        ℂfld
↾t   ![[,] [,]](_icc.gif)                  ℂfld
↾t    ![[,] [,]](_icc.gif)                    |
97 | 85, 96 | eleqtrd 2551 |
. 2
        ℂfld ↾t    ![[,] [,]](_icc.gif)                    |
98 | 1, 3, 8, 9, 10, 97 | limcres 22920 |
1
        lim   lim    |