Step | Hyp | Ref
| Expression |
1 | | limcresiooub.d |
. . . . . 6
   |
2 | | limcresiooub.cled |
. . . . . 6

  |
3 | | iooss1 11696 |
. . . . . 6
             |
4 | 1, 2, 3 | syl2anc 673 |
. . . . 5
    
      |
5 | 4 | resabs1d 5140 |
. . . 4
       
             |
6 | 5 | eqcomd 2477 |
. . 3
                     |
7 | 6 | oveq1d 6323 |
. 2
        lim    
          lim    |
8 | | limcresiooub.f |
. . . 4
       |
9 | | fresin 5764 |
. . . 4
     
                 |
10 | 8, 9 | syl 17 |
. . 3
                   |
11 | | limcresiooub.bcss |
. . . 4
    
  |
12 | 11, 4 | ssind 3647 |
. . 3
    
        |
13 | | inss2 3644 |
. . . . 5
           |
14 | | ioosscn 37687 |
. . . . 5
     |
15 | 13, 14 | sstri 3427 |
. . . 4
       |
16 | 15 | a1i 11 |
. . 3
         |
17 | | eqid 2471 |
. . 3
  ℂfld   ℂfld |
18 | | eqid 2471 |
. . 3
   ℂfld ↾t               ℂfld
↾t             |
19 | | limcresiooub.b |
. . . . 5
   |
20 | | limcresiooub.c |
. . . . . 6
   |
21 | 20 | rexrd 9708 |
. . . . 5
   |
22 | | limcresiooub.bltc |
. . . . 5
   |
23 | | ubioc1 11713 |
. . . . 5
     ![(,] (,]](_ioc.gif)    |
24 | 19, 21, 22, 23 | syl3anc 1292 |
. . . 4
   ![(,] (,]](_ioc.gif)    |
25 | | snunioo2 37702 |
. . . . . . 7
             ![(,] (,]](_ioc.gif)    |
26 | 19, 21, 22, 25 | syl3anc 1292 |
. . . . . 6
           ![(,] (,]](_ioc.gif)    |
27 | 26 | fveq2d 5883 |
. . . . 5
        ℂfld
↾t                               ℂfld
↾t                 ![(,] (,]](_ioc.gif)     |
28 | 17 | cnfldtop 21882 |
. . . . . . . 8
  ℂfld  |
29 | | ovex 6336 |
. . . . . . . . . 10
     |
30 | 29 | inex2 4538 |
. . . . . . . . 9
       |
31 | | snex 4641 |
. . . . . . . . 9
 
 |
32 | 30, 31 | unex 6608 |
. . . . . . . 8
           |
33 | | resttop 20253 |
. . . . . . . 8
    ℂfld
              ℂfld ↾t              |
34 | 28, 32, 33 | mp2an 686 |
. . . . . . 7
   ℂfld ↾t             |
35 | 34 | a1i 11 |
. . . . . 6
    ℂfld
↾t              |
36 | | pnfxr 11435 |
. . . . . . . . . . . . . 14
 |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
   |
38 | | xrleid 11472 |
. . . . . . . . . . . . . 14

  |
39 | 19, 38 | syl 17 |
. . . . . . . . . . . . 13

  |
40 | 20 | ltpnfd 11446 |
. . . . . . . . . . . . 13
   |
41 | | iocssioo 11749 |
. . . . . . . . . . . . 13
         ![(,] (,]](_ioc.gif) 
     |
42 | 19, 37, 39, 40, 41 | syl22anc 1293 |
. . . . . . . . . . . 12
   ![(,] (,]](_ioc.gif) 
     |
43 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
 
   |
44 | | snidg 3986 |
. . . . . . . . . . . . . . . . . . 19
     |
45 | | elun2 3593 |
. . . . . . . . . . . . . . . . . . 19
               |
46 | 20, 44, 45 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
             |
47 | 46 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
             |
48 | 43, 47 | eqeltrd 2549 |
. . . . . . . . . . . . . . . 16
 
             |
49 | 48 | adantlr 729 |
. . . . . . . . . . . . . . 15
     ![(,] (,]](_ioc.gif)                |
50 | | simpll 768 |
. . . . . . . . . . . . . . . 16
     ![(,] (,]](_ioc.gif)  
   |
51 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
  ![(,] (,]](_ioc.gif)  
  |
52 | 51 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     ![(,] (,]](_ioc.gif)  
   |
53 | 21 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
  ![(,] (,]](_ioc.gif)  
  |
54 | 53 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     ![(,] (,]](_ioc.gif)  
   |
55 | | iocssre 11739 |
. . . . . . . . . . . . . . . . . . . 20
     ![(,] (,]](_ioc.gif)    |
56 | 19, 20, 55 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
   ![(,] (,]](_ioc.gif) 
  |
57 | 56 | sselda 3418 |
. . . . . . . . . . . . . . . . . 18
 
  ![(,] (,]](_ioc.gif)  
  |
58 | 57 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     ![(,] (,]](_ioc.gif)  
   |
59 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
 
  ![(,] (,]](_ioc.gif)  
  ![(,] (,]](_ioc.gif)    |
60 | | iocgtlb 37695 |
. . . . . . . . . . . . . . . . . . 19
    ![(,] (,]](_ioc.gif)     |
61 | 51, 53, 59, 60 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
 
  ![(,] (,]](_ioc.gif)  
  |
62 | 61 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     ![(,] (,]](_ioc.gif)  
   |
63 | 20 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
     ![(,] (,]](_ioc.gif)  
   |
64 | | iocleub 37696 |
. . . . . . . . . . . . . . . . . . . 20
    ![(,] (,]](_ioc.gif)     |
65 | 51, 53, 59, 64 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . 19
 
  ![(,] (,]](_ioc.gif)  
  |
66 | 65 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
     ![(,] (,]](_ioc.gif)  

  |
67 | | neqne 2651 |
. . . . . . . . . . . . . . . . . . . 20
   |
68 | 67 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
     ![(,] (,]](_ioc.gif)  
   |
69 | 68 | necomd 2698 |
. . . . . . . . . . . . . . . . . 18
     ![(,] (,]](_ioc.gif)  
   |
70 | 58, 63, 66, 69 | leneltd 9806 |
. . . . . . . . . . . . . . . . 17
     ![(,] (,]](_ioc.gif)  
   |
71 | 52, 54, 58, 62, 70 | eliood 37691 |
. . . . . . . . . . . . . . . 16
     ![(,] (,]](_ioc.gif)  
       |
72 | 12 | sselda 3418 |
. . . . . . . . . . . . . . . . 17
 
    

       |
73 | | elun1 3592 |
. . . . . . . . . . . . . . . . 17
      
            |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
            |
75 | 50, 71, 74 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     ![(,] (,]](_ioc.gif)  
             |
76 | 49, 75 | pm2.61dan 808 |
. . . . . . . . . . . . . 14
 
  ![(,] (,]](_ioc.gif)  
            |
77 | 76 | ralrimiva 2809 |
. . . . . . . . . . . . 13
    ![(,] (,]](_ioc.gif)               |
78 | | dfss3 3408 |
. . . . . . . . . . . . 13
   ![(,] (,]](_ioc.gif)            
  ![(,] (,]](_ioc.gif)               |
79 | 77, 78 | sylibr 217 |
. . . . . . . . . . . 12
   ![(,] (,]](_ioc.gif) 
            |
80 | 42, 79 | ssind 3647 |
. . . . . . . . . . 11
   ![(,] (,]](_ioc.gif) 
                 |
81 | 80 | sseld 3417 |
. . . . . . . . . 10
    ![(,] (,]](_ioc.gif)                    |
82 | 24 | adantr 472 |
. . . . . . . . . . . . . 14
 
   ![(,] (,]](_ioc.gif)    |
83 | 43, 82 | eqeltrd 2549 |
. . . . . . . . . . . . 13
 
   ![(,] (,]](_ioc.gif)    |
84 | 83 | adantlr 729 |
. . . . . . . . . . . 12
                  
   ![(,] (,]](_ioc.gif)    |
85 | | ioossioc 37684 |
. . . . . . . . . . . . 13
      ![(,] (,]](_ioc.gif)   |
86 | 19 | ad2antrr 740 |
. . . . . . . . . . . . . 14
                  

  |
87 | 21 | ad2antrr 740 |
. . . . . . . . . . . . . 14
                  

  |
88 | | elinel1 3610 |
. . . . . . . . . . . . . . . 16
               
     |
89 | | elioore 11691 |
. . . . . . . . . . . . . . . 16
   
  |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . 15
               
  |
91 | 90 | ad2antlr 741 |
. . . . . . . . . . . . . 14
                  

  |
92 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
                  

  |
93 | 88 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
                  

     |
94 | | ioogtlb 37688 |
. . . . . . . . . . . . . . 15
        |
95 | 86, 92, 93, 94 | syl3anc 1292 |
. . . . . . . . . . . . . 14
                  

  |
96 | 1 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
                  

  |
97 | | elinel2 3611 |
. . . . . . . . . . . . . . . . . 18
               
            |
98 | | id 22 |
. . . . . . . . . . . . . . . . . . 19

  |
99 | | elsn 3973 |
. . . . . . . . . . . . . . . . . . 19
     |
100 | 98, 99 | sylnibr 312 |
. . . . . . . . . . . . . . . . . 18

    |
101 | | elunnel2 37423 |
. . . . . . . . . . . . . . . . . 18
           
           |
102 | 97, 100, 101 | syl2an 485 |
. . . . . . . . . . . . . . . . 17
                


       |
103 | 13, 102 | sseldi 3416 |
. . . . . . . . . . . . . . . 16
                

      |
104 | 103 | adantll 728 |
. . . . . . . . . . . . . . 15
                  

      |
105 | | iooltub 37706 |
. . . . . . . . . . . . . . 15
         |
106 | 96, 87, 104, 105 | syl3anc 1292 |
. . . . . . . . . . . . . 14
                  

  |
107 | 86, 87, 91, 95, 106 | eliood 37691 |
. . . . . . . . . . . . 13
                  

      |
108 | 85, 107 | sseldi 3416 |
. . . . . . . . . . . 12
                  

  ![(,] (,]](_ioc.gif)    |
109 | 84, 108 | pm2.61dan 808 |
. . . . . . . . . . 11
 
               
  ![(,] (,]](_ioc.gif)    |
110 | 109 | ex 441 |
. . . . . . . . . 10
                
  ![(,] (,]](_ioc.gif)     |
111 | 81, 110 | impbid 195 |
. . . . . . . . 9
    ![(,] (,]](_ioc.gif)                    |
112 | 111 | eqrdv 2469 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)                   |
113 | | retop 21860 |
. . . . . . . . . 10
     |
114 | 113 | a1i 11 |
. . . . . . . . 9
       |
115 | 32 | a1i 11 |
. . . . . . . . 9
             |
116 | | iooretop 21864 |
. . . . . . . . . 10
        |
117 | 116 | a1i 11 |
. . . . . . . . 9
   
      |
118 | | elrestr 15405 |
. . . . . . . . 9
                       
                    ↾t              |
119 | 114, 115,
117, 118 | syl3anc 1292 |
. . . . . . . 8
                     ↾t              |
120 | 112, 119 | eqeltrd 2549 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)       ↾t              |
121 | 17 | tgioo2 21899 |
. . . . . . . . 9
       ℂfld
↾t   |
122 | 121 | oveq1i 6318 |
. . . . . . . 8
     ↾t                ℂfld
↾t 
↾t             |
123 | 28 | a1i 11 |
. . . . . . . . 9
   ℂfld
  |
124 | | ioossre 11721 |
. . . . . . . . . . . 12
     |
125 | 13, 124 | sstri 3427 |
. . . . . . . . . . 11
       |
126 | 125 | a1i 11 |
. . . . . . . . . 10
         |
127 | 20 | snssd 4108 |
. . . . . . . . . 10
     |
128 | 126, 127 | unssd 3601 |
. . . . . . . . 9
             |
129 | | reex 9648 |
. . . . . . . . . 10
 |
130 | 129 | a1i 11 |
. . . . . . . . 9
   |
131 | | restabs 20258 |
. . . . . . . . 9
    ℂfld
               ℂfld ↾t  ↾t               ℂfld
↾t              |
132 | 123, 128,
130, 131 | syl3anc 1292 |
. . . . . . . 8
     ℂfld ↾t  ↾t               ℂfld
↾t              |
133 | 122, 132 | syl5eq 2517 |
. . . . . . 7
      ↾t               ℂfld
↾t              |
134 | 120, 133 | eleqtrd 2551 |
. . . . . 6
   ![(,] (,]](_ioc.gif)     ℂfld ↾t              |
135 | | isopn3i 20175 |
. . . . . 6
     ℂfld
↾t              ![(,] (,]](_ioc.gif)     ℂfld ↾t                    ℂfld
↾t                 ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)    |
136 | 35, 134, 135 | syl2anc 673 |
. . . . 5
        ℂfld
↾t                 ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)    |
137 | 27, 136 | eqtr2d 2506 |
. . . 4
   ![(,] (,]](_ioc.gif)         ℂfld ↾t                          |
138 | 24, 137 | eleqtrd 2551 |
. . 3
        ℂfld ↾t                          |
139 | 10, 12, 16, 17, 18, 138 | limcres 22920 |
. 2
              lim         lim    |
140 | 7, 139 | eqtrd 2505 |
1
        lim         lim    |