Step | Hyp | Ref
| Expression |
1 | | smcn.u |
. . 3
 |
2 | | smcn.x |
. . . 4
     |
3 | | smcn.s |
. . . 4
      |
4 | 2, 3 | nvsf 26287 |
. . 3
         |
5 | 1, 4 | ax-mp 5 |
. 2
       |
6 | | smcn.t |
. . . . . 6
                   |
7 | | 1rp 11335 |
. . . . . . . 8
 |
8 | | simpr 467 |
. . . . . . . . . . . 12
 
   |
9 | | smcn.n |
. . . . . . . . . . . . 13
 CV   |
10 | 2, 9 | nvcl 26337 |
. . . . . . . . . . . 12
         |
11 | 1, 8, 10 | sylancr 674 |
. . . . . . . . . . 11
 
       |
12 | | abscl 13390 |
. . . . . . . . . . . 12
       |
13 | 12 | adantr 471 |
. . . . . . . . . . 11
 
       |
14 | 11, 13 | readdcld 9696 |
. . . . . . . . . 10
 
             |
15 | 2, 9 | nvge0 26352 |
. . . . . . . . . . . 12
         |
16 | 1, 8, 15 | sylancr 674 |
. . . . . . . . . . 11
 

      |
17 | | absge0 13399 |
. . . . . . . . . . . 12
       |
18 | 17 | adantr 471 |
. . . . . . . . . . 11
 

      |
19 | 11, 13, 16, 18 | addge0d 10217 |
. . . . . . . . . 10
 

            |
20 | 14, 19 | ge0p1rpd 11397 |
. . . . . . . . 9
 
               |
21 | | rpdivcl 11354 |
. . . . . . . . 9
                               |
22 | 20, 21 | sylan 478 |
. . . . . . . 8
                     |
23 | | rpaddcl 11352 |
. . . . . . . 8
                                   |
24 | 7, 22, 23 | sylancr 674 |
. . . . . . 7
                       |
25 | 24 | rpreccld 11380 |
. . . . . 6
                         |
26 | 6, 25 | syl5eqel 2544 |
. . . . 5
       |
27 | | smcn.c |
. . . . . . . . . . . 12
     |
28 | 2, 27 | imsmet 26372 |
. . . . . . . . . . 11
       |
29 | 1, 28 | ax-mp 5 |
. . . . . . . . . 10
     |
30 | 29 | a1i 11 |
. . . . . . . . 9
              
             |
31 | 1 | a1i 11 |
. . . . . . . . . 10
              
         |
32 | | simplll 773 |
. . . . . . . . . 10
              
         |
33 | | simpllr 774 |
. . . . . . . . . 10
              
         |
34 | 2, 3 | nvscl 26296 |
. . . . . . . . . 10
         |
35 | 31, 32, 33, 34 | syl3anc 1276 |
. . . . . . . . 9
              
             |
36 | | simprll 777 |
. . . . . . . . . 10
              
         |
37 | | simprlr 778 |
. . . . . . . . . 10
              
         |
38 | 2, 3 | nvscl 26296 |
. . . . . . . . . 10
         |
39 | 31, 36, 37, 38 | syl3anc 1276 |
. . . . . . . . 9
              
             |
40 | | metcl 21396 |
. . . . . . . . 9
                             |
41 | 30, 35, 39, 40 | syl3anc 1276 |
. . . . . . . 8
              
                     |
42 | 2, 3 | nvscl 26296 |
. . . . . . . . . . 11
         |
43 | 31, 36, 33, 42 | syl3anc 1276 |
. . . . . . . . . 10
              
             |
44 | | metcl 21396 |
. . . . . . . . . 10
                             |
45 | 30, 35, 43, 44 | syl3anc 1276 |
. . . . . . . . 9
              
                     |
46 | | metcl 21396 |
. . . . . . . . . 10
                             |
47 | 30, 43, 39, 46 | syl3anc 1276 |
. . . . . . . . 9
              
                     |
48 | 45, 47 | readdcld 9696 |
. . . . . . . 8
              
                                   |
49 | | rpre 11337 |
. . . . . . . . 9

  |
50 | 49 | ad2antlr 738 |
. . . . . . . 8
              
         |
51 | | mettri 21416 |
. . . . . . . . 9
                    
                                        |
52 | 30, 35, 39, 43, 51 | syl13anc 1278 |
. . . . . . . 8
              
                                               |
53 | 1, 33, 10 | sylancr 674 |
. . . . . . . . . . . 12
              
             |
54 | 32 | abscld 13547 |
. . . . . . . . . . . 12
              
             |
55 | 53, 54 | readdcld 9696 |
. . . . . . . . . . 11
              
                   |
56 | | peano2re 9832 |
. . . . . . . . . . 11
          
              |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
              
                     |
58 | 26 | adantr 471 |
. . . . . . . . . . 11
              
         |
59 | 58 | rpred 11370 |
. . . . . . . . . 10
              
         |
60 | 57, 59 | remulcld 9697 |
. . . . . . . . 9
              
                       |
61 | 32, 36 | subcld 10012 |
. . . . . . . . . . . . 13
              
           |
62 | 61 | abscld 13547 |
. . . . . . . . . . . 12
              
               |
63 | 62, 53 | remulcld 9697 |
. . . . . . . . . . 11
              
                     |
64 | 36 | abscld 13547 |
. . . . . . . . . . . 12
              
             |
65 | | eqid 2462 |
. . . . . . . . . . . . . . 15
         |
66 | 2, 65 | nvmcl 26317 |
. . . . . . . . . . . . . 14
 
           |
67 | 31, 33, 37, 66 | syl3anc 1276 |
. . . . . . . . . . . . 13
              
                 |
68 | 2, 9 | nvcl 26337 |
. . . . . . . . . . . . 13
                         |
69 | 1, 67, 68 | sylancr 674 |
. . . . . . . . . . . 12
              
                     |
70 | 64, 69 | remulcld 9697 |
. . . . . . . . . . 11
              
                           |
71 | 53, 59 | remulcld 9697 |
. . . . . . . . . . 11
              
               |
72 | | peano2re 9832 |
. . . . . . . . . . . . 13
             |
73 | 54, 72 | syl 17 |
. . . . . . . . . . . 12
              
               |
74 | 73, 59 | remulcld 9697 |
. . . . . . . . . . 11
              
                 |
75 | 1, 33, 15 | sylancr 674 |
. . . . . . . . . . . . 13
              
             |
76 | 32, 36 | abssubd 13564 |
. . . . . . . . . . . . . 14
              
                     |
77 | 36, 32 | subcld 10012 |
. . . . . . . . . . . . . . . 16
              
           |
78 | 77 | abscld 13547 |
. . . . . . . . . . . . . . 15
              
               |
79 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . 19

  |
80 | 79 | cnmetdval 21840 |
. . . . . . . . . . . . . . . . . 18
 
   
          |
81 | 32, 36, 80 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
              
                    |
82 | 81, 76 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
              
                    |
83 | | simprrl 779 |
. . . . . . . . . . . . . . . 16
              
              |
84 | 82, 83 | eqbrtrrd 4439 |
. . . . . . . . . . . . . . 15
              
               |
85 | 78, 59, 84 | ltled 9809 |
. . . . . . . . . . . . . 14
              
            
  |
86 | 76, 85 | eqbrtrd 4437 |
. . . . . . . . . . . . 13
              
            
  |
87 | 62, 59, 53, 75, 86 | lemul1ad 10574 |
. . . . . . . . . . . 12
              
                  
        |
88 | 58 | rpcnd 11372 |
. . . . . . . . . . . . 13
              
         |
89 | 53 | recnd 9695 |
. . . . . . . . . . . . 13
              
             |
90 | 88, 89 | mulcomd 9690 |
. . . . . . . . . . . 12
              
                     |
91 | 87, 90 | breqtrd 4441 |
. . . . . . . . . . 11
              
                  
        |
92 | 36 | absge0d 13555 |
. . . . . . . . . . . 12
              
             |
93 | 2, 9 | nvge0 26352 |
. . . . . . . . . . . . 13
          
              |
94 | 1, 67, 93 | sylancr 674 |
. . . . . . . . . . . 12
              
                     |
95 | 54, 78 | readdcld 9696 |
. . . . . . . . . . . . 13
              
                     |
96 | 32, 36 | pncan3d 10015 |
. . . . . . . . . . . . . . 15
              
             |
97 | 96 | fveq2d 5892 |
. . . . . . . . . . . . . 14
              
                     |
98 | 32, 77 | abstrid 13567 |
. . . . . . . . . . . . . 14
              
              
              |
99 | 97, 98 | eqbrtrrd 4439 |
. . . . . . . . . . . . 13
              
          
              |
100 | | 1red 9684 |
. . . . . . . . . . . . . 14
              
         |
101 | | 1re 9668 |
. . . . . . . . . . . . . . . . . . 19
 |
102 | 22 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
              
                       |
103 | | ltaddrp 11365 |
. . . . . . . . . . . . . . . . . . 19
                                   |
104 | 101, 102,
103 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
              
                         |
105 | 24 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
              
                         |
106 | 105 | recgt1d 11384 |
. . . . . . . . . . . . . . . . . 18
              
                                             |
107 | 104, 106 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
              
                           |
108 | 6, 107 | syl5eqbr 4450 |
. . . . . . . . . . . . . . . 16
              
         |
109 | 59, 100, 108 | ltled 9809 |
. . . . . . . . . . . . . . 15
              
         |
110 | 78, 59, 100, 85, 109 | letrd 9818 |
. . . . . . . . . . . . . 14
              
            
  |
111 | 78, 100, 54, 110 | leadd2dd 10256 |
. . . . . . . . . . . . 13
              
                  
        |
112 | 64, 95, 73, 99, 111 | letrd 9818 |
. . . . . . . . . . . 12
              
          
        |
113 | 2, 65, 9, 27 | imsdval 26367 |
. . . . . . . . . . . . . . 15
 
                   |
114 | 31, 33, 37, 113 | syl3anc 1276 |
. . . . . . . . . . . . . 14
              
                         |
115 | | simprrr 780 |
. . . . . . . . . . . . . 14
              
             |
116 | 114, 115 | eqbrtrrd 4439 |
. . . . . . . . . . . . 13
              
                     |
117 | 69, 59, 116 | ltled 9809 |
. . . . . . . . . . . 12
              
                     |
118 | 64, 73, 69, 59, 92, 94, 112, 117 | lemul12ad 10577 |
. . . . . . . . . . 11
              
                        
          |
119 | 63, 70, 71, 74, 91, 118 | le2addd 10260 |
. . . . . . . . . 10
              
                                      
                  |
120 | | eqid 2462 |
. . . . . . . . . . . . . 14
         |
121 | 2, 120, 3, 9, 27 | imsdval2 26368 |
. . . . . . . . . . . . 13
                                                  |
122 | 31, 35, 43, 121 | syl3anc 1276 |
. . . . . . . . . . . 12
              
                                              |
123 | | neg1cn 10741 |
. . . . . . . . . . . . . . . 16
  |
124 | | mulcl 9649 |
. . . . . . . . . . . . . . . 16
         |
125 | 123, 36, 124 | sylancr 674 |
. . . . . . . . . . . . . . 15
              
            |
126 | 2, 120, 3 | nvdir 26301 |
. . . . . . . . . . . . . . 15
     
 
                              |
127 | 31, 32, 125, 33, 126 | syl13anc 1278 |
. . . . . . . . . . . . . 14
              
                                     |
128 | 36 | mulm1d 10098 |
. . . . . . . . . . . . . . . . 17
              
             |
129 | 128 | oveq2d 6331 |
. . . . . . . . . . . . . . . 16
              
                 |
130 | 32, 36 | negsubd 10018 |
. . . . . . . . . . . . . . . 16
              
              |
131 | 129, 130 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
              
                |
132 | 131 | oveq1d 6330 |
. . . . . . . . . . . . . 14
              
                        |
133 | 123 | a1i 11 |
. . . . . . . . . . . . . . . 16
              
          |
134 | 2, 3 | nvsass 26298 |
. . . . . . . . . . . . . . . 16
   
                    |
135 | 31, 133, 36, 33, 134 | syl13anc 1278 |
. . . . . . . . . . . . . . 15
              
                         |
136 | 135 | oveq2d 6331 |
. . . . . . . . . . . . . 14
              
                                                 |
137 | 127, 132,
136 | 3eqtr3d 2504 |
. . . . . . . . . . . . 13
              
                                    |
138 | 137 | fveq2d 5892 |
. . . . . . . . . . . 12
              
                                            |
139 | 2, 3, 9 | nvs 26340 |
. . . . . . . . . . . . 13
                             |
140 | 31, 61, 33, 139 | syl3anc 1276 |
. . . . . . . . . . . 12
              
                               |
141 | 122, 138,
140 | 3eqtr2d 2502 |
. . . . . . . . . . 11
              
                                 |
142 | 2, 65, 9, 27 | imsdval 26367 |
. . . . . . . . . . . . 13
                                             |
143 | 31, 43, 39, 142 | syl3anc 1276 |
. . . . . . . . . . . 12
              
                                         |
144 | 2, 65, 3 | nvmdi 26320 |
. . . . . . . . . . . . . 14
  
 
                              |
145 | 31, 36, 33, 37, 144 | syl13anc 1278 |
. . . . . . . . . . . . 13
              
                                     |
146 | 145 | fveq2d 5892 |
. . . . . . . . . . . 12
              
                                             |
147 | 2, 3, 9 | nvs 26340 |
. . . . . . . . . . . . 13
                                               |
148 | 31, 36, 67, 147 | syl3anc 1276 |
. . . . . . . . . . . 12
              
                                           |
149 | 143, 146,
148 | 3eqtr2d 2502 |
. . . . . . . . . . 11
              
                                       |
150 | 141, 149 | oveq12d 6333 |
. . . . . . . . . 10
              
                                                                   |
151 | 54 | recnd 9695 |
. . . . . . . . . . . . 13
              
             |
152 | | 1cnd 9685 |
. . . . . . . . . . . . 13
              
         |
153 | 89, 151, 152 | addassd 9691 |
. . . . . . . . . . . 12
              
                                 |
154 | 153 | oveq1d 6330 |
. . . . . . . . . . 11
              
                                     |
155 | 73 | recnd 9695 |
. . . . . . . . . . . 12
              
               |
156 | 89, 155, 88 | adddird 9694 |
. . . . . . . . . . 11
              
                                       |
157 | 154, 156 | eqtrd 2496 |
. . . . . . . . . 10
              
                                       |
158 | 119, 150,
157 | 3brtr4d 4447 |
. . . . . . . . 9
              
                                                 |
159 | 57 | recnd 9695 |
. . . . . . . . . . . 12
              
                     |
160 | 105 | rpcnd 11372 |
. . . . . . . . . . . 12
              
                         |
161 | 105 | rpne0d 11375 |
. . . . . . . . . . . 12
              
                         |
162 | 159, 160,
161 | divrecd 10414 |
. . . . . . . . . . 11
              
                                                                       |
163 | 6 | oveq2i 6326 |
. . . . . . . . . . 11
                                               |
164 | 162, 163 | syl6reqr 2515 |
. . . . . . . . . 10
              
                                                     |
165 | | simplr 767 |
. . . . . . . . . . 11
              
         |
166 | 102 | rpred 11370 |
. . . . . . . . . . . . 13
              
                       |
167 | 166 | ltp1d 10565 |
. . . . . . . . . . . 12
              
                    
                  |
168 | 102 | rpcnd 11372 |
. . . . . . . . . . . . 13
              
                       |
169 | 168, 152 | addcomd 9861 |
. . . . . . . . . . . 12
              
                                         |
170 | 167, 169 | breqtrd 4441 |
. . . . . . . . . . 11
              
                    
                  |
171 | 57, 165, 105, 170 | ltdiv23d 11432 |
. . . . . . . . . 10
              
                                       |
172 | 164, 171 | eqbrtrd 4437 |
. . . . . . . . 9
              
                    
  |
173 | 48, 60, 50, 158, 172 | lelttrd 9819 |
. . . . . . . 8
              
                                   |
174 | 41, 48, 50, 52, 173 | lelttrd 9819 |
. . . . . . 7
              
                     |
175 | 174 | expr 624 |
. . . . . 6
      
 
    
 
                    |
176 | 175 | ralrimivva 2821 |
. . . . 5
                                  |
177 | | breq2 4420 |
. . . . . . . . 9
    
 
  
     |
178 | | breq2 4420 |
. . . . . . . . 9
     
       |
179 | 177, 178 | anbi12d 722 |
. . . . . . . 8
                           |
180 | 179 | imbi1d 323 |
. . . . . . 7
        
                 
    
 
                     |
181 | 180 | 2ralbidv 2844 |
. . . . . 6
  
                                                        |
182 | 181 | rspcev 3162 |
. . . . 5
  

    
 
                                                 |
183 | 26, 176, 182 | syl2anc 671 |
. . . 4
       
                           |
184 | 183 | ralrimiva 2814 |
. . 3
 
                                |
185 | 184 | rgen2 2825 |
. 2
     
                          |
186 | | cnxmet 21842 |
. . 3

      |
187 | 2, 27 | imsxmet 26373 |
. . . 4
        |
188 | 1, 187 | ax-mp 5 |
. . 3
      |
189 | | smcn.k |
. . . . 5
  ℂfld |
190 | 189 | cnfldtopn 21851 |
. . . 4
      |
191 | | smcn.j |
. . . 4
     |
192 | 190, 191,
191 | txmetcn 21612 |
. . 3
  
    
    
                  

                                 |
193 | 186, 188,
188, 192 | mp3an 1373 |
. 2
    
        

                               |
194 | 5, 185, 193 | mpbir2an 936 |
1
     |