Step | Hyp | Ref
| Expression |
1 | | dvadd.bg |
. . . 4
       |
2 | | eqid 2177 |
. . . . 5
 ↾t   ↾t   |
3 | | dvaddcntop.j |
. . . . 5
      |
4 | | eqid 2177 |
. . . . 5
  #                   #                  |
5 | | dvaddbr.s |
. . . . 5

  |
6 | | dvaddxx.g |
. . . . 5
       |
7 | | dvadd.x |
. . . . 5

  |
8 | 2, 3, 4, 5, 6, 7 | eldvap 14154 |
. . . 4
            ↾t         #
                lim      |
9 | 1, 8 | mpbid 147 |
. . 3
       ↾t         #
                lim     |
10 | 9 | simpld 112 |
. 2
      ↾t        |
11 | | dvadd.f |
. . . . 5
       |
12 | 7, 5 | sstrd 3166 |
. . . . 5

  |
13 | 3 | cntoptopon 14035 |
. . . . . . . . 9
TopOn   |
14 | | resttopon 13674 |
. . . . . . . . 9
  TopOn 

 ↾t  TopOn    |
15 | 13, 5, 14 | sylancr 414 |
. . . . . . . 8
 
↾t  TopOn    |
16 | | topontop 13517 |
. . . . . . . 8
  ↾t  TopOn   ↾t    |
17 | 15, 16 | syl 14 |
. . . . . . 7
 
↾t    |
18 | | toponuni 13518 |
. . . . . . . . 9
  ↾t  TopOn    ↾t    |
19 | 15, 18 | syl 14 |
. . . . . . . 8
   ↾t    |
20 | 7, 19 | sseqtrd 3194 |
. . . . . . 7

  ↾t    |
21 | | eqid 2177 |
. . . . . . . 8
  ↾t   
↾t   |
22 | 21 | ntrss2 13624 |
. . . . . . 7
  
↾t 
  ↾t        ↾t        |
23 | 17, 20, 22 | syl2anc 411 |
. . . . . 6
      ↾t        |
24 | | dvadd.bf |
. . . . . . . 8
       |
25 | | eqid 2177 |
. . . . . . . . 9
  #                   #                  |
26 | 2, 3, 25, 5, 11, 7 | eldvap 14154 |
. . . . . . . 8
            ↾t         #
                lim      |
27 | 24, 26 | mpbid 147 |
. . . . . . 7
       ↾t         #
                lim     |
28 | 27 | simpld 112 |
. . . . . 6
      ↾t        |
29 | 23, 28 | sseldd 3157 |
. . . . 5
   |
30 | 11, 12, 29 | dvlemap 14152 |
. . . 4
 
 #                   |
31 | 6, 12, 29 | dvlemap 14152 |
. . . 4
 
 #                   |
32 | | ssidd 3177 |
. . . 4

  |
33 | | txtopon 13765 |
. . . . . 6
  TopOn 
TopOn  
  TopOn      |
34 | 13, 13, 33 | mp2an 426 |
. . . . 5
  TopOn     |
35 | 34 | toponrestid 13524 |
. . . 4
    
↾t     |
36 | 27 | simprd 114 |
. . . 4
   
# 
               lim    |
37 | 9 | simprd 114 |
. . . 4
   
# 
               lim    |
38 | 3 | addcncntop 14055 |
. . . . 5
     |
39 | 5, 11, 7 | dvcl 14155 |
. . . . . . 7
 
    
  |
40 | 24, 39 | mpdan 421 |
. . . . . 6
   |
41 | 5, 6, 7 | dvcl 14155 |
. . . . . . 7
 
    
  |
42 | 1, 41 | mpdan 421 |
. . . . . 6
   |
43 | 40, 42 | opelxpd 4660 |
. . . . 5
        |
44 | 34 | toponunii 13520 |
. . . . . 6
      |
45 | 44 | cncnpi 13731 |
. . . . 5
      
                 |
46 | 38, 43, 45 | sylancr 414 |
. . . 4
    
         |
47 | 30, 31, 32, 32, 3, 35, 36, 37, 46 | limccnp2cntop 14149 |
. . 3
     
# 
                               lim    |
48 | | elrabi 2891 |
. . . . . . . . . . 11
  #    |
49 | 48 | adantl 277 |
. . . . . . . . . 10
 
 #     |
50 | 11 | ffnd 5367 |
. . . . . . . . . . . 12
   |
51 | 50 | adantr 276 |
. . . . . . . . . . 11
 
 #  
  |
52 | 6 | ffnd 5367 |
. . . . . . . . . . . 12
   |
53 | 52 | adantr 276 |
. . . . . . . . . . 11
 
 #  
  |
54 | | cnex 7935 |
. . . . . . . . . . . . 13
 |
55 | | ssexg 4143 |
. . . . . . . . . . . . 13
 
   |
56 | 12, 54, 55 | sylancl 413 |
. . . . . . . . . . . 12
   |
57 | 56 | adantr 276 |
. . . . . . . . . . 11
 
 #  
  |
58 | | inidm 3345 |
. . . . . . . . . . 11
   |
59 | | eqidd 2178 |
. . . . . . . . . . 11
    #
 
           |
60 | | eqidd 2178 |
. . . . . . . . . . 11
    #
 
           |
61 | 11 | adantr 276 |
. . . . . . . . . . . . 13
 
 #         |
62 | 61 | ffvelcdmda 5652 |
. . . . . . . . . . . 12
    #
 
       |
63 | 6 | adantr 276 |
. . . . . . . . . . . . 13
 
 #         |
64 | 63 | ffvelcdmda 5652 |
. . . . . . . . . . . 12
    #
 
       |
65 | 62, 64 | addcld 7977 |
. . . . . . . . . . 11
    #
 
             |
66 | 51, 53, 57, 57, 58, 59, 60, 65 | ofvalg 6092 |
. . . . . . . . . 10
    #
 
                    |
67 | 49, 66 | mpdan 421 |
. . . . . . . . 9
 
 #     
                |
68 | | eqidd 2178 |
. . . . . . . . . . 11
    #
 
           |
69 | | eqidd 2178 |
. . . . . . . . . . 11
    #
 
           |
70 | 61 | ffvelcdmda 5652 |
. . . . . . . . . . . 12
    #
 
       |
71 | 63 | ffvelcdmda 5652 |
. . . . . . . . . . . 12
    #
 
       |
72 | 70, 71 | addcld 7977 |
. . . . . . . . . . 11
    #
 
             |
73 | 51, 53, 57, 57, 58, 68, 69, 72 | ofvalg 6092 |
. . . . . . . . . 10
    #
 
                    |
74 | 29, 73 | mpidan 423 |
. . . . . . . . 9
 
 #     
                |
75 | 67, 74 | oveq12d 5893 |
. . . . . . . 8
 
 #                                           |
76 | | ffvelcdm 5650 |
. . . . . . . . . 10
     
       |
77 | 11, 48, 76 | syl2an 289 |
. . . . . . . . 9
 
 #         |
78 | 63, 49 | ffvelcdmd 5653 |
. . . . . . . . 9
 
 #         |
79 | 11, 29 | ffvelcdmd 5653 |
. . . . . . . . . 10
       |
80 | 79 | adantr 276 |
. . . . . . . . 9
 
 #         |
81 | 6, 29 | ffvelcdmd 5653 |
. . . . . . . . . 10
       |
82 | 81 | adantr 276 |
. . . . . . . . 9
 
 #         |
83 | 77, 78, 80, 82 | addsub4d 8315 |
. . . . . . . 8
 
 #                                                 |
84 | 75, 83 | eqtrd 2210 |
. . . . . . 7
 
 #                                           |
85 | 84 | oveq1d 5890 |
. . . . . 6
 
 #                                                   |
86 | 61, 49 | ffvelcdmd 5653 |
. . . . . . . 8
 
 #         |
87 | 86, 80 | subcld 8268 |
. . . . . . 7
 
 #               |
88 | 78, 82 | subcld 8268 |
. . . . . . 7
 
 #               |
89 | | ssrab2 3241 |
. . . . . . . . . 10

# 
 |
90 | 89, 12 | sstrid 3167 |
. . . . . . . . 9
  #
   |
91 | 90 | sselda 3156 |
. . . . . . . 8
 
 #     |
92 | 12, 29 | sseldd 3157 |
. . . . . . . . 9
   |
93 | 92 | adantr 276 |
. . . . . . . 8
 
 #  
  |
94 | 91, 93 | subcld 8268 |
. . . . . . 7
 
 #       |
95 | | breq1 4007 |
. . . . . . . . . . 11
  #
#    |
96 | 95 | elrab 2894 |
. . . . . . . . . 10
  #   #
   |
97 | 96 | simprbi 275 |
. . . . . . . . 9
  #  #   |
98 | 97 | adantl 277 |
. . . . . . . 8
 
 #   #   |
99 | 91, 93, 98 | subap0d 8601 |
. . . . . . 7
 
 #     #   |
100 | 87, 88, 94, 99 | divdirapd 8786 |
. . . . . 6
 
 #                                                             |
101 | 85, 100 | eqtrd 2210 |
. . . . 5
 
 #                                                       |
102 | 101 | mpteq2dva 4094 |
. . . 4
   #      
                  #                                   |
103 | 102 | oveq1d 5890 |
. . 3
    #
                      lim    
# 
                               lim    |
104 | 47, 103 | eleqtrrd 2257 |
. 2
     
# 
    
                lim    |
105 | | eqid 2177 |
. . 3
  #                         #      
                 |
106 | | addcl 7936 |
. . . . 5
 
     |
107 | 106 | adantl 277 |
. . . 4
 
       |
108 | 107, 11, 6, 56, 56, 58 | off 6095 |
. . 3
          |
109 | 2, 3, 105, 5, 108, 7 | eldvap 14154 |
. 2
     
    
      ↾t      
    #
                      lim      |
110 | 10, 104, 109 | mpbir2and 944 |
1
   
        |