Step | Hyp | Ref
| Expression |
1 | | 1red 9655 |
. . . 4
  |
2 | | 2re 10676 |
. . . . 5
 |
3 | 2 | a1i 11 |
. . . 4
  |
4 | | 1le2 10820 |
. . . . 5
 |
5 | 4 | a1i 11 |
. . . 4
  |
6 | | reelprrecn 9628 |
. . . . . . 7
    |
7 | 6 | a1i 11 |
. . . . . 6
     |
8 | | recn 9626 |
. . . . . . . . . 10
   |
9 | | 3nn0 10884 |
. . . . . . . . . . 11
 |
10 | | expcl 12287 |
. . . . . . . . . . 11
 
       |
11 | 9, 10 | mpan2 676 |
. . . . . . . . . 10
       |
12 | 8, 11 | syl 17 |
. . . . . . . . 9
       |
13 | | 3cn 10681 |
. . . . . . . . . 10
 |
14 | | 3ne0 10701 |
. . . . . . . . . 10
 |
15 | | divcl 10273 |
. . . . . . . . . 10
     
         |
16 | 13, 14, 15 | mp3an23 1355 |
. . . . . . . . 9
             |
17 | 12, 16 | syl 17 |
. . . . . . . 8
         |
18 | | mulcl 9620 |
. . . . . . . . 9
 
     |
19 | 13, 8, 18 | sylancr 668 |
. . . . . . . 8
     |
20 | 17, 19 | subcld 9983 |
. . . . . . 7
             |
21 | 20 | adantl 468 |
. . . . . 6
              |
22 | | ovex 6316 |
. . . . . . 7
       |
23 | 22 | a1i 11 |
. . . . . 6
          |
24 | 17 | adantl 468 |
. . . . . . 7
          |
25 | | ovex 6316 |
. . . . . . . 8
     |
26 | 25 | a1i 11 |
. . . . . . 7
        |
27 | | divrec2 10284 |
. . . . . . . . . . . . 13
     
                 |
28 | 13, 14, 27 | mp3an23 1355 |
. . . . . . . . . . . 12
                     |
29 | 12, 28 | syl 17 |
. . . . . . . . . . 11
                 |
30 | 29 | mpteq2ia 4484 |
. . . . . . . . . 10
                   |
31 | 30 | oveq2i 6299 |
. . . . . . . . 9
                       |
32 | 12 | adantl 468 |
. . . . . . . . . . 11
        |
33 | | ovex 6316 |
. . . . . . . . . . . 12
       |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
          |
35 | | eqid 2450 |
. . . . . . . . . . . . . . 15
             |
36 | 35, 11 | fmpti 6043 |
. . . . . . . . . . . . . 14
           |
37 | | ssid 3450 |
. . . . . . . . . . . . . 14
 |
38 | | ax-resscn 9593 |
. . . . . . . . . . . . . . 15
 |
39 | | 3nn 10765 |
. . . . . . . . . . . . . . . . . 18
 |
40 | | dvexp 22900 |
. . . . . . . . . . . . . . . . . 18
                     |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
                   |
42 | | 3m1e2 10723 |
. . . . . . . . . . . . . . . . . . . 20
   |
43 | 42 | oveq2i 6299 |
. . . . . . . . . . . . . . . . . . 19
           |
44 | 43 | oveq2i 6299 |
. . . . . . . . . . . . . . . . . 18
               |
45 | 44 | mpteq2i 4485 |
. . . . . . . . . . . . . . . . 17
                   |
46 | 41, 45 | eqtri 2472 |
. . . . . . . . . . . . . . . 16
                 |
47 | 33, 46 | dmmpti 5705 |
. . . . . . . . . . . . . . 15
         |
48 | 38, 47 | sseqtr4i 3464 |
. . . . . . . . . . . . . 14
         |
49 | | dvres3 22861 |
. . . . . . . . . . . . . 14
    
           
          
                      |
50 | 6, 36, 37, 48, 49 | mp4an 678 |
. . . . . . . . . . . . 13
                     |
51 | | resmpt 5153 |
. . . . . . . . . . . . . . 15

      
         |
52 | 38, 51 | ax-mp 5 |
. . . . . . . . . . . . . 14
      
        |
53 | 52 | oveq2i 6299 |
. . . . . . . . . . . . 13
                   |
54 | 46 | reseq1i 5100 |
. . . . . . . . . . . . . 14
        
            |
55 | | resmpt 5153 |
. . . . . . . . . . . . . . 15

        
           |
56 | 38, 55 | ax-mp 5 |
. . . . . . . . . . . . . 14
        
          |
57 | 54, 56 | eqtri 2472 |
. . . . . . . . . . . . 13
        
          |
58 | 50, 53, 57 | 3eqtr3i 2480 |
. . . . . . . . . . . 12
                 |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
                  |
60 | | ax-1cn 9594 |
. . . . . . . . . . . . 13
 |
61 | 60, 13, 14 | divcli 10346 |
. . . . . . . . . . . 12
   |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
    |
63 | 7, 32, 34, 59, 62 | dvmptcmul 22911 |
. . . . . . . . . 10
                          |
64 | 63 | trud 1452 |
. . . . . . . . 9
                         |
65 | | sqcl 12334 |
. . . . . . . . . . . . 13
       |
66 | | mulcl 9620 |
. . . . . . . . . . . . 13
               |
67 | 13, 65, 66 | sylancr 668 |
. . . . . . . . . . . 12
         |
68 | | divrec2 10284 |
. . . . . . . . . . . . 13
       
                     |
69 | 13, 14, 68 | mp3an23 1355 |
. . . . . . . . . . . 12
                           |
70 | 8, 67, 69 | 3syl 18 |
. . . . . . . . . . 11
                     |
71 | | divcan3 10291 |
. . . . . . . . . . . . 13
     
               |
72 | 13, 14, 71 | mp3an23 1355 |
. . . . . . . . . . . 12
                   |
73 | 8, 65, 72 | 3syl 18 |
. . . . . . . . . . 11
               |
74 | 70, 73 | eqtr3d 2486 |
. . . . . . . . . 10
                 |
75 | 74 | mpteq2ia 4484 |
. . . . . . . . 9
                   |
76 | 31, 64, 75 | 3eqtri 2476 |
. . . . . . . 8
                 |
77 | 76 | a1i 11 |
. . . . . . 7
                  |
78 | 19 | adantl 468 |
. . . . . . 7
      |
79 | | 3ex 10682 |
. . . . . . . 8
 |
80 | 79 | a1i 11 |
. . . . . . 7
    |
81 | 8 | adantl 468 |
. . . . . . . . 9
    |
82 | | 1red 9655 |
. . . . . . . . 9
    |
83 | 7 | dvmptid 22904 |
. . . . . . . . 9
        |
84 | 13 | a1i 11 |
. . . . . . . . 9
  |
85 | 7, 81, 82, 83, 84 | dvmptcmul 22911 |
. . . . . . . 8
            |
86 | | 3t1e3 10757 |
. . . . . . . . 9
   |
87 | 86 | mpteq2i 4485 |
. . . . . . . 8
       |
88 | 85, 87 | syl6eq 2500 |
. . . . . . 7
          |
89 | 7, 24, 26, 77, 78, 80, 88 | dvmptsub 22914 |
. . . . . 6
                        |
90 | | 1re 9639 |
. . . . . . . 8
 |
91 | | iccssre 11713 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
  |
92 | 90, 2, 91 | mp2an 677 |
. . . . . . 7
  ![[,] [,]](_icc.gif)   |
93 | 92 | a1i 11 |
. . . . . 6
  ![[,] [,]](_icc.gif) 
  |
94 | | eqid 2450 |
. . . . . . 7
  ℂfld   ℂfld |
95 | 94 | tgioo2 21814 |
. . . . . 6
       ℂfld
↾t   |
96 | | iccntr 21832 |
. . . . . . . 8
 
       
      ![[,] [,]](_icc.gif)         |
97 | 90, 2, 96 | mp2an 677 |
. . . . . . 7
             ![[,] [,]](_icc.gif)        |
98 | 97 | a1i 11 |
. . . . . 6
      
      ![[,] [,]](_icc.gif)         |
99 | 7, 21, 23, 89, 93, 95, 94, 98 | dvmptres2 22909 |
. . . . 5
    ![[,] [,]](_icc.gif)                            |
100 | | ioossicc 11717 |
. . . . . . 7
      ![[,] [,]](_icc.gif)   |
101 | | resmpt 5153 |
. . . . . . 7
       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                            |
102 | 100, 101 | ax-mp 5 |
. . . . . 6
    ![[,] [,]](_icc.gif)        
                  |
103 | 92, 38 | sstri 3440 |
. . . . . . . . 9
  ![[,] [,]](_icc.gif)   |
104 | | resmpt 5153 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif) 
        
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)           |
105 | 103, 104 | ax-mp 5 |
. . . . . . . 8
        
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)          |
106 | | eqid 2450 |
. . . . . . . . . . . 12
                 |
107 | | subcl 9871 |
. . . . . . . . . . . . . 14
     
         |
108 | 13, 107 | mpan2 676 |
. . . . . . . . . . . . 13
             |
109 | 65, 108 | syl 17 |
. . . . . . . . . . . 12
         |
110 | 106, 109 | fmpti 6043 |
. . . . . . . . . . 11
             |
111 | 37, 110, 37 | 3pm3.2i 1185 |
. . . . . . . . . 10
               |
112 | | ovex 6316 |
. . . . . . . . . . 11
           |
113 | | cnelprrecn 9629 |
. . . . . . . . . . . . . 14
    |
114 | 113 | a1i 11 |
. . . . . . . . . . . . 13
     |
115 | 65 | adantl 468 |
. . . . . . . . . . . . 13
        |
116 | | ovex 6316 |
. . . . . . . . . . . . . 14
         |
117 | 116 | a1i 11 |
. . . . . . . . . . . . 13
            |
118 | | 2nn 10764 |
. . . . . . . . . . . . . . 15
 |
119 | | dvexp 22900 |
. . . . . . . . . . . . . . 15
                     |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . . . . . 14
                   |
121 | 120 | a1i 11 |
. . . . . . . . . . . . 13
                    |
122 | 13 | a1i 11 |
. . . . . . . . . . . . 13
    |
123 | | c0ex 9634 |
. . . . . . . . . . . . . 14
 |
124 | 123 | a1i 11 |
. . . . . . . . . . . . 13
    |
125 | 114, 84 | dvmptc 22905 |
. . . . . . . . . . . . 13
        |
126 | 114, 115,
117, 121, 122, 124, 125 | dvmptsub 22914 |
. . . . . . . . . . . 12
                        |
127 | 126 | trud 1452 |
. . . . . . . . . . 11
                       |
128 | 112, 127 | dmmpti 5705 |
. . . . . . . . . 10
           |
129 | | dvcn 22868 |
. . . . . . . . . 10
                                         |
130 | 111, 128,
129 | mp2an 677 |
. . . . . . . . 9
             |
131 | | rescncf 21922 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif) 
                        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        |
132 | 103, 130,
131 | mp2 9 |
. . . . . . . 8
        
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
133 | 105, 132 | eqeltrri 2525 |
. . . . . . 7
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      |
134 | | rescncf 21922 |
. . . . . . 7
       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)                         |
135 | 100, 133,
134 | mp2 9 |
. . . . . 6
    ![[,] [,]](_icc.gif)        
              |
136 | 102, 135 | eqeltrri 2525 |
. . . . 5
                     |
137 | 99, 136 | syl6eqel 2536 |
. . . 4
    ![[,] [,]](_icc.gif)                        |
138 | 100 | a1i 11 |
. . . . . 6
   
  ![[,] [,]](_icc.gif)    |
139 | | ioombl 22511 |
. . . . . . 7
     |
140 | 139 | a1i 11 |
. . . . . 6
      |
141 | 22 | a1i 11 |
. . . . . 6
   ![[,] [,]](_icc.gif)           |
142 | | cniccibl 22791 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)            |
143 | 90, 2, 133, 142 | mp3an 1363 |
. . . . . . 7
   ![[,] [,]](_icc.gif)           |
144 | 143 | a1i 11 |
. . . . . 6
   ![[,] [,]](_icc.gif)            |
145 | 138, 140,
141, 144 | iblss 22755 |
. . . . 5
               |
146 | 99, 145 | eqeltrd 2528 |
. . . 4
    ![[,] [,]](_icc.gif)                 |
147 | | resmpt 5153 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
            
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)               |
148 | 92, 147 | ax-mp 5 |
. . . . . 6
            
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)              |
149 | | eqid 2450 |
. . . . . . . . . 10
                         |
150 | 149, 20 | fmpti 6043 |
. . . . . . . . 9
                 |
151 | | ssid 3450 |
. . . . . . . . 9
 |
152 | 38, 150, 151 | 3pm3.2i 1185 |
. . . . . . . 8
                   |
153 | 89 | trud 1452 |
. . . . . . . . 9
                       |
154 | 22, 153 | dmmpti 5705 |
. . . . . . . 8
               |
155 | | dvcn 22868 |
. . . . . . . 8
                                                     |
156 | 152, 154,
155 | mp2an 677 |
. . . . . . 7
                 |
157 | | rescncf 21922 |
. . . . . . 7
   ![[,] [,]](_icc.gif) 
                                ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        |
158 | 92, 156, 157 | mp2 9 |
. . . . . 6
            
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
159 | 148, 158 | eqeltrri 2525 |
. . . . 5
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)      |
160 | 159 | a1i 11 |
. . . 4
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       |
161 | 1, 3, 5, 137, 146, 160 | ftc2 22989 |
. . 3
           ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)                   |
162 | 161 | trud 1452 |
. 2
           ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)                  |
163 | | itgeq2 22728 |
. . 3
 
          ![[,] [,]](_icc.gif)                                  ![[,] [,]](_icc.gif)                                 |
164 | | oveq1 6295 |
. . . . 5
           |
165 | 164 | oveq1d 6303 |
. . . 4
               |
166 | 99 | trud 1452 |
. . . 4
    ![[,] [,]](_icc.gif)                           |
167 | | ovex 6316 |
. . . 4
       |
168 | 165, 166,
167 | fvmpt 5946 |
. . 3
          ![[,] [,]](_icc.gif)                         |
169 | 163, 168 | mprg 2750 |
. 2
           ![[,] [,]](_icc.gif)                                |
170 | 2 | leidi 10145 |
. . . . . . . . 9
 |
171 | 90, 2 | elicc2i 11697 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif) 
    |
172 | 2, 4, 170, 171 | mpbir3an 1189 |
. . . . . . . 8
  ![[,] [,]](_icc.gif)   |
173 | | oveq1 6295 |
. . . . . . . . . . . 12
           |
174 | 173 | oveq1d 6303 |
. . . . . . . . . . 11
               |
175 | | oveq2 6296 |
. . . . . . . . . . 11
       |
176 | 174, 175 | oveq12d 6306 |
. . . . . . . . . 10
                       |
177 | | cu2 12370 |
. . . . . . . . . . . . 13
     |
178 | 177 | oveq1i 6298 |
. . . . . . . . . . . 12
         |
179 | | 3t2e6 10758 |
. . . . . . . . . . . 12
   |
180 | 178, 179 | oveq12i 6300 |
. . . . . . . . . . 11
               |
181 | | 2cn 10677 |
. . . . . . . . . . . . . . 15
 |
182 | | 6cn 10688 |
. . . . . . . . . . . . . . 15
 |
183 | 181, 182,
13, 14 | divdiri 10361 |
. . . . . . . . . . . . . 14
           |
184 | | 6p2e8 10748 |
. . . . . . . . . . . . . . . 16
   |
185 | 182, 181,
184 | addcomli 9822 |
. . . . . . . . . . . . . . 15
   |
186 | 185 | oveq1i 6298 |
. . . . . . . . . . . . . 14
       |
187 | 182, 13, 181, 14 | divmuli 10358 |
. . . . . . . . . . . . . . . 16
  
    |
188 | 179, 187 | mpbir 213 |
. . . . . . . . . . . . . . 15
   |
189 | 188 | oveq2i 6299 |
. . . . . . . . . . . . . 14
           |
190 | 183, 186,
189 | 3eqtr3i 2480 |
. . . . . . . . . . . . 13
       |
191 | 190 | oveq1i 6298 |
. . . . . . . . . . . 12
           |
192 | 181, 13, 14 | divcli 10346 |
. . . . . . . . . . . . 13
   |
193 | | subsub3 9903 |
. . . . . . . . . . . . 13
   
               |
194 | 192, 182,
181, 193 | mp3an 1363 |
. . . . . . . . . . . 12
             |
195 | 191, 194 | eqtr4i 2475 |
. . . . . . . . . . 11
           |
196 | | 4cn 10684 |
. . . . . . . . . . . . 13
 |
197 | | 4p2e6 10741 |
. . . . . . . . . . . . . 14
   |
198 | 196, 181,
197 | addcomli 9822 |
. . . . . . . . . . . . 13
   |
199 | 182, 181,
196, 198 | subaddrii 9961 |
. . . . . . . . . . . 12
   |
200 | 199 | oveq2i 6299 |
. . . . . . . . . . 11
           |
201 | 180, 195,
200 | 3eqtri 2476 |
. . . . . . . . . 10
               |
202 | 176, 201 | syl6eq 2500 |
. . . . . . . . 9
                 |
203 | | eqid 2450 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)              |
204 | | ovex 6316 |
. . . . . . . . 9
     |
205 | 202, 203,
204 | fvmpt 5946 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                      |
206 | 172, 205 | ax-mp 5 |
. . . . . . 7
    ![[,] [,]](_icc.gif)                     |
207 | 90 | leidi 10145 |
. . . . . . . . 9
 |
208 | 90, 2 | elicc2i 11697 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif) 
    |
209 | 90, 207, 4, 208 | mpbir3an 1189 |
. . . . . . . 8
  ![[,] [,]](_icc.gif)   |
210 | | oveq1 6295 |
. . . . . . . . . . . 12
           |
211 | 210 | oveq1d 6303 |
. . . . . . . . . . 11
               |
212 | | oveq2 6296 |
. . . . . . . . . . 11
       |
213 | 211, 212 | oveq12d 6306 |
. . . . . . . . . 10
                       |
214 | | 3z 10967 |
. . . . . . . . . . . . 13
 |
215 | | 1exp 12298 |
. . . . . . . . . . . . 13
       |
216 | 214, 215 | ax-mp 5 |
. . . . . . . . . . . 12
     |
217 | 216 | oveq1i 6298 |
. . . . . . . . . . 11
         |
218 | 217, 86 | oveq12i 6300 |
. . . . . . . . . 10
               |
219 | 213, 218 | syl6eq 2500 |
. . . . . . . . 9
                 |
220 | | ovex 6316 |
. . . . . . . . 9
     |
221 | 219, 203,
220 | fvmpt 5946 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                      |
222 | 209, 221 | ax-mp 5 |
. . . . . . 7
    ![[,] [,]](_icc.gif)                     |
223 | 206, 222 | oveq12i 6300 |
. . . . . 6
     ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)                            |
224 | | sub4 9916 |
. . . . . . 7
                                 |
225 | 192, 196,
61, 13, 224 | mp4an 678 |
. . . . . 6
                     |
226 | 13, 14 | pm3.2i 457 |
. . . . . . . . 9
   |
227 | | divsubdir 10300 |
. . . . . . . . 9
 
               |
228 | 181, 60, 226, 227 | mp3an 1363 |
. . . . . . . 8
           |
229 | | 2m1e1 10721 |
. . . . . . . . 9
   |
230 | 229 | oveq1i 6298 |
. . . . . . . 8
       |
231 | 228, 230 | eqtr3i 2474 |
. . . . . . 7
         |
232 | | 3p1e4 10732 |
. . . . . . . 8
   |
233 | 196, 13, 60, 232 | subaddrii 9961 |
. . . . . . 7
   |
234 | 231, 233 | oveq12i 6300 |
. . . . . 6
               |
235 | 223, 225,
234 | 3eqtri 2476 |
. . . . 5
     ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)                      |
236 | 13, 14 | dividi 10337 |
. . . . . 6
   |
237 | 236 | oveq2i 6299 |
. . . . 5
           |
238 | 235, 237 | eqtr4i 2475 |
. . . 4
     ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)                        |
239 | | divsubdir 10300 |
. . . . 5
 
               |
240 | 60, 13, 226, 239 | mp3an 1363 |
. . . 4
           |
241 | 238, 240 | eqtr4i 2475 |
. . 3
     ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)                      |
242 | | divneg 10299 |
. . . . 5
 
         |
243 | 181, 13, 14, 242 | mp3an 1363 |
. . . 4
       |
244 | 13, 60 | negsubdi2i 9958 |
. . . . . 6
      |
245 | 42 | negeqi 9865 |
. . . . . 6
     |
246 | 244, 245 | eqtr3i 2474 |
. . . . 5
    |
247 | 246 | oveq1i 6298 |
. . . 4
        |
248 | 243, 247 | eqtr4i 2475 |
. . 3
        |
249 | 241, 248 | eqtr4i 2475 |
. 2
     ![[,] [,]](_icc.gif)                    ![[,] [,]](_icc.gif)                     |
250 | 162, 169,
249 | 3eqtr3i 2480 |
1
                 |