Step | Hyp | Ref
| Expression |
1 | | limcicciooub.4 |
. 2
     ![[,] [,]](_icc.gif)      |
2 | | ioossicc 11720 |
. . 3
      ![[,] [,]](_icc.gif)   |
3 | 2 | a1i 11 |
. 2
    
  ![[,] [,]](_icc.gif)    |
4 | | limcicciooub.1 |
. . . 4
   |
5 | | limcicciooub.2 |
. . . 4
   |
6 | 4, 5 | iccssred 37602 |
. . 3
   ![[,] [,]](_icc.gif) 
  |
7 | | ax-resscn 9596 |
. . 3
 |
8 | 6, 7 | syl6ss 3444 |
. 2
   ![[,] [,]](_icc.gif) 
  |
9 | | eqid 2451 |
. 2
  ℂfld   ℂfld |
10 | | eqid 2451 |
. 2
   ℂfld ↾t    ![[,] [,]](_icc.gif)         ℂfld
↾t    ![[,] [,]](_icc.gif)       |
11 | | retop 21782 |
. . . . . . . . 9
     |
12 | 11 | a1i 11 |
. . . . . . . 8
       |
13 | 4 | rexrd 9690 |
. . . . . . . . . . 11
   |
14 | | iocssre 11714 |
. . . . . . . . . . 11
     ![(,] (,]](_ioc.gif)    |
15 | 13, 5, 14 | syl2anc 667 |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif) 
  |
16 | | difssd 3561 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)     |
17 | 15, 16 | unssd 3610 |
. . . . . . . . 9
    ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
18 | | uniretop 21783 |
. . . . . . . . 9
      |
19 | 17, 18 | syl6sseq 3478 |
. . . . . . . 8
    ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)           |
20 | | elioore 11666 |
. . . . . . . . . . . . . . 15
   
  |
21 | 20 | ad2antlr 733 |
. . . . . . . . . . . . . 14
          |
22 | | simplr 762 |
. . . . . . . . . . . . . . . 16
             |
23 | 13 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
          |
24 | | pnfxr 11412 |
. . . . . . . . . . . . . . . . 17
 |
25 | | elioo2 11677 |
. . . . . . . . . . . . . . . . 17
      

    |
26 | 23, 24, 25 | sylancl 668 |
. . . . . . . . . . . . . . . 16
           

    |
27 | 22, 26 | mpbid 214 |
. . . . . . . . . . . . . . 15
            |
28 | 27 | simp2d 1021 |
. . . . . . . . . . . . . 14
          |
29 | | simpr 463 |
. . . . . . . . . . . . . 14
          |
30 | 5 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
          |
31 | | elioc2 11697 |
. . . . . . . . . . . . . . 15
      ![(,] (,]](_ioc.gif) 

    |
32 | 23, 30, 31 | syl2anc 667 |
. . . . . . . . . . . . . 14
           ![(,] (,]](_ioc.gif) 

    |
33 | 21, 28, 29, 32 | mpbir3and 1191 |
. . . . . . . . . . . . 13
          ![(,] (,]](_ioc.gif)    |
34 | 33 | orcd 394 |
. . . . . . . . . . . 12
           ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
35 | 20 | ad2antlr 733 |
. . . . . . . . . . . . . 14
       
  |
36 | | 3mix3 1179 |
. . . . . . . . . . . . . . . . 17

    |
37 | | 3ianor 1002 |
. . . . . . . . . . . . . . . . 17
 


   |
38 | 36, 37 | sylibr 216 |
. . . . . . . . . . . . . . . 16


   |
39 | 38 | adantl 468 |
. . . . . . . . . . . . . . 15
        
   |
40 | 4 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
       
  |
41 | 5 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
       
  |
42 | | elicc2 11699 |
. . . . . . . . . . . . . . . 16
 
    ![[,] [,]](_icc.gif)  
    |
43 | 40, 41, 42 | syl2anc 667 |
. . . . . . . . . . . . . . 15
           ![[,] [,]](_icc.gif)  
    |
44 | 39, 43 | mtbird 303 |
. . . . . . . . . . . . . 14
       
  ![[,] [,]](_icc.gif)    |
45 | 35, 44 | eldifd 3415 |
. . . . . . . . . . . . 13
       
   ![[,] [,]](_icc.gif)     |
46 | 45 | olcd 395 |
. . . . . . . . . . . 12
           ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
47 | 34, 46 | pm2.61dan 800 |
. . . . . . . . . . 11
 
   
   ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
48 | | elun 3574 |
. . . . . . . . . . 11
    ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
49 | 47, 48 | sylibr 216 |
. . . . . . . . . 10
 
   
   ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
50 | 49 | ralrimiva 2802 |
. . . . . . . . 9
         ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
51 | | dfss3 3422 |
. . . . . . . . 9
       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)    
       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
52 | 50, 51 | sylibr 216 |
. . . . . . . 8
       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)      |
53 | | eqid 2451 |
. . . . . . . . 9
   
       |
54 | 53 | ntrss 20070 |
. . . . . . . 8
         ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)               ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)           
              
       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)       |
55 | 12, 19, 52, 54 | syl3anc 1268 |
. . . . . . 7
       
              
       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)       |
56 | 24 | a1i 11 |
. . . . . . . . 9
   |
57 | | limcicciooub.3 |
. . . . . . . . 9
   |
58 | 5 | ltpnfd 11423 |
. . . . . . . . 9
   |
59 | 13, 56, 5, 57, 58 | eliood 37595 |
. . . . . . . 8
      |
60 | | iooretop 21786 |
. . . . . . . . 9
        |
61 | | isopn3i 20098 |
. . . . . . . . 9
             
                    |
62 | 12, 60, 61 | sylancl 668 |
. . . . . . . 8
       
             |
63 | 59, 62 | eleqtrrd 2532 |
. . . . . . 7
                  |
64 | 55, 63 | sseldd 3433 |
. . . . . 6
               ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)       |
65 | 5 | rexrd 9690 |
. . . . . . 7
   |
66 | 4, 5, 57 | ltled 9783 |
. . . . . . 7

  |
67 | | ubicc2 11749 |
. . . . . . 7
     ![[,] [,]](_icc.gif)    |
68 | 13, 65, 66, 67 | syl3anc 1268 |
. . . . . 6
   ![[,] [,]](_icc.gif)    |
69 | 64, 68 | elind 3618 |
. . . . 5
        
       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
70 | | iocssicc 11722 |
. . . . . . 7
  ![(,] (,]](_ioc.gif)    ![[,] [,]](_icc.gif)   |
71 | 70 | a1i 11 |
. . . . . 6
   ![(,] (,]](_ioc.gif) 
  ![[,] [,]](_icc.gif)    |
72 | | eqid 2451 |
. . . . . . 7
     ↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)    |
73 | 18, 72 | restntr 20198 |
. . . . . 6
        ![[,] [,]](_icc.gif)    ![(,] (,]](_ioc.gif)    ![[,] [,]](_icc.gif)            ↾t   ![[,] [,]](_icc.gif)        ![(,] (,]](_ioc.gif)          
       ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
74 | 12, 6, 71, 73 | syl3anc 1268 |
. . . . 5
          ↾t   ![[,] [,]](_icc.gif)        ![(,] (,]](_ioc.gif)                  ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
75 | 69, 74 | eleqtrrd 2532 |
. . . 4
          ↾t   ![[,] [,]](_icc.gif)        ![(,] (,]](_ioc.gif)     |
76 | | eqid 2451 |
. . . . . . . . 9
         |
77 | 9, 76 | rerest 21822 |
. . . . . . . 8
   ![[,] [,]](_icc.gif) 
   ℂfld ↾t   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)     |
78 | 6, 77 | syl 17 |
. . . . . . 7
    ℂfld
↾t   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)     |
79 | 78 | eqcomd 2457 |
. . . . . 6
      ↾t   ![[,] [,]](_icc.gif)      ℂfld
↾t   ![[,] [,]](_icc.gif)     |
80 | 79 | fveq2d 5869 |
. . . . 5
         ↾t   ![[,] [,]](_icc.gif)          ℂfld
↾t   ![[,] [,]](_icc.gif)      |
81 | 80 | fveq1d 5867 |
. . . 4
          ↾t   ![[,] [,]](_icc.gif)        ![(,] (,]](_ioc.gif)          ℂfld
↾t   ![[,] [,]](_icc.gif)        ![(,] (,]](_ioc.gif)     |
82 | 75, 81 | eleqtrd 2531 |
. . 3
        ℂfld ↾t   ![[,] [,]](_icc.gif)        ![(,] (,]](_ioc.gif)     |
83 | 68 | snssd 4117 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    |
84 | | ssequn2 3607 |
. . . . . . . 8
     ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
85 | 83, 84 | sylib 200 |
. . . . . . 7
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
86 | 85 | eqcomd 2457 |
. . . . . 6
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       |
87 | 86 | oveq2d 6306 |
. . . . 5
    ℂfld
↾t   ![[,] [,]](_icc.gif)      ℂfld
↾t    ![[,] [,]](_icc.gif)        |
88 | 87 | fveq2d 5869 |
. . . 4
       ℂfld
↾t   ![[,] [,]](_icc.gif)          ℂfld
↾t    ![[,] [,]](_icc.gif)         |
89 | | snunioo2 37606 |
. . . . . 6
             ![(,] (,]](_ioc.gif)    |
90 | 13, 65, 57, 89 | syl3anc 1268 |
. . . . 5
           ![(,] (,]](_ioc.gif)    |
91 | 90 | eqcomd 2457 |
. . . 4
   ![(,] (,]](_ioc.gif)            |
92 | 88, 91 | fveq12d 5871 |
. . 3
        ℂfld
↾t   ![[,] [,]](_icc.gif)        ![(,] (,]](_ioc.gif)          ℂfld
↾t    ![[,] [,]](_icc.gif)                    |
93 | 82, 92 | eleqtrd 2531 |
. 2
        ℂfld ↾t    ![[,] [,]](_icc.gif)                    |
94 | 1, 3, 8, 9, 10, 93 | limcres 22841 |
1
        lim   lim    |