Step | Hyp | Ref
| Expression |
1 | | funmpt 5249 |
. . . . . . . . 9
  #      |
2 | | funforn 5440 |
. . . . . . . . 9
   #       #         #         #       |
3 | 1, 2 | mpbi 145 |
. . . . . . . 8
  #         #
        #      |
4 | | fof 5433 |
. . . . . . . 8
   #         #
        #       #         #         #       |
5 | 3, 4 | ax-mp 5 |
. . . . . . 7
  #         #
        #      |
6 | | simpl 109 |
. . . . . . . . . 10
 
 #     |
7 | | breq1 4003 |
. . . . . . . . . . . . . 14
  #
#    |
8 | 7 | elrab 2893 |
. . . . . . . . . . . . 13
  #   #    |
9 | 8 | biimpi 120 |
. . . . . . . . . . . 12
  # 
 #    |
10 | 9 | adantl 277 |
. . . . . . . . . . 11
 
 #    #    |
11 | 10 | simpld 112 |
. . . . . . . . . 10
 
 #     |
12 | 10 | simprd 114 |
. . . . . . . . . 10
 
 #   #   |
13 | 6, 11, 12 | divclapd 8723 |
. . . . . . . . 9
 
 #       |
14 | 13 | ralrimiva 2550 |
. . . . . . . 8
   #
     |
15 | | eqid 2177 |
. . . . . . . . 9
  #       #      |
16 | 15 | rnmptss 5672 |
. . . . . . . 8
 
 #      #
      |
17 | 14, 16 | syl 14 |
. . . . . . 7
 
 #       |
18 | | fss 5372 |
. . . . . . 7
    #         #         #       #     
  #         #
        |
19 | 5, 17, 18 | sylancr 414 |
. . . . . 6
   #         #
        |
20 | 15 | dmmpt 5119 |
. . . . . . 7
  #       #      |
21 | | ssrab2 3240 |
. . . . . . . 8
  #
     #   |
22 | | ssrab2 3240 |
. . . . . . . 8
 # 
 |
23 | 21, 22 | sstri 3164 |
. . . . . . 7
  #
     |
24 | 20, 23 | eqsstri 3187 |
. . . . . 6
  #      |
25 | | cnex 7913 |
. . . . . . 7
 |
26 | 25, 25 | elpm2 6673 |
. . . . . 6
   #          #
      
 #      
  #
       |
27 | 19, 24, 26 | sylanblrc 416 |
. . . . 5
   #         |
28 | | dvfcnpm 13792 |
. . . . 5
   #        
 #           #
         |
29 | 27, 28 | syl 14 |
. . . 4
    #
        
 #          |
30 | | ssidd 3176 |
. . . . . . 7
   |
31 | | divclap 8611 |
. . . . . . . . . 10
 
#      |
32 | 31 | 3expb 1204 |
. . . . . . . . 9
  
#       |
33 | 8, 32 | sylan2b 287 |
. . . . . . . 8
 
 #       |
34 | 33 | fmpttd 5666 |
. . . . . . 7
   #        #
     |
35 | 22 | a1i 9 |
. . . . . . 7
  # 
  |
36 | 30, 34, 35 | dvbss 13787 |
. . . . . 6
 
  #       #    |
37 | | elrabi 2890 |
. . . . . . . 8
  # 
  |
38 | 37 | adantl 277 |
. . . . . . 7
 
 #     |
39 | | simpl 109 |
. . . . . . . . 9
 
 #     |
40 | 38 | sqcld 10624 |
. . . . . . . . 9
 
 #         |
41 | | breq1 4003 |
. . . . . . . . . . . . 13
  #
#    |
42 | 41 | elrab 2893 |
. . . . . . . . . . . 12
  #   #    |
43 | 42 | simprbi 275 |
. . . . . . . . . . 11
  # 
#   |
44 | 43 | adantl 277 |
. . . . . . . . . 10
 
 #   #   |
45 | | sqap0 10559 |
. . . . . . . . . . 11
      #
#    |
46 | 38, 45 | syl 14 |
. . . . . . . . . 10
 
 #        #
#    |
47 | 44, 46 | mpbird 167 |
. . . . . . . . 9
 
 #       #   |
48 | 39, 40, 47 | divclapd 8723 |
. . . . . . . 8
 
 #           |
49 | 48 | negcld 8232 |
. . . . . . 7
 
 #            |
50 | | simpr 110 |
. . . . . . . . 9
 
 #    #
   |
51 | | eqid 2177 |
. . . . . . . . . . 11
           |
52 | 51 | cntoptop 13666 |
. . . . . . . . . 10
      |
53 | | 0cn 7927 |
. . . . . . . . . . 11
 |
54 | | cnopnap 13727 |
. . . . . . . . . . 11
  #         |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . 10
 #        |
56 | | isopn3i 13268 |
. . . . . . . . . 10
      
 #                     #    #    |
57 | 52, 55, 56 | mp2an 426 |
. . . . . . . . 9
             #    #
  |
58 | 50, 57 | eleqtrrdi 2271 |
. . . . . . . 8
 
 #                #     |
59 | 38 | sqvald 10623 |
. . . . . . . . . . . . . 14
 
 #           |
60 | 59 | oveq2d 5884 |
. . . . . . . . . . . . 13
 
 #               |
61 | 39, 38, 38, 44, 44 | divdivap1d 8755 |
. . . . . . . . . . . . 13
 
 #             |
62 | 60, 61 | eqtr4d 2213 |
. . . . . . . . . . . 12
 
 #               |
63 | 62 | negeqd 8129 |
. . . . . . . . . . 11
 
 #                 |
64 | 39, 38, 44 | divclapd 8723 |
. . . . . . . . . . . 12
 
 #       |
65 | 64, 38, 44 | divnegapd 8736 |
. . . . . . . . . . 11
 
 #               |
66 | 63, 65 | eqtrd 2210 |
. . . . . . . . . 10
 
 #                 |
67 | 64 | negcld 8232 |
. . . . . . . . . . . 12
 
 #        |
68 | | eqid 2177 |
. . . . . . . . . . . . 13
  #          #    
    |
69 | 68 | cdivcncfap 13720 |
. . . . . . . . . . . 12
  
   #          #       |
70 | 67, 69 | syl 14 |
. . . . . . . . . . 11
 
 #     #          #       |
71 | | oveq2 5876 |
. . . . . . . . . . 11
             |
72 | 70, 50, 71 | cnmptlimc 13776 |
. . . . . . . . . 10
 
 #           #        lim    |
73 | 66, 72 | eqeltrd 2254 |
. . . . . . . . 9
 
 #             #
       lim    |
74 | | cncff 13697 |
. . . . . . . . . . . 12
   #          #       #           #
     |
75 | 70, 74 | syl 14 |
. . . . . . . . . . 11
 
 #     #           #
     |
76 | 22 | a1i 9 |
. . . . . . . . . . 11
 
 #    # 
  |
77 | 75, 76 | limcdifap 13764 |
. . . . . . . . . 10
 
 #      #    
   lim      #          #  #   lim    |
78 | | elrabi 2890 |
. . . . . . . . . . . . . . . . . . . . 21
   #
 #
  #    |
79 | 78 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
    #     #  #    #    |
80 | | breq1 4003 |
. . . . . . . . . . . . . . . . . . . . 21
  #
#    |
81 | 80 | elrab 2893 |
. . . . . . . . . . . . . . . . . . . 20
  #   #    |
82 | 79, 81 | sylib 122 |
. . . . . . . . . . . . . . . . . . 19
    #     #  #    #    |
83 | 82 | simpld 112 |
. . . . . . . . . . . . . . . . . 18
    #     #  #     |
84 | 37 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . 18
    #     #  #     |
85 | 83, 84 | subcld 8245 |
. . . . . . . . . . . . . . . . 17
    #     #  #       |
86 | 64 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
    #     #  #       |
87 | 81 | simprbi 275 |
. . . . . . . . . . . . . . . . . . 19
  # 
#   |
88 | 79, 87 | syl 14 |
. . . . . . . . . . . . . . . . . 18
    #     #  #   #   |
89 | 86, 83, 88 | divclapd 8723 |
. . . . . . . . . . . . . . . . 17
    #     #  #         |
90 | | mulneg12 8331 |
. . . . . . . . . . . . . . . . 17
                             |
91 | 85, 89, 90 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
    #     #  #                       |
92 | 84, 83, 89 | subdird 8349 |
. . . . . . . . . . . . . . . . 17
    #     #  #                           |
93 | 83, 84 | negsubdi2d 8261 |
. . . . . . . . . . . . . . . . . 18
    #     #  #          |
94 | 93 | oveq1d 5883 |
. . . . . . . . . . . . . . . . 17
    #     #  #                      |
95 | | oveq2 5876 |
. . . . . . . . . . . . . . . . . . . 20
       |
96 | | simpll 527 |
. . . . . . . . . . . . . . . . . . . . 21
    #     #  #  
  |
97 | 96, 83, 88 | divclapd 8723 |
. . . . . . . . . . . . . . . . . . . 20
    #     #  #       |
98 | 15, 95, 79, 97 | fvmptd3 5604 |
. . . . . . . . . . . . . . . . . . 19
    #     #  #      #
           |
99 | 43 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . . . . 21
    #     #  #   #   |
100 | 96, 84, 99 | divcanap2d 8725 |
. . . . . . . . . . . . . . . . . . . 20
    #     #  #         |
101 | 100 | oveq1d 5883 |
. . . . . . . . . . . . . . . . . . 19
    #     #  #             |
102 | 84, 86, 83, 88 | divassapd 8759 |
. . . . . . . . . . . . . . . . . . 19
    #     #  #                 |
103 | 98, 101, 102 | 3eqtr2d 2216 |
. . . . . . . . . . . . . . . . . 18
    #     #  #      #
               |
104 | | oveq2 5876 |
. . . . . . . . . . . . . . . . . . . 20
       |
105 | 50 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
    #     #  #    #    |
106 | 15, 104, 105, 86 | fvmptd3 5604 |
. . . . . . . . . . . . . . . . . . 19
    #     #  #      #
           |
107 | 86, 83, 88 | divcanap2d 8725 |
. . . . . . . . . . . . . . . . . . 19
    #     #  #             |
108 | 106, 107 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . . 18
    #     #  #      #
               |
109 | 103, 108 | oveq12d 5886 |
. . . . . . . . . . . . . . . . 17
    #     #  #       #           #                         |
110 | 92, 94, 109 | 3eqtr4d 2220 |
. . . . . . . . . . . . . . . 16
    #     #  #                #           #
          |
111 | 86, 83, 88 | divnegapd 8736 |
. . . . . . . . . . . . . . . . 17
    #     #  #          
    |
112 | 111 | oveq2d 5884 |
. . . . . . . . . . . . . . . 16
    #     #  #                       |
113 | 91, 110, 112 | 3eqtr3d 2218 |
. . . . . . . . . . . . . . 15
    #     #  #       #           #                    |
114 | 113 | oveq1d 5883 |
. . . . . . . . . . . . . 14
    #     #  #        #           #                           |
115 | 86 | negcld 8232 |
. . . . . . . . . . . . . . . 16
    #     #  #        |
116 | 115, 83, 88 | divclapd 8723 |
. . . . . . . . . . . . . . 15
    #     #  #          |
117 | | breq1 4003 |
. . . . . . . . . . . . . . . . . . 19
  #
#    |
118 | 117 | elrab 2893 |
. . . . . . . . . . . . . . . . . 18
   #
 #
   #  #    |
119 | 118 | simprbi 275 |
. . . . . . . . . . . . . . . . 17
   #
 #
 #   |
120 | 119 | adantl 277 |
. . . . . . . . . . . . . . . 16
    #     #  #   #   |
121 | 83, 84, 120 | subap0d 8578 |
. . . . . . . . . . . . . . 15
    #     #  #     #   |
122 | 116, 85, 121 | divcanap3d 8728 |
. . . . . . . . . . . . . 14
    #     #  #                       |
123 | 114, 122 | eqtrd 2210 |
. . . . . . . . . . . . 13
    #     #  #        #           #                   |
124 | 123 | mpteq2dva 4090 |
. . . . . . . . . . . 12
 
 #      #  #       #           #
               #  #          |
125 | | ssrab2 3240 |
. . . . . . . . . . . . 13
  #  # 
 #   |
126 | | resmpt 4950 |
. . . . . . . . . . . . 13
   #  # 
 # 
   #          #  #      #  #          |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . . . 12
   #          #  #      #  #         |
128 | 124, 127 | eqtr4di 2228 |
. . . . . . . . . . 11
 
 #      #  #       #           #
               #    
  
  #
 #
    |
129 | 128 | oveq1d 5883 |
. . . . . . . . . 10
 
 #       #  #       #           #
            lim      #    
  
  #
 #
  lim
   |
130 | 77, 129 | eqtr4d 2213 |
. . . . . . . . 9
 
 #      #    
   lim      #
 #
      #           #             lim    |
131 | 73, 130 | eleqtrd 2256 |
. . . . . . . 8
 
 #              #  #       #
          #             lim    |
132 | 51 | cntoptopon 13665 |
. . . . . . . . . 10
     TopOn   |
133 | 132 | toponrestid 13152 |
. . . . . . . . 9
           ↾t   |
134 | | eqid 2177 |
. . . . . . . . 9
   #
 #
      #           #                #  #       #
          #              |
135 | | ssidd 3176 |
. . . . . . . . 9
 
 #     |
136 | 34 | adantr 276 |
. . . . . . . . 9
 
 #     #        #
     |
137 | 133, 51, 134, 135, 136, 76 | eldvap 13784 |
. . . . . . . 8
 
 #      
 #             
              #              #  #       #
          #             lim      |
138 | 58, 131, 137 | mpbir2and 944 |
. . . . . . 7
 
 #       #                |
139 | | breldmg 4828 |
. . . . . . 7
           
 #                  #
       |
140 | 38, 49, 138, 139 | syl3anc 1238 |
. . . . . 6
 
 #    
 #        |
141 | 36, 140 | eqelssd 3174 |
. . . . 5
 
  #       #    |
142 | 141 | feq2d 5348 |
. . . 4
     #           #
          #         #       |
143 | 29, 142 | mpbid 147 |
. . 3
    #
        #
     |
144 | 143 | ffnd 5361 |
. 2
    #
      #
   |
145 | 11 | sqcld 10624 |
. . . . . 6
 
 #         |
146 | | sqap0 10559 |
. . . . . . . 8
      #
#    |
147 | 11, 146 | syl 14 |
. . . . . . 7
 
 #        #
#    |
148 | 12, 147 | mpbird 167 |
. . . . . 6
 
 #       #   |
149 | 6, 145, 148 | divclapd 8723 |
. . . . 5
 
 #           |
150 | 149 | negcld 8232 |
. . . 4
 
 #            |
151 | 150 | ralrimiva 2550 |
. . 3
   #
           |
152 | | eqid 2177 |
. . . 4
  #            #           |
153 | 152 | fnmpt 5337 |
. . 3
 
 #         
  #
          #
   |
154 | 151, 153 | syl 14 |
. 2
   #           #
   |
155 | 29 | ffund 5364 |
. . . . 5
 
  #        |
156 | 155 | adantr 276 |
. . . 4
 
 #   
  #        |
157 | | funbrfv 5549 |
. . . 4
    #           #                  #                   |
158 | 156, 138,
157 | sylc 62 |
. . 3
 
 #       #                  |
159 | | oveq1 5875 |
. . . . . 6
           |
160 | 159 | oveq2d 5884 |
. . . . 5
               |
161 | 160 | negeqd 8129 |
. . . 4
                 |
162 | 152, 161,
50, 49 | fvmptd3 5604 |
. . 3
 
 #      #                      |
163 | 158, 162 | eqtr4d 2213 |
. 2
 
 #       #            #
              |
164 | 144, 154,
163 | eqfnfvd 5611 |
1
    #
       #            |