Proof of Theorem dirkercncflem2
Step | Hyp | Ref
| Expression |
1 | | difss 3560 |
. . . . 5
       
     |
2 | | ioossre 11696 |
. . . . 5
     |
3 | 1, 2 | sstri 3441 |
. . . 4
       
 |
4 | 3 | a1i 11 |
. . 3
           |
5 | | dirkercncflem2.n |
. . . . . . . . 9
   |
6 | 5 | adantr 467 |
. . . . . . . 8
 
        
  |
7 | 6 | nnred 10624 |
. . . . . . 7
 
        
  |
8 | | halfre 10828 |
. . . . . . . 8
   |
9 | 8 | a1i 11 |
. . . . . . 7
 
             |
10 | 7, 9 | readdcld 9670 |
. . . . . 6
 
               |
11 | 4 | sselda 3432 |
. . . . . 6
 
           |
12 | 10, 11 | remulcld 9671 |
. . . . 5
 
                 |
13 | 12 | resincld 14197 |
. . . 4
 
                     |
14 | | dirkercncflem2.f |
. . . 4
     
               |
15 | 13, 14 | fmptd 6046 |
. . 3
               |
16 | | 2re 10679 |
. . . . . . 7
 |
17 | | pire 23413 |
. . . . . . 7
 |
18 | 16, 17 | remulcli 9657 |
. . . . . 6
   |
19 | 18 | a1i 11 |
. . . . 5
 
          
  |
20 | 11 | rehalfcld 10859 |
. . . . . 6
 
             |
21 | 20 | resincld 14197 |
. . . . 5
 
                 |
22 | 19, 21 | remulcld 9671 |
. . . 4
 
                     |
23 | | dirkercncflem2.g |
. . . 4
     
               |
24 | 22, 23 | fmptd 6046 |
. . 3
               |
25 | | iooretop 21786 |
. . . 4
         |
26 | 25 | a1i 11 |
. . 3
           |
27 | | dirkercncflem2.y |
. . 3
       |
28 | | eqid 2451 |
. . 3
                 |
29 | 14 | a1i 11 |
. . . . . . . 8
                       |
30 | 29 | oveq2d 6306 |
. . . . . . 7
                           |
31 | | resmpt 5154 |
. . . . . . . . . . . 12
     
                    
         
                |
32 | 3, 31 | ax-mp 5 |
. . . . . . . . . . 11
            
                              |
33 | 32 | eqcomi 2460 |
. . . . . . . . . 10
                                
          |
34 | 33 | a1i 11 |
. . . . . . . . 9
      
                               
      |
35 | 34 | oveq2d 6306 |
. . . . . . . 8
                                    
            |
36 | | ax-resscn 9596 |
. . . . . . . . . 10
 |
37 | 36 | a1i 11 |
. . . . . . . . 9

  |
38 | 5 | nncnd 10625 |
. . . . . . . . . . . . . 14
   |
39 | | halfcn 10829 |
. . . . . . . . . . . . . . 15
   |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
     |
41 | 38, 40 | addcld 9662 |
. . . . . . . . . . . . 13
       |
42 | 41 | adantr 467 |
. . . . . . . . . . . 12
 

      |
43 | 37 | sselda 3432 |
. . . . . . . . . . . 12
 

  |
44 | 42, 43 | mulcld 9663 |
. . . . . . . . . . 11
 

        |
45 | 44 | sincld 14184 |
. . . . . . . . . 10
 

            |
46 | | eqid 2451 |
. . . . . . . . . 10
                         |
47 | 45, 46 | fmptd 6046 |
. . . . . . . . 9
                   |
48 | | ssid 3451 |
. . . . . . . . . . 11
 |
49 | 48, 3 | pm3.2i 457 |
. . . . . . . . . 10
        
  |
50 | 49 | a1i 11 |
. . . . . . . . 9
             |
51 | | eqid 2451 |
. . . . . . . . . 10
  ℂfld   ℂfld |
52 | 51 | tgioo2 21821 |
. . . . . . . . . 10
       ℂfld
↾t   |
53 | 51, 52 | dvres 22866 |
. . . . . . . . 9
                                                                            
                |
54 | 37, 47, 50, 53 | syl21anc 1267 |
. . . . . . . 8
              
                               
                |
55 | | retop 21782 |
. . . . . . . . . . 11
     |
56 | | rehaus 21817 |
. . . . . . . . . . . . 13
     |
57 | 2, 27 | sseldi 3430 |
. . . . . . . . . . . . 13
   |
58 | | uniretop 21783 |
. . . . . . . . . . . . . 14
      |
59 | 58 | sncld 20387 |
. . . . . . . . . . . . 13
     

 
          |
60 | 56, 57, 59 | sylancr 669 |
. . . . . . . . . . . 12
             |
61 | 58 | difopn 20049 |
. . . . . . . . . . . 12
           
                       |
62 | 25, 60, 61 | sylancr 669 |
. . . . . . . . . . 11
               |
63 | | isopn3i 20098 |
. . . . . . . . . . 11
                         
                       |
64 | 55, 62, 63 | sylancr 669 |
. . . . . . . . . 10
       
                       |
65 | 64 | reseq2d 5105 |
. . . . . . . . 9
                      
                                        |
66 | | reelprrecn 9631 |
. . . . . . . . . . . . 13
    |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
      |
68 | 41 | adantr 467 |
. . . . . . . . . . . . . . 15
 

      |
69 | | simpr 463 |
. . . . . . . . . . . . . . 15
 

  |
70 | 68, 69 | mulcld 9663 |
. . . . . . . . . . . . . 14
 

        |
71 | 70 | sincld 14184 |
. . . . . . . . . . . . 13
 

            |
72 | | eqid 2451 |
. . . . . . . . . . . . 13
                         |
73 | 71, 72 | fmptd 6046 |
. . . . . . . . . . . 12
                   |
74 | | ssid 3451 |
. . . . . . . . . . . . 13
 |
75 | 74 | a1i 11 |
. . . . . . . . . . . 12

  |
76 | | dvsinax 37783 |
. . . . . . . . . . . . . . . 16
                                       |
77 | 41, 76 | syl 17 |
. . . . . . . . . . . . . . 15
                                   |
78 | 77 | dmeqd 5037 |
. . . . . . . . . . . . . 14
                                   |
79 | | eqid 2451 |
. . . . . . . . . . . . . . 15
                                     |
80 | 70 | coscld 14185 |
. . . . . . . . . . . . . . . 16
 

            |
81 | 68, 80 | mulcld 9663 |
. . . . . . . . . . . . . . 15
 

                  |
82 | 79, 81 | dmmptd 5708 |
. . . . . . . . . . . . . 14
                     |
83 | 78, 82 | eqtrd 2485 |
. . . . . . . . . . . . 13
                 |
84 | 36, 83 | syl5sseqr 3481 |
. . . . . . . . . . . 12

                |
85 | | dvres3 22868 |
. . . . . . . . . . . 12
    
                   
                                                 |
86 | 67, 73, 75, 84, 85 | syl22anc 1269 |
. . . . . . . . . . 11
              
                    |
87 | | resmpt 5154 |
. . . . . . . . . . . . 13

            
               |
88 | 36, 87 | mp1i 13 |
. . . . . . . . . . . 12
                             |
89 | 88 | oveq2d 6306 |
. . . . . . . . . . 11
              
                  |
90 | 77 | reseq1d 5104 |
. . . . . . . . . . . 12
                                       |
91 | | resmpt 5154 |
. . . . . . . . . . . . 13

                                        |
92 | 36, 91 | ax-mp 5 |
. . . . . . . . . . . 12
                                       |
93 | 90, 92 | syl6eq 2501 |
. . . . . . . . . . 11
                                     |
94 | 86, 89, 93 | 3eqtr3d 2493 |
. . . . . . . . . 10
                                   |
95 | 94 | reseq1d 5104 |
. . . . . . . . 9
                    
                                  |
96 | | resmpt 5154 |
. . . . . . . . . 10
     
                                    
                      |
97 | 3, 96 | mp1i 13 |
. . . . . . . . 9
                                  
                      |
98 | 65, 95, 97 | 3eqtrd 2489 |
. . . . . . . 8
                      
                                          |
99 | 35, 54, 98 | 3eqtrd 2489 |
. . . . . . 7
                            
                      |
100 | | dirkercncflem2.h |
. . . . . . . . 9
     
                     |
101 | 100 | a1i 11 |
. . . . . . . 8
                             |
102 | 101 | eqcomd 2457 |
. . . . . . 7
      
                      |
103 | 30, 99, 102 | 3eqtrd 2489 |
. . . . . 6
     |
104 | 103 | dmeqd 5037 |
. . . . 5
     |
105 | 11 | recnd 9669 |
. . . . . . 7
 
           |
106 | 105, 81 | syldan 473 |
. . . . . 6
 
                           |
107 | 100, 106 | dmmptd 5708 |
. . . . 5
     
     |
108 | 104, 107 | eqtr2d 2486 |
. . . 4
         
   |
109 | | eqimss 3484 |
. . . 4
     
   

            |
110 | 108, 109 | syl 17 |
. . 3
         
   |
111 | | dirkercncflem2.i |
. . . . . . . 8
     
             |
112 | 111 | a1i 11 |
. . . . . . 7
                     |
113 | | resmpt 5154 |
. . . . . . . . . . . . 13
     
                              
                |
114 | 3, 113 | ax-mp 5 |
. . . . . . . . . . . 12
    
                      
               |
115 | 114 | eqcomi 2460 |
. . . . . . . . . . 11
           
                               |
116 | 115 | oveq2i 6301 |
. . . . . . . . . 10
                                               |
117 | 116 | a1i 11 |
. . . . . . . . 9
                                                 |
118 | | 2cn 10680 |
. . . . . . . . . . . . . 14
 |
119 | | picn 23414 |
. . . . . . . . . . . . . 14
 |
120 | 118, 119 | mulcli 9648 |
. . . . . . . . . . . . 13
   |
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
 

    |
122 | 43 | halfcld 10857 |
. . . . . . . . . . . . 13
 

    |
123 | 122 | sincld 14184 |
. . . . . . . . . . . 12
 

        |
124 | 121, 123 | mulcld 9663 |
. . . . . . . . . . 11
 

            |
125 | | eqid 2451 |
. . . . . . . . . . 11
                         |
126 | 124, 125 | fmptd 6046 |
. . . . . . . . . 10
                   |
127 | 51, 52 | dvres 22866 |
. . . . . . . . . 10
                                                                            
                |
128 | 37, 126, 50, 127 | syl21anc 1267 |
. . . . . . . . 9
              
                               
                |
129 | 64 | reseq2d 5105 |
. . . . . . . . . 10
                      
                                        |
130 | 36 | sseli 3428 |
. . . . . . . . . . . . . . . 16
   |
131 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . . . . . 21
   |
132 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . . . 21
   |
133 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
   |
134 | | 2ne0 10702 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
136 | 131, 132,
133, 135 | div13d 10407 |
. . . . . . . . . . . . . . . . . . . 20
           |
137 | | halfcl 10838 |
. . . . . . . . . . . . . . . . . . . . 21
     |
138 | 137 | mulid1d 9660 |
. . . . . . . . . . . . . . . . . . . 20
         |
139 | 136, 138 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . 19
         |
140 | 139 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                 |
141 | 140 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
   
                     |
142 | 141 | eqcomd 2457 |
. . . . . . . . . . . . . . . 16
   
                     |
143 | 130, 142 | syl 17 |
. . . . . . . . . . . . . . 15
   
                     |
144 | 143 | adantl 468 |
. . . . . . . . . . . . . 14
 

            
           |
145 | 144 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
                             |
146 | 145 | oveq2d 6306 |
. . . . . . . . . . . 12
     
                           |
147 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 

    |
148 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 

    |
149 | 148, 69 | mulcld 9663 |
. . . . . . . . . . . . . . . . . 18
 

      |
150 | 149 | sincld 14184 |
. . . . . . . . . . . . . . . . 17
 

          |
151 | 147, 150 | mulcld 9663 |
. . . . . . . . . . . . . . . 16
 

              |
152 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
                             |
153 | 151, 152 | fmptd 6046 |
. . . . . . . . . . . . . . 15
                     |
154 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . . . 21
   |
155 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
156 | 154, 155 | mulcld 9663 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
157 | | dvasinbx 37792 |
. . . . . . . . . . . . . . . . . . . 20
   
       
               
               |
158 | 156, 39, 157 | sylancl 668 |
. . . . . . . . . . . . . . . . . . 19
     
               
               |
159 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
160 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
161 | 159, 160,
148 | mul32d 9843 |
. . . . . . . . . . . . . . . . . . . . . 22
 

              |
162 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
163 | 159, 162 | recidd 10378 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

      |
164 | 163 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . 22
 

          |
165 | 160 | mulid2d 9661 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
166 | 161, 164,
165 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . . . . 21
 

        |
167 | 139 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
168 | 167 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 

                |
169 | 166, 168 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . 20
 

   
                      |
170 | 169 | mpteq2dva 4489 |
. . . . . . . . . . . . . . . . . . 19
                               |
171 | 158, 170 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . 18
     
                       |
172 | 171 | dmeqd 5037 |
. . . . . . . . . . . . . . . . 17
                  
          |
173 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
           
         |
174 | 69 | halfcld 10857 |
. . . . . . . . . . . . . . . . . . . 20
 

    |
175 | 174 | coscld 14185 |
. . . . . . . . . . . . . . . . . . 19
 

        |
176 | 160, 175 | mulcld 9663 |
. . . . . . . . . . . . . . . . . 18
 

          |
177 | 173, 176 | dmmptd 5708 |
. . . . . . . . . . . . . . . . 17
             |
178 | 172, 177 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
                   |
179 | 36, 178 | syl5sseqr 3481 |
. . . . . . . . . . . . . . 15

                  |
180 | | dvres3 22868 |
. . . . . . . . . . . . . . 15
    
                     
   
                            
                      |
181 | 67, 153, 75, 179, 180 | syl22anc 1269 |
. . . . . . . . . . . . . 14
                
                      |
182 | | resmpt 5154 |
. . . . . . . . . . . . . . . 16

    
              
            |
183 | 36, 182 | mp1i 13 |
. . . . . . . . . . . . . . 15
                
   
            |
184 | 183 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                
                    |
185 | 171 | reseq1d 5104 |
. . . . . . . . . . . . . 14
                                 |
186 | 181, 184,
185 | 3eqtr3d 2493 |
. . . . . . . . . . . . 13
     
                         |
187 | | resmpt 5154 |
. . . . . . . . . . . . . 14

                        |
188 | 36, 187 | ax-mp 5 |
. . . . . . . . . . . . 13
                       |
189 | 186, 188 | syl6eq 2501 |
. . . . . . . . . . . 12
     
                       |
190 | 146, 189 | eqtrd 2485 |
. . . . . . . . . . 11
     
                     |
191 | 190 | reseq1d 5104 |
. . . . . . . . . 10
                    
                   
      |
192 | 4 | resmptd 5156 |
. . . . . . . . . 10
                
         
              |
193 | 129, 191,
192 | 3eqtrd 2489 |
. . . . . . . . 9
                      
                                  |
194 | 117, 128,
193 | 3eqtrd 2489 |
. . . . . . . 8
                                           |
195 | 194 | eqcomd 2457 |
. . . . . . 7
      
                                    |
196 | 23 | a1i 11 |
. . . . . . . . 9
            
          |
197 | 196 | oveq2d 6306 |
. . . . . . . 8
                           |
198 | 197 | eqcomd 2457 |
. . . . . . 7
                           |
199 | 112, 195,
198 | 3eqtrrd 2490 |
. . . . . 6
     |
200 | 199 | dmeqd 5037 |
. . . . 5
     |
201 | 105, 176 | syldan 473 |
. . . . . 6
 
                   |
202 | 111, 201 | dmmptd 5708 |
. . . . 5
     
     |
203 | 200, 202 | eqtr2d 2486 |
. . . 4
         
   |
204 | | eqimss 3484 |
. . . 4
     
   

            |
205 | 203, 204 | syl 17 |
. . 3
         
   |
206 | 105, 70 | syldan 473 |
. . . . . . . 8
 
                 |
207 | 206 | ralrimiva 2802 |
. . . . . . 7
      
            |
208 | | eqid 2451 |
. . . . . . . 8
                                 |
209 | 208 | fnmpt 5704 |
. . . . . . 7
 
                                         |
210 | 207, 209 | syl 17 |
. . . . . 6
      
                    |
211 | | eqidd 2452 |
. . . . . . . . . 10
 
              
                            |
212 | | simpr 463 |
. . . . . . . . . . 11
           
   |
213 | 212 | oveq2d 6306 |
. . . . . . . . . 10
           
               |
214 | | simpr 463 |
. . . . . . . . . 10
 
        
          |
215 | 38 | adantr 467 |
. . . . . . . . . . . 12
 
        
  |
216 | | 1cnd 9659 |
. . . . . . . . . . . . 13
 
           |
217 | 216 | halfcld 10857 |
. . . . . . . . . . . 12
 
             |
218 | 215, 217 | addcld 9662 |
. . . . . . . . . . 11
 
               |
219 | | eldifi 3555 |
. . . . . . . . . . . . . 14
        
      |
220 | | elioore 11666 |
. . . . . . . . . . . . . 14
       |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . . 13
        
  |
222 | 221 | recnd 9669 |
. . . . . . . . . . . 12
        
  |
223 | 222 | adantl 468 |
. . . . . . . . . . 11
 
        
  |
224 | 218, 223 | mulcld 9663 |
. . . . . . . . . 10
 
                 |
225 | 211, 213,
214, 224 | fvmptd 5954 |
. . . . . . . . 9
 
                                     |
226 | | eleq1 2517 |
. . . . . . . . . . . . . . . 16
         
    
      |
227 | 226 | anbi2d 710 |
. . . . . . . . . . . . . . 15
  
        
             |
228 | | oveq1 6297 |
. . . . . . . . . . . . . . . 16
 
         |
229 | 228 | neeq1d 2683 |
. . . . . . . . . . . . . . 15
      
      |
230 | 227, 229 | imbi12d 322 |
. . . . . . . . . . . . . 14
   
                         
       |
231 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . . . . 21
               |
232 | | elioore 11666 |
. . . . . . . . . . . . . . . . . . . . 21
       |
233 | 231, 232,
130 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
           |
234 | | 2cnd 10682 |
. . . . . . . . . . . . . . . . . . . 20
           |
235 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
           |
236 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
           |
237 | | 0re 9643 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
238 | | pipos 23415 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
239 | 237, 238 | gtneii 9746 |
. . . . . . . . . . . . . . . . . . . . 21
 |
240 | 239 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
           |
241 | 233, 234,
235, 236, 240 | divdiv1d 10414 |
. . . . . . . . . . . . . . . . . . 19
            
      |
242 | 241 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . 18
                   |
243 | 242 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
                   |
244 | | dirkercncflem2.yne0 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
245 | 244 | neneqd 2629 |
. . . . . . . . . . . . . . . . . 18
 
                 |
246 | 105 | halfcld 10857 |
. . . . . . . . . . . . . . . . . . 19
 
             |
247 | | sineq0 23476 |
. . . . . . . . . . . . . . . . . . 19
                 |
248 | 246, 247 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
                       |
249 | 245, 248 | mtbid 302 |
. . . . . . . . . . . . . . . . 17
 
            
  |
250 | 243, 249 | eqneltrd 2548 |
. . . . . . . . . . . . . . . 16
 
               |
251 | | 2rp 11307 |
. . . . . . . . . . . . . . . . . 18
 |
252 | | pirp 23416 |
. . . . . . . . . . . . . . . . . 18
 |
253 | | rpmulcl 11324 |
. . . . . . . . . . . . . . . . . 18
       |
254 | 251, 252,
253 | mp2an 678 |
. . . . . . . . . . . . . . . . 17
   |
255 | | mod0 12103 |
. . . . . . . . . . . . . . . . 17
   
             |
256 | 11, 254, 255 | sylancl 668 |
. . . . . . . . . . . . . . . 16
 
                     |
257 | 250, 256 | mtbird 303 |
. . . . . . . . . . . . . . 15
 
               |
258 | 257 | neqned 2631 |
. . . . . . . . . . . . . 14
 
               |
259 | 230, 258 | chvarv 2107 |
. . . . . . . . . . . . 13
 
               |
260 | 259 | neneqd 2629 |
. . . . . . . . . . . 12
 
               |
261 | | simpll 760 |
. . . . . . . . . . . . 13
                           |
262 | | simpr 463 |
. . . . . . . . . . . . . 14
                                       |
263 | 222 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
                           |
264 | 57 | recnd 9669 |
. . . . . . . . . . . . . . . 16
   |
265 | 264 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                           |
266 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . 19
   |
267 | 5 | nnred 10624 |
. . . . . . . . . . . . . . . . . . 19
   |
268 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . 21
   |
269 | 268 | rehalfcld 10859 |
. . . . . . . . . . . . . . . . . . . 20
     |
270 | 267, 269 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . 19
       |
271 | 5 | nngt0d 10653 |
. . . . . . . . . . . . . . . . . . 19
   |
272 | 251 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
273 | 272 | rpreccld 11351 |
. . . . . . . . . . . . . . . . . . . 20
     |
274 | 267, 273 | ltaddrpd 11371 |
. . . . . . . . . . . . . . . . . . 19
       |
275 | 266, 267,
270, 271, 274 | lttrd 9796 |
. . . . . . . . . . . . . . . . . 18
       |
276 | 275 | gt0ne0d 10178 |
. . . . . . . . . . . . . . . . 17
       |
277 | 41, 276 | jca 535 |
. . . . . . . . . . . . . . . 16
             |
278 | 277 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                                     |
279 | | mulcan 10249 |
. . . . . . . . . . . . . . 15
 
     
    
            
   |
280 | 263, 265,
278, 279 | syl3anc 1268 |
. . . . . . . . . . . . . 14
                                     
   |
281 | 262, 280 | mpbid 214 |
. . . . . . . . . . . . 13
                           |
282 | | oveq1 6297 |
. . . . . . . . . . . . . 14
 
         |
283 | | dirkercncflem2.ymod |
. . . . . . . . . . . . . 14
       |
284 | 282, 283 | sylan9eqr 2507 |
. . . . . . . . . . . . 13
 
 
     |
285 | 261, 281,
284 | syl2anc 667 |
. . . . . . . . . . . 12
                               |
286 | 260, 285 | mtand 665 |
. . . . . . . . . . 11
 
                       |
287 | 41, 264 | mulcld 9663 |
. . . . . . . . . . . . 13
         |
288 | 287 | adantr 467 |
. . . . . . . . . . . 12
 
                 |
289 | | elsnc2g 3998 |
. . . . . . . . . . . 12
                                     |
290 | 288, 289 | syl 17 |
. . . . . . . . . . 11
 
                       
 
             |
291 | 286, 290 | mtbird 303 |
. . . . . . . . . 10
 
                         |
292 | 224, 291 | eldifd 3415 |
. . . . . . . . 9
 
                           |
293 | 225, 292 | eqeltrd 2529 |
. . . . . . . 8
 
                                         |
294 | | sinf 14178 |
. . . . . . . . . . . 12
     |
295 | 294 | fdmi 5734 |
. . . . . . . . . . 11
 |
296 | 295 | eqcomi 2460 |
. . . . . . . . . 10
 |
297 | 296 | a1i 11 |
. . . . . . . . 9
 
        
  |
298 | 297 | difeq1d 3550 |
. . . . . . . 8
 
                               |
299 | 293, 298 | eleqtrd 2531 |
. . . . . . 7
 
                                         |
300 | 299 | ralrimiva 2802 |
. . . . . 6
      
                        
           |
301 | | fnfvrnss 6051 |
. . . . . 6
       
                                                          
               
            |
302 | 210, 300,
301 | syl2anc 667 |
. . . . 5
                             |
303 | | uncom 3578 |
. . . . . . . . . 10
     
                   |
304 | 303 | a1i 11 |
. . . . . . . . 9
               
           |
305 | 27 | snssd 4117 |
. . . . . . . . . 10
         |
306 | | undif 3848 |
. . . . . . . . . 10
      
  
    
          |
307 | 305, 306 | sylib 200 |
. . . . . . . . 9
                   |
308 | 304, 307 | eqtrd 2485 |
. . . . . . . 8
                   |
309 | 308 | mpteq1d 4484 |
. . . . . . 7
                                                                                     |
310 | | iftrue 3887 |
. . . . . . . . . . . . 13
  
              
                      |
311 | | oveq2 6298 |
. . . . . . . . . . . . 13
               |
312 | 310, 311 | eqtr4d 2488 |
. . . . . . . . . . . 12
  
              
                      |
313 | 312 | adantl 468 |
. . . . . . . . . . 11
          
              
                      |
314 | | iffalse 3890 |
. . . . . . . . . . . . 13
                 
                                    |
315 | 314 | adantl 468 |
. . . . . . . . . . . 12
       
                                                      |
316 | | eqidd 2452 |
. . . . . . . . . . . . 13
       
      
                            |
317 | | oveq2 6298 |
. . . . . . . . . . . . . 14
               |
318 | 317 | adantl 468 |
. . . . . . . . . . . . 13
   
    

               |
319 | | simpl 459 |
. . . . . . . . . . . . . . 15
     

      |
320 | | id 22 |
. . . . . . . . . . . . . . . . 17

  |
321 | | elsn 3982 |
. . . . . . . . . . . . . . . . 17
     |
322 | 320, 321 | sylnibr 307 |
. . . . . . . . . . . . . . . 16

    |
323 | 322 | adantl 468 |
. . . . . . . . . . . . . . 15
     

    |
324 | 319, 323 | eldifd 3415 |
. . . . . . . . . . . . . 14
     

          |
325 | 324 | adantll 720 |
. . . . . . . . . . . . 13
       
           |
326 | 41 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
      |
327 | 220 | recnd 9669 |
. . . . . . . . . . . . . . . 16
       |
328 | 327 | adantl 468 |
. . . . . . . . . . . . . . 15
 
    
  |
329 | 326, 328 | mulcld 9663 |
. . . . . . . . . . . . . 14
 
    
 
      |
330 | 329 | adantr 467 |
. . . . . . . . . . . . 13
       
         |
331 | 316, 318,
325, 330 | fvmptd 5954 |
. . . . . . . . . . . 12
       
                             |
332 | 315, 331 | eqtrd 2485 |
. . . . . . . . . . 11
       
                                        |
333 | 313, 332 | pm2.61dan 800 |
. . . . . . . . . 10
 
    
                                       |
334 | 333 | mpteq2dva 4489 |
. . . . . . . . 9
                                                    |
335 | | ioosscn 37591 |
. . . . . . . . . . . . . 14
     |
336 | | resmpt 5154 |
. . . . . . . . . . . . . 14
    
        
                   |
337 | 335, 336 | ax-mp 5 |
. . . . . . . . . . . . 13
        
                  |
338 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
                 |
339 | 338 | mulc1cncf 21937 |
. . . . . . . . . . . . . . . 16
                   |
340 | 41, 339 | syl 17 |
. . . . . . . . . . . . . . 15
               |
341 | 51 | cnfldtop 21804 |
. . . . . . . . . . . . . . . . . . 19
  ℂfld  |
342 | | unicntop 37371 |
. . . . . . . . . . . . . . . . . . . 20
   ℂfld |
343 | 342 | restid 15332 |
. . . . . . . . . . . . . . . . . . 19
   ℂfld    ℂfld
↾t    ℂfld  |
344 | 341, 343 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
   ℂfld ↾t    ℂfld |
345 | 344 | eqcomi 2460 |
. . . . . . . . . . . . . . . . 17
  ℂfld    ℂfld ↾t   |
346 | 51, 345, 345 | cncfcn 21941 |
. . . . . . . . . . . . . . . 16
 
        ℂfld
  ℂfld   |
347 | 74, 75, 346 | sylancr 669 |
. . . . . . . . . . . . . . 15
        ℂfld   ℂfld   |
348 | 340, 347 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
            ℂfld
  ℂfld   |
349 | 2, 37 | syl5ss 3443 |
. . . . . . . . . . . . . 14
    
  |
350 | 342 | cnrest 20301 |
. . . . . . . . . . . . . 14
             ℂfld
  ℂfld     
        
         ℂfld ↾t        ℂfld   |
351 | 348, 349,
350 | syl2anc 667 |
. . . . . . . . . . . . 13
                   ℂfld
↾t        ℂfld   |
352 | 337, 351 | syl5eqelr 2534 |
. . . . . . . . . . . 12
                 ℂfld
↾t        ℂfld   |
353 | 51 | cnfldtopon 21803 |
. . . . . . . . . . . . . 14
  ℂfld TopOn   |
354 | | resttopon 20177 |
. . . . . . . . . . . . . 14
    ℂfld
TopOn      
   ℂfld ↾t      TopOn        |
355 | 353, 349,
354 | sylancr 669 |
. . . . . . . . . . . . 13
    ℂfld
↾t      TopOn        |
356 | | cncnp 20296 |
. . . . . . . . . . . . 13
     ℂfld
↾t      TopOn        ℂfld
TopOn                    ℂfld ↾t        ℂfld
                                            ℂfld ↾t        ℂfld        |
357 | 355, 353,
356 | sylancl 668 |
. . . . . . . . . . . 12
                  ℂfld ↾t        ℂfld
                                            ℂfld ↾t        ℂfld        |
358 | 352, 357 | mpbid 214 |
. . . . . . . . . . 11
                      
                      ℂfld
↾t        ℂfld       |
359 | 358 | simprd 465 |
. . . . . . . . . 10
                        ℂfld ↾t        ℂfld      |
360 | | fveq2 5865 |
. . . . . . . . . . . 12
      ℂfld ↾t        ℂfld         ℂfld
↾t        ℂfld      |
361 | 360 | eleq2d 2514 |
. . . . . . . . . . 11
                   ℂfld ↾t        ℂfld                     ℂfld ↾t        ℂfld       |
362 | 361 | rspccva 3149 |
. . . . . . . . . 10
                         ℂfld ↾t        ℂfld   
    
                 ℂfld ↾t        ℂfld      |
363 | 359, 27, 362 | syl2anc 667 |
. . . . . . . . 9
                  ℂfld ↾t        ℂfld      |
364 | 334, 363 | eqeltrd 2529 |
. . . . . . . 8
                                           ℂfld
↾t        ℂfld      |
365 | 308 | eqcomd 2457 |
. . . . . . . . . . 11
          
        |
366 | 365 | oveq2d 6306 |
. . . . . . . . . 10
    ℂfld
↾t         ℂfld
↾t                |
367 | 366 | oveq1d 6305 |
. . . . . . . . 9
     ℂfld ↾t        ℂfld     ℂfld
↾t                ℂfld   |
368 | 367 | fveq1d 5867 |
. . . . . . . 8
      ℂfld ↾t        ℂfld         ℂfld
↾t                ℂfld      |
369 | 364, 368 | eleqtrd 2531 |
. . . . . . 7
                                           ℂfld
↾t                ℂfld      |
370 | 309, 369 | eqeltrd 2529 |
. . . . . 6
                                                   ℂfld
↾t                ℂfld      |
371 | | eqid 2451 |
. . . . . . 7
   ℂfld ↾t                 ℂfld ↾t               |
372 | | eqid 2451 |
. . . . . . 7
                          |