Step | Hyp | Ref
| Expression |
1 | | 1red 10055 |
. . . 4
|
2 | | 2re 11090 |
. . . . 5
|
3 | 2 | a1i 11 |
. . . 4
|
4 | | 1le2 11241 |
. . . . 5
|
5 | 4 | a1i 11 |
. . . 4
|
6 | | reelprrecn 10028 |
. . . . . . 7
|
7 | 6 | a1i 11 |
. . . . . 6
|
8 | | recn 10026 |
. . . . . . . . . 10
|
9 | | 3nn0 11310 |
. . . . . . . . . . 11
|
10 | | expcl 12878 |
. . . . . . . . . . 11
|
11 | 9, 10 | mpan2 707 |
. . . . . . . . . 10
|
12 | 8, 11 | syl 17 |
. . . . . . . . 9
|
13 | | 3cn 11095 |
. . . . . . . . . 10
|
14 | | 3ne0 11115 |
. . . . . . . . . 10
|
15 | | divcl 10691 |
. . . . . . . . . 10
|
16 | 13, 14, 15 | mp3an23 1416 |
. . . . . . . . 9
|
17 | 12, 16 | syl 17 |
. . . . . . . 8
|
18 | | mulcl 10020 |
. . . . . . . . 9
|
19 | 13, 8, 18 | sylancr 695 |
. . . . . . . 8
|
20 | 17, 19 | subcld 10392 |
. . . . . . 7
|
21 | 20 | adantl 482 |
. . . . . 6
|
22 | | ovexd 6680 |
. . . . . 6
|
23 | 17 | adantl 482 |
. . . . . . 7
|
24 | | ovexd 6680 |
. . . . . . 7
|
25 | | divrec2 10702 |
. . . . . . . . . . . . 13
|
26 | 13, 14, 25 | mp3an23 1416 |
. . . . . . . . . . . 12
|
27 | 12, 26 | syl 17 |
. . . . . . . . . . 11
|
28 | 27 | mpteq2ia 4740 |
. . . . . . . . . 10
|
29 | 28 | oveq2i 6661 |
. . . . . . . . 9
|
30 | 12 | adantl 482 |
. . . . . . . . . . 11
|
31 | | ovexd 6680 |
. . . . . . . . . . 11
|
32 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
33 | 32, 11 | fmpti 6383 |
. . . . . . . . . . . . . 14
|
34 | | ssid 3624 |
. . . . . . . . . . . . . 14
|
35 | | ax-resscn 9993 |
. . . . . . . . . . . . . . 15
|
36 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
37 | | 3nn 11186 |
. . . . . . . . . . . . . . . . . 18
|
38 | | dvexp 23716 |
. . . . . . . . . . . . . . . . . 18
|
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
40 | | 3m1e2 11137 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 41 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . 18
|
43 | 42 | mpteq2i 4741 |
. . . . . . . . . . . . . . . . 17
|
44 | 39, 43 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
|
45 | 36, 44 | dmmpti 6023 |
. . . . . . . . . . . . . . 15
|
46 | 35, 45 | sseqtr4i 3638 |
. . . . . . . . . . . . . 14
|
47 | | dvres3 23677 |
. . . . . . . . . . . . . 14
|
48 | 6, 33, 34, 46, 47 | mp4an 709 |
. . . . . . . . . . . . 13
|
49 | | resmpt 5449 |
. . . . . . . . . . . . . . 15
|
50 | 35, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
51 | 50 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
52 | 44 | reseq1i 5392 |
. . . . . . . . . . . . . 14
|
53 | | resmpt 5449 |
. . . . . . . . . . . . . . 15
|
54 | 35, 53 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
55 | 52, 54 | eqtri 2644 |
. . . . . . . . . . . . 13
|
56 | 48, 51, 55 | 3eqtr3i 2652 |
. . . . . . . . . . . 12
|
57 | 56 | a1i 11 |
. . . . . . . . . . 11
|
58 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
59 | 58, 13, 14 | divcli 10767 |
. . . . . . . . . . . 12
|
60 | 59 | a1i 11 |
. . . . . . . . . . 11
|
61 | 7, 30, 31, 57, 60 | dvmptcmul 23727 |
. . . . . . . . . 10
|
62 | 61 | trud 1493 |
. . . . . . . . 9
|
63 | | sqcl 12925 |
. . . . . . . . . . . . 13
|
64 | | mulcl 10020 |
. . . . . . . . . . . . 13
|
65 | 13, 63, 64 | sylancr 695 |
. . . . . . . . . . . 12
|
66 | | divrec2 10702 |
. . . . . . . . . . . . 13
|
67 | 13, 14, 66 | mp3an23 1416 |
. . . . . . . . . . . 12
|
68 | 8, 65, 67 | 3syl 18 |
. . . . . . . . . . 11
|
69 | | divcan3 10711 |
. . . . . . . . . . . . 13
|
70 | 13, 14, 69 | mp3an23 1416 |
. . . . . . . . . . . 12
|
71 | 8, 63, 70 | 3syl 18 |
. . . . . . . . . . 11
|
72 | 68, 71 | eqtr3d 2658 |
. . . . . . . . . 10
|
73 | 72 | mpteq2ia 4740 |
. . . . . . . . 9
|
74 | 29, 62, 73 | 3eqtri 2648 |
. . . . . . . 8
|
75 | 74 | a1i 11 |
. . . . . . 7
|
76 | 19 | adantl 482 |
. . . . . . 7
|
77 | | 3ex 11096 |
. . . . . . . 8
|
78 | 77 | a1i 11 |
. . . . . . 7
|
79 | 8 | adantl 482 |
. . . . . . . . 9
|
80 | | 1red 10055 |
. . . . . . . . 9
|
81 | 7 | dvmptid 23720 |
. . . . . . . . 9
|
82 | 13 | a1i 11 |
. . . . . . . . 9
|
83 | 7, 79, 80, 81, 82 | dvmptcmul 23727 |
. . . . . . . 8
|
84 | | 3t1e3 11178 |
. . . . . . . . 9
|
85 | 84 | mpteq2i 4741 |
. . . . . . . 8
|
86 | 83, 85 | syl6eq 2672 |
. . . . . . 7
|
87 | 7, 23, 24, 75, 76, 78, 86 | dvmptsub 23730 |
. . . . . 6
|
88 | | 1re 10039 |
. . . . . . . 8
|
89 | | iccssre 12255 |
. . . . . . . 8
|
90 | 88, 2, 89 | mp2an 708 |
. . . . . . 7
|
91 | 90 | a1i 11 |
. . . . . 6
|
92 | | eqid 2622 |
. . . . . . 7
ℂfld ℂfld |
93 | 92 | tgioo2 22606 |
. . . . . 6
ℂfld
↾t |
94 | | iccntr 22624 |
. . . . . . . 8
|
95 | 88, 2, 94 | mp2an 708 |
. . . . . . 7
|
96 | 95 | a1i 11 |
. . . . . 6
|
97 | 7, 21, 22, 87, 91, 93, 92, 96 | dvmptres2 23725 |
. . . . 5
|
98 | | ioossicc 12259 |
. . . . . . 7
|
99 | | resmpt 5449 |
. . . . . . 7
|
100 | 98, 99 | ax-mp 5 |
. . . . . 6
|
101 | 90, 35 | sstri 3612 |
. . . . . . . . 9
|
102 | | resmpt 5449 |
. . . . . . . . 9
|
103 | 101, 102 | ax-mp 5 |
. . . . . . . 8
|
104 | | eqid 2622 |
. . . . . . . . . . . 12
|
105 | | subcl 10280 |
. . . . . . . . . . . . . 14
|
106 | 13, 105 | mpan2 707 |
. . . . . . . . . . . . 13
|
107 | 63, 106 | syl 17 |
. . . . . . . . . . . 12
|
108 | 104, 107 | fmpti 6383 |
. . . . . . . . . . 11
|
109 | 34, 108, 34 | 3pm3.2i 1239 |
. . . . . . . . . 10
|
110 | | ovex 6678 |
. . . . . . . . . . 11
|
111 | | cnelprrecn 10029 |
. . . . . . . . . . . . . 14
|
112 | 111 | a1i 11 |
. . . . . . . . . . . . 13
|
113 | 63 | adantl 482 |
. . . . . . . . . . . . 13
|
114 | | ovexd 6680 |
. . . . . . . . . . . . 13
|
115 | | 2nn 11185 |
. . . . . . . . . . . . . . 15
|
116 | | dvexp 23716 |
. . . . . . . . . . . . . . 15
|
117 | 115, 116 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
118 | 117 | a1i 11 |
. . . . . . . . . . . . 13
|
119 | 13 | a1i 11 |
. . . . . . . . . . . . 13
|
120 | | c0ex 10034 |
. . . . . . . . . . . . . 14
|
121 | 120 | a1i 11 |
. . . . . . . . . . . . 13
|
122 | 112, 82 | dvmptc 23721 |
. . . . . . . . . . . . 13
|
123 | 112, 113,
114, 118, 119, 121, 122 | dvmptsub 23730 |
. . . . . . . . . . . 12
|
124 | 123 | trud 1493 |
. . . . . . . . . . 11
|
125 | 110, 124 | dmmpti 6023 |
. . . . . . . . . 10
|
126 | | dvcn 23684 |
. . . . . . . . . 10
|
127 | 109, 125,
126 | mp2an 708 |
. . . . . . . . 9
|
128 | | rescncf 22700 |
. . . . . . . . 9
|
129 | 101, 127,
128 | mp2 9 |
. . . . . . . 8
|
130 | 103, 129 | eqeltrri 2698 |
. . . . . . 7
|
131 | | rescncf 22700 |
. . . . . . 7
|
132 | 98, 130, 131 | mp2 9 |
. . . . . 6
|
133 | 100, 132 | eqeltrri 2698 |
. . . . 5
|
134 | 97, 133 | syl6eqel 2709 |
. . . 4
|
135 | 98 | a1i 11 |
. . . . . 6
|
136 | | ioombl 23333 |
. . . . . . 7
|
137 | 136 | a1i 11 |
. . . . . 6
|
138 | | ovexd 6680 |
. . . . . 6
|
139 | | cniccibl 23607 |
. . . . . . . 8
|
140 | 88, 2, 130, 139 | mp3an 1424 |
. . . . . . 7
|
141 | 140 | a1i 11 |
. . . . . 6
|
142 | 135, 137,
138, 141 | iblss 23571 |
. . . . 5
|
143 | 97, 142 | eqeltrd 2701 |
. . . 4
|
144 | | resmpt 5449 |
. . . . . . 7
|
145 | 90, 144 | ax-mp 5 |
. . . . . 6
|
146 | | eqid 2622 |
. . . . . . . . . 10
|
147 | 146, 20 | fmpti 6383 |
. . . . . . . . 9
|
148 | | ssid 3624 |
. . . . . . . . 9
|
149 | 35, 147, 148 | 3pm3.2i 1239 |
. . . . . . . 8
|
150 | | ovex 6678 |
. . . . . . . . 9
|
151 | 87 | trud 1493 |
. . . . . . . . 9
|
152 | 150, 151 | dmmpti 6023 |
. . . . . . . 8
|
153 | | dvcn 23684 |
. . . . . . . 8
|
154 | 149, 152,
153 | mp2an 708 |
. . . . . . 7
|
155 | | rescncf 22700 |
. . . . . . 7
|
156 | 90, 154, 155 | mp2 9 |
. . . . . 6
|
157 | 145, 156 | eqeltrri 2698 |
. . . . 5
|
158 | 157 | a1i 11 |
. . . 4
|
159 | 1, 3, 5, 134, 143, 158 | ftc2 23807 |
. . 3
|
160 | 159 | trud 1493 |
. 2
|
161 | | itgeq2 23544 |
. . 3
|
162 | | oveq1 6657 |
. . . . 5
|
163 | 162 | oveq1d 6665 |
. . . 4
|
164 | 97 | trud 1493 |
. . . 4
|
165 | | ovex 6678 |
. . . 4
|
166 | 163, 164,
165 | fvmpt 6282 |
. . 3
|
167 | 161, 166 | mprg 2926 |
. 2
|
168 | 2 | leidi 10562 |
. . . . . . . . 9
|
169 | 88, 2 | elicc2i 12239 |
. . . . . . . . 9
|
170 | 2, 4, 168, 169 | mpbir3an 1244 |
. . . . . . . 8
|
171 | | oveq1 6657 |
. . . . . . . . . . . 12
|
172 | 171 | oveq1d 6665 |
. . . . . . . . . . 11
|
173 | | oveq2 6658 |
. . . . . . . . . . 11
|
174 | 172, 173 | oveq12d 6668 |
. . . . . . . . . 10
|
175 | | cu2 12963 |
. . . . . . . . . . . . 13
|
176 | 175 | oveq1i 6660 |
. . . . . . . . . . . 12
|
177 | | 3t2e6 11179 |
. . . . . . . . . . . 12
|
178 | 176, 177 | oveq12i 6662 |
. . . . . . . . . . 11
|
179 | | 2cn 11091 |
. . . . . . . . . . . . . . 15
|
180 | | 6cn 11102 |
. . . . . . . . . . . . . . 15
|
181 | 179, 180,
13, 14 | divdiri 10782 |
. . . . . . . . . . . . . 14
|
182 | | 6p2e8 11169 |
. . . . . . . . . . . . . . . 16
|
183 | 180, 179,
182 | addcomli 10228 |
. . . . . . . . . . . . . . 15
|
184 | 183 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
185 | 180, 13, 179, 14 | divmuli 10779 |
. . . . . . . . . . . . . . . 16
|
186 | 177, 185 | mpbir 221 |
. . . . . . . . . . . . . . 15
|
187 | 186 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
188 | 181, 184,
187 | 3eqtr3i 2652 |
. . . . . . . . . . . . 13
|
189 | 188 | oveq1i 6660 |
. . . . . . . . . . . 12
|
190 | 179, 13, 14 | divcli 10767 |
. . . . . . . . . . . . 13
|
191 | | subsub3 10313 |
. . . . . . . . . . . . 13
|
192 | 190, 180,
179, 191 | mp3an 1424 |
. . . . . . . . . . . 12
|
193 | 189, 192 | eqtr4i 2647 |
. . . . . . . . . . 11
|
194 | | 4cn 11098 |
. . . . . . . . . . . . 13
|
195 | | 4p2e6 11162 |
. . . . . . . . . . . . . 14
|
196 | 194, 179,
195 | addcomli 10228 |
. . . . . . . . . . . . 13
|
197 | 180, 179,
194, 196 | subaddrii 10370 |
. . . . . . . . . . . 12
|
198 | 197 | oveq2i 6661 |
. . . . . . . . . . 11
|
199 | 178, 193,
198 | 3eqtri 2648 |
. . . . . . . . . 10
|
200 | 174, 199 | syl6eq 2672 |
. . . . . . . . 9
|
201 | | eqid 2622 |
. . . . . . . . 9
|
202 | | ovex 6678 |
. . . . . . . . 9
|
203 | 200, 201,
202 | fvmpt 6282 |
. . . . . . . 8
|
204 | 170, 203 | ax-mp 5 |
. . . . . . 7
|
205 | 88 | leidi 10562 |
. . . . . . . . 9
|
206 | 88, 2 | elicc2i 12239 |
. . . . . . . . 9
|
207 | 88, 205, 4, 206 | mpbir3an 1244 |
. . . . . . . 8
|
208 | | oveq1 6657 |
. . . . . . . . . . . 12
|
209 | 208 | oveq1d 6665 |
. . . . . . . . . . 11
|
210 | | oveq2 6658 |
. . . . . . . . . . 11
|
211 | 209, 210 | oveq12d 6668 |
. . . . . . . . . 10
|
212 | | 3z 11410 |
. . . . . . . . . . . . 13
|
213 | | 1exp 12889 |
. . . . . . . . . . . . 13
|
214 | 212, 213 | ax-mp 5 |
. . . . . . . . . . . 12
|
215 | 214 | oveq1i 6660 |
. . . . . . . . . . 11
|
216 | 215, 84 | oveq12i 6662 |
. . . . . . . . . 10
|
217 | 211, 216 | syl6eq 2672 |
. . . . . . . . 9
|
218 | | ovex 6678 |
. . . . . . . . 9
|
219 | 217, 201,
218 | fvmpt 6282 |
. . . . . . . 8
|
220 | 207, 219 | ax-mp 5 |
. . . . . . 7
|
221 | 204, 220 | oveq12i 6662 |
. . . . . 6
|
222 | | sub4 10326 |
. . . . . . 7
|
223 | 190, 194,
59, 13, 222 | mp4an 709 |
. . . . . 6
|
224 | 13, 14 | pm3.2i 471 |
. . . . . . . . 9
|
225 | | divsubdir 10721 |
. . . . . . . . 9
|
226 | 179, 58, 224, 225 | mp3an 1424 |
. . . . . . . 8
|
227 | | 2m1e1 11135 |
. . . . . . . . 9
|
228 | 227 | oveq1i 6660 |
. . . . . . . 8
|
229 | 226, 228 | eqtr3i 2646 |
. . . . . . 7
|
230 | | 3p1e4 11153 |
. . . . . . . 8
|
231 | 194, 13, 58, 230 | subaddrii 10370 |
. . . . . . 7
|
232 | 229, 231 | oveq12i 6662 |
. . . . . 6
|
233 | 221, 223,
232 | 3eqtri 2648 |
. . . . 5
|
234 | 13, 14 | dividi 10758 |
. . . . . 6
|
235 | 234 | oveq2i 6661 |
. . . . 5
|
236 | 233, 235 | eqtr4i 2647 |
. . . 4
|
237 | | divsubdir 10721 |
. . . . 5
|
238 | 58, 13, 224, 237 | mp3an 1424 |
. . . 4
|
239 | 236, 238 | eqtr4i 2647 |
. . 3
|
240 | | divneg 10719 |
. . . . 5
|
241 | 179, 13, 14, 240 | mp3an 1424 |
. . . 4
|
242 | 13, 58 | negsubdi2i 10367 |
. . . . . 6
|
243 | 40 | negeqi 10274 |
. . . . . 6
|
244 | 242, 243 | eqtr3i 2646 |
. . . . 5
|
245 | 244 | oveq1i 6660 |
. . . 4
|
246 | 241, 245 | eqtr4i 2647 |
. . 3
|
247 | 239, 246 | eqtr4i 2647 |
. 2
|
248 | 160, 167,
247 | 3eqtr3i 2652 |
1
|