Step | Hyp | Ref
| Expression |
1 | | 1elunit 12291 |
. . 3
|
2 | | 0elunit 12290 |
. . 3
|
3 | | 0red 10041 |
. . . 4
|
4 | | 1red 10055 |
. . . 4
|
5 | | eqid 2622 |
. . . . 5
ℂfld ℂfld |
6 | 5 | subcn 22669 |
. . . . . 6
ℂfld ℂfld ℂfld |
7 | 6 | a1i 11 |
. . . . 5
ℂfld
ℂfld ℂfld |
8 | | lgamgulm.r |
. . . . . . . . . . 11
|
9 | | lgamgulm.u |
. . . . . . . . . . 11
|
10 | 8, 9 | lgamgulmlem1 24755 |
. . . . . . . . . 10
|
11 | | lgamgulm.a |
. . . . . . . . . 10
|
12 | 10, 11 | sseldd 3604 |
. . . . . . . . 9
|
13 | 12 | eldifad 3586 |
. . . . . . . 8
|
14 | | lgamgulm.n |
. . . . . . . . . 10
|
15 | 14 | nnred 11035 |
. . . . . . . . 9
|
16 | 15 | recnd 10068 |
. . . . . . . 8
|
17 | 14 | nnne0d 11065 |
. . . . . . . 8
|
18 | 13, 16, 17 | divcld 10801 |
. . . . . . 7
|
19 | | unitssre 12319 |
. . . . . . . . 9
|
20 | | ax-resscn 9993 |
. . . . . . . . 9
|
21 | 19, 20 | sstri 3612 |
. . . . . . . 8
|
22 | 21 | a1i 11 |
. . . . . . 7
|
23 | | ssid 3624 |
. . . . . . . 8
|
24 | 23 | a1i 11 |
. . . . . . 7
|
25 | | cncfmptc 22714 |
. . . . . . 7
|
26 | 18, 22, 24, 25 | syl3anc 1326 |
. . . . . 6
|
27 | | cncfmptid 22715 |
. . . . . . 7
|
28 | 21, 24, 27 | sylancr 695 |
. . . . . 6
|
29 | 26, 28 | mulcncf 23215 |
. . . . 5
|
30 | 18 | adantr 481 |
. . . . . . . . . . 11
|
31 | | simpr 477 |
. . . . . . . . . . . . 13
|
32 | 19, 31 | sseldi 3601 |
. . . . . . . . . . . 12
|
33 | 32 | recnd 10068 |
. . . . . . . . . . 11
|
34 | 30, 33 | mulcld 10060 |
. . . . . . . . . 10
|
35 | | 1cnd 10056 |
. . . . . . . . . 10
|
36 | 34, 35 | addcld 10059 |
. . . . . . . . 9
|
37 | | rere 13862 |
. . . . . . . . . . . 12
|
38 | 37 | adantl 482 |
. . . . . . . . . . 11
|
39 | 36 | recld 13934 |
. . . . . . . . . . . . 13
|
40 | 34 | recld 13934 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | 40 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | 41 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
43 | 34 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
44 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . 19
|
45 | | absrele 14048 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 34, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 44 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . 20
|
48 | 8 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
50 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
51 | 49, 50 | nndivred 11069 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | 18 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
54 | 30 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
55 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
56 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
57 | 55, 56 | elicc2i 12239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
58 | 57 | simp2bi 1077 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
60 | 13, 16, 17 | absdivd 14194 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
61 | 14 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
62 | 61 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
63 | 15, 62 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
64 | 63 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
65 | 60, 64 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
66 | 13 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
67 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
68 | 67 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
69 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
70 | 69 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
71 | 70 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
72 | 71 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
73 | 68, 72 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
74 | 73, 9 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
75 | 74 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
76 | 11, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
77 | 76 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
78 | 66, 48, 61, 77 | lediv1dd 11930 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
79 | 65, 78 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
80 | 79 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
81 | 57 | simp3bi 1078 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | 53, 51, 32, 44, 54, 59, 80, 82 | lemul12ad 10966 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 30, 33 | absmuld 14193 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
85 | 32, 59 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | 84, 86 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 51 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
89 | 88 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . 22
|
90 | 83, 87, 89 | 3brtr3d 4684 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | | lgamgulm.l |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
92 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
94 | 48, 15, 93 | lemuldiv2d 11922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
95 | 91, 94 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
96 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
97 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
99 | 16, 96, 98 | divrecd 10804 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
100 | 95, 99 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 4 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
102 | 48, 101, 61 | ledivmuld 11925 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
103 | 100, 102 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 43, 51, 47, 90, 104 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | | halflt1 11250 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 43, 47, 44, 105, 107 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 42, 43, 44, 46, 108 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . 18
|
110 | 40, 44 | absltd 14168 |
. . . . . . . . . . . . . . . . . 18
|
111 | 109, 110 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
112 | 111 | simpld 475 |
. . . . . . . . . . . . . . . 16
|
113 | 44 | renegcld 10457 |
. . . . . . . . . . . . . . . . 17
|
114 | 113, 40 | posdifd 10614 |
. . . . . . . . . . . . . . . 16
|
115 | 112, 114 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
116 | 41, 35 | subnegd 10399 |
. . . . . . . . . . . . . . 15
|
117 | 115, 116 | breqtrd 4679 |
. . . . . . . . . . . . . 14
|
118 | 34, 35 | readdd 13954 |
. . . . . . . . . . . . . . 15
|
119 | | re1 13894 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
|
121 | 118, 120 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
122 | 117, 121 | breqtrrd 4681 |
. . . . . . . . . . . . 13
|
123 | 39, 122 | elrpd 11869 |
. . . . . . . . . . . 12
|
124 | 123 | adantr 481 |
. . . . . . . . . . 11
|
125 | 38, 124 | eqeltrrd 2702 |
. . . . . . . . . 10
|
126 | 125 | ex 450 |
. . . . . . . . 9
|
127 | | eqid 2622 |
. . . . . . . . . 10
|
128 | 127 | ellogdm 24385 |
. . . . . . . . 9
|
129 | 36, 126, 128 | sylanbrc 698 |
. . . . . . . 8
|
130 | | eqidd 2623 |
. . . . . . . 8
|
131 | 127 | logcn 24393 |
. . . . . . . . . . 11
|
132 | 131 | a1i 11 |
. . . . . . . . . 10
|
133 | | cncff 22696 |
. . . . . . . . . 10
|
134 | 132, 133 | syl 17 |
. . . . . . . . 9
|
135 | 134 | feqmptd 6249 |
. . . . . . . 8
|
136 | | fveq2 6191 |
. . . . . . . 8
|
137 | 129, 130,
135, 136 | fmptco 6396 |
. . . . . . 7
|
138 | | fvres 6207 |
. . . . . . . . 9
|
139 | 129, 138 | syl 17 |
. . . . . . . 8
|
140 | 139 | mpteq2dva 4744 |
. . . . . . 7
|
141 | 137, 140 | eqtrd 2656 |
. . . . . 6
|
142 | | eqid 2622 |
. . . . . . . . 9
|
143 | 129, 142 | fmptd 6385 |
. . . . . . . 8
|
144 | | difss 3737 |
. . . . . . . . 9
|
145 | 5 | addcn 22668 |
. . . . . . . . . . 11
ℂfld ℂfld ℂfld |
146 | 145 | a1i 11 |
. . . . . . . . . 10
ℂfld
ℂfld ℂfld |
147 | | 1cnd 10056 |
. . . . . . . . . . 11
|
148 | | cncfmptc 22714 |
. . . . . . . . . . 11
|
149 | 147, 22, 24, 148 | syl3anc 1326 |
. . . . . . . . . 10
|
150 | 5, 146, 29, 149 | cncfmpt2f 22717 |
. . . . . . . . 9
|
151 | | cncffvrn 22701 |
. . . . . . . . 9
|
152 | 144, 150,
151 | sylancr 695 |
. . . . . . . 8
|
153 | 143, 152 | mpbird 247 |
. . . . . . 7
|
154 | 153, 132 | cncfco 22710 |
. . . . . 6
|
155 | 141, 154 | eqeltrrd 2702 |
. . . . 5
|
156 | 5, 7, 29, 155 | cncfmpt2f 22717 |
. . . 4
|
157 | 20 | a1i 11 |
. . . . . . . 8
|
158 | 19 | a1i 11 |
. . . . . . . 8
|
159 | 127 | logdmn0 24386 |
. . . . . . . . . . 11
|
160 | 129, 159 | syl 17 |
. . . . . . . . . 10
|
161 | 36, 160 | logcld 24317 |
. . . . . . . . 9
|
162 | 34, 161 | subcld 10392 |
. . . . . . . 8
|
163 | 5 | tgioo2 22606 |
. . . . . . . 8
ℂfld
↾t |
164 | | iccntr 22624 |
. . . . . . . . 9
|
165 | 55, 4, 164 | sylancr 695 |
. . . . . . . 8
|
166 | 157, 158,
162, 163, 5, 165 | dvmptntr 23734 |
. . . . . . 7
|
167 | | reelprrecn 10028 |
. . . . . . . . 9
|
168 | 167 | a1i 11 |
. . . . . . . 8
|
169 | 13 | adantr 481 |
. . . . . . . . . 10
|
170 | 16 | adantr 481 |
. . . . . . . . . 10
|
171 | 17 | adantr 481 |
. . . . . . . . . 10
|
172 | 169, 170,
171 | divcld 10801 |
. . . . . . . . 9
|
173 | | ioossicc 12259 |
. . . . . . . . . . 11
|
174 | 173 | sseli 3599 |
. . . . . . . . . 10
|
175 | 174, 33 | sylan2 491 |
. . . . . . . . 9
|
176 | 172, 175 | mulcld 10060 |
. . . . . . . 8
|
177 | 13 | adantr 481 |
. . . . . . . . . . 11
|
178 | 16 | adantr 481 |
. . . . . . . . . . 11
|
179 | 17 | adantr 481 |
. . . . . . . . . . 11
|
180 | 177, 178,
179 | divcld 10801 |
. . . . . . . . . 10
|
181 | 157 | sselda 3603 |
. . . . . . . . . 10
|
182 | 180, 181 | mulcld 10060 |
. . . . . . . . 9
|
183 | | 1cnd 10056 |
. . . . . . . . . . 11
|
184 | 168 | dvmptid 23720 |
. . . . . . . . . . 11
|
185 | 168, 181,
183, 184, 18 | dvmptcmul 23727 |
. . . . . . . . . 10
|
186 | 18 | mulid1d 10057 |
. . . . . . . . . . 11
|
187 | 186 | mpteq2dv 4745 |
. . . . . . . . . 10
|
188 | 185, 187 | eqtrd 2656 |
. . . . . . . . 9
|
189 | 173, 158 | syl5ss 3614 |
. . . . . . . . 9
|
190 | | retop 22565 |
. . . . . . . . . . 11
|
191 | | iooretop 22569 |
. . . . . . . . . . 11
|
192 | | isopn3i 20886 |
. . . . . . . . . . 11
|
193 | 190, 191,
192 | mp2an 708 |
. . . . . . . . . 10
|
194 | 193 | a1i 11 |
. . . . . . . . 9
|
195 | 168, 182,
180, 188, 189, 163, 5, 194 | dvmptres2 23725 |
. . . . . . . 8
|
196 | 174, 161 | sylan2 491 |
. . . . . . . 8
|
197 | | 1cnd 10056 |
. . . . . . . . . . 11
|
198 | 176, 197 | addcld 10059 |
. . . . . . . . . 10
|
199 | 174, 160 | sylan2 491 |
. . . . . . . . . 10
|
200 | 198, 199 | reccld 10794 |
. . . . . . . . 9
|
201 | 200, 172 | mulcld 10060 |
. . . . . . . 8
|
202 | | cnelprrecn 10029 |
. . . . . . . . . 10
|
203 | 202 | a1i 11 |
. . . . . . . . 9
|
204 | 174, 129 | sylan2 491 |
. . . . . . . . 9
|
205 | | eldifi 3732 |
. . . . . . . . . . 11
|
206 | 205 | adantl 482 |
. . . . . . . . . 10
|
207 | 127 | logdmn0 24386 |
. . . . . . . . . . 11
|
208 | 207 | adantl 482 |
. . . . . . . . . 10
|
209 | 206, 208 | logcld 24317 |
. . . . . . . . 9
|
210 | 206, 208 | reccld 10794 |
. . . . . . . . 9
|
211 | 182, 183 | addcld 10059 |
. . . . . . . . . 10
|
212 | | 0cnd 10033 |
. . . . . . . . . . . 12
|
213 | 168, 147 | dvmptc 23721 |
. . . . . . . . . . . 12
|
214 | 168, 182,
180, 188, 183, 212, 213 | dvmptadd 23723 |
. . . . . . . . . . 11
|
215 | 18 | addid1d 10236 |
. . . . . . . . . . . 12
|
216 | 215 | mpteq2dv 4745 |
. . . . . . . . . . 11
|
217 | 214, 216 | eqtrd 2656 |
. . . . . . . . . 10
|
218 | 168, 211,
180, 217, 189, 163, 5, 194 | dvmptres2 23725 |
. . . . . . . . 9
|
219 | | fvres 6207 |
. . . . . . . . . . . . 13
|
220 | 219 | mpteq2ia 4740 |
. . . . . . . . . . . 12
|
221 | 135, 220 | syl6req 2673 |
. . . . . . . . . . 11
|
222 | 221 | oveq2d 6666 |
. . . . . . . . . 10
|
223 | 127 | dvlog 24397 |
. . . . . . . . . 10
|
224 | 222, 223 | syl6eq 2672 |
. . . . . . . . 9
|
225 | | fveq2 6191 |
. . . . . . . . 9
|
226 | | oveq2 6658 |
. . . . . . . . 9
|
227 | 168, 203,
204, 172, 209, 210, 218, 224, 225, 226 | dvmptco 23735 |
. . . . . . . 8
|
228 | 168, 176,
172, 195, 196, 201, 227 | dvmptsub 23730 |
. . . . . . 7
|
229 | 166, 228 | eqtrd 2656 |
. . . . . 6
|
230 | 229 | dmeqd 5326 |
. . . . 5
|
231 | | ovex 6678 |
. . . . . 6
|
232 | | eqid 2622 |
. . . . . 6
|
233 | 231, 232 | dmmpti 6023 |
. . . . 5
|
234 | 230, 233 | syl6eq 2672 |
. . . 4
|
235 | | 2re 11090 |
. . . . . . . . . . 11
|
236 | 235 | a1i 11 |
. . . . . . . . . 10
|
237 | 236, 48 | remulcld 10070 |
. . . . . . . . 9
|
238 | 8 | nnrpd 11870 |
. . . . . . . . . . 11
|
239 | 48, 238 | ltaddrpd 11905 |
. . . . . . . . . 10
|
240 | 48 | recnd 10068 |
. . . . . . . . . . 11
|
241 | 240 | 2timesd 11275 |
. . . . . . . . . 10
|
242 | 239, 241 | breqtrrd 4681 |
. . . . . . . . 9
|
243 | 48, 237, 15, 242, 91 | ltletrd 10197 |
. . . . . . . 8
|
244 | | difrp 11868 |
. . . . . . . . 9
|
245 | 48, 15, 244 | syl2anc 693 |
. . . . . . . 8
|
246 | 243, 245 | mpbid 222 |
. . . . . . 7
|
247 | 246 | rprecred 11883 |
. . . . . 6
|
248 | 14 | nnrecred 11066 |
. . . . . 6
|
249 | 247, 248 | resubcld 10458 |
. . . . 5
|
250 | 48, 249 | remulcld 10070 |
. . . 4
|
251 | 229 | fveq1d 6193 |
. . . . . . 7
|
252 | 251 | fveq2d 6195 |
. . . . . 6
|
253 | 252 | adantr 481 |
. . . . 5
|
254 | | nfv 1843 |
. . . . . . 7
|
255 | | nfcv 2764 |
. . . . . . . . 9
|
256 | | nffvmpt1 6199 |
. . . . . . . . 9
|
257 | 255, 256 | nffv 6198 |
. . . . . . . 8
|
258 | | nfcv 2764 |
. . . . . . . 8
|
259 | | nfcv 2764 |
. . . . . . . 8
|
260 | 257, 258,
259 | nfbr 4699 |
. . . . . . 7
|
261 | 254, 260 | nfim 1825 |
. . . . . 6
|
262 | | eleq1 2689 |
. . . . . . . 8
|
263 | 262 | anbi2d 740 |
. . . . . . 7
|
264 | | fveq2 6191 |
. . . . . . . . 9
|
265 | 264 | fveq2d 6195 |
. . . . . . . 8
|
266 | 265 | breq1d 4663 |
. . . . . . 7
|
267 | 263, 266 | imbi12d 334 |
. . . . . 6
|
268 | | simpr 477 |
. . . . . . . . . 10
|
269 | 232 | fvmpt2 6291 |
. . . . . . . . . 10
|
270 | 268, 231,
269 | sylancl 694 |
. . . . . . . . 9
|
271 | 270 | fveq2d 6195 |
. . . . . . . 8
|
272 | 172, 197,
200 | subdid 10486 |
. . . . . . . . . 10
|
273 | 172 | mulid1d 10057 |
. . . . . . . . . . 11
|
274 | 172, 200 | mulcomd 10061 |
. . . . . . . . . . 11
|
275 | 273, 274 | oveq12d 6668 |
. . . . . . . . . 10
|
276 | 272, 275 | eqtr2d 2657 |
. . . . . . . . 9
|
277 | 276 | fveq2d 6195 |
. . . . . . . 8
|
278 | 169, 170,
171 | absdivd 14194 |
. . . . . . . . . . 11
|
279 | 15 | adantr 481 |
. . . . . . . . . . . . 13
|
280 | 62 | adantr 481 |
. . . . . . . . . . . . 13
|
281 | 279, 280 | absidd 14161 |
. . . . . . . . . . . 12
|
282 | 281 | oveq2d 6666 |
. . . . . . . . . . 11
|
283 | 278, 282 | eqtrd 2656 |
. . . . . . . . . 10
|
284 | 283 | oveq1d 6665 |
. . . . . . . . 9
|
285 | 197, 200 | subcld 10392 |
. . . . . . . . . 10
|
286 | 172, 285 | absmuld 14193 |
. . . . . . . . 9
|
287 | 66 | adantr 481 |
. . . . . . . . . . 11
|
288 | 287 | recnd 10068 |
. . . . . . . . . 10
|
289 | 285 | abscld 14175 |
. . . . . . . . . . 11
|
290 | 289 | recnd 10068 |
. . . . . . . . . 10
|
291 | 288, 290,
170, 171 | div23d 10838 |
. . . . . . . . 9
|
292 | 284, 286,
291 | 3eqtr4d 2666 |
. . . . . . . 8
|
293 | 271, 277,
292 | 3eqtrd 2660 |
. . . . . . 7
|
294 | 48 | adantr 481 |
. . . . . . . . . 10
|
295 | 247 | adantr 481 |
. . . . . . . . . . . 12
|
296 | 248 | adantr 481 |
. . . . . . . . . . . 12
|
297 | 295, 296 | resubcld 10458 |
. . . . . . . . . . 11
|
298 | 279, 297 | remulcld 10070 |
. . . . . . . . . 10
|
299 | 13 | absge0d 14183 |
. . . . . . . . . . 11
|
300 | 299 | adantr 481 |
. . . . . . . . . 10
|
301 | 285 | absge0d 14183 |
. . . . . . . . . 10
|
302 | 77 | adantr 481 |
. . . . . . . . . 10
|
303 | 246 | adantr 481 |
. . . . . . . . . . . . . 14
|
304 | 238 | adantr 481 |
. . . . . . . . . . . . . 14
|
305 | 303, 304 | rpdivcld 11889 |
. . . . . . . . . . . . 13
|
306 | 12 | dmgmn0 24752 |
. . . . . . . . . . . . . . . . . . 19
|
307 | 306 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
308 | 169, 170,
307, 171 | divne0d 10817 |
. . . . . . . . . . . . . . . . 17
|
309 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . . 20
|
310 | 309 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
311 | 310 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
|
312 | 311 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . 17
|
313 | 172, 175,
308, 312 | mulne0d 10679 |
. . . . . . . . . . . . . . . 16
|
314 | 176, 313 | reccld 10794 |
. . . . . . . . . . . . . . 15
|
315 | 197, 314 | addcld 10059 |
. . . . . . . . . . . . . 14
|
316 | 176, 197,
176, 313 | divdird 10839 |
. . . . . . . . . . . . . . . 16
|
317 | 176, 313 | dividd 10799 |
. . . . . . . . . . . . . . . . 17
|
318 | 317 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
319 | 316, 318 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
320 | 198, 176,
199, 313 | divne0d 10817 |
. . . . . . . . . . . . . . 15
|
321 | 319, 320 | eqnetrrd 2862 |
. . . . . . . . . . . . . 14
|
322 | 315, 321 | absrpcld 14187 |
. . . . . . . . . . . . 13
|
323 | | 1red 10055 |
. . . . . . . . . . . . 13
|
324 | | 0le1 10551 |
. . . . . . . . . . . . . 14
|
325 | 324 | a1i 11 |
. . . . . . . . . . . . 13
|
326 | 305 | rpred 11872 |
. . . . . . . . . . . . . 14
|
327 | 314 | negcld 10379 |
. . . . . . . . . . . . . . . 16
|
328 | 327 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
329 | 328, 323 | resubcld 10458 |
. . . . . . . . . . . . . 14
|
330 | 315 | abscld 14175 |
. . . . . . . . . . . . . 14
|
331 | 240 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
332 | 304 | rpne0d 11877 |
. . . . . . . . . . . . . . . . 17
|
333 | 170, 331,
331, 332 | divsubdird 10840 |
. . . . . . . . . . . . . . . 16
|
334 | 331, 332 | dividd 10799 |
. . . . . . . . . . . . . . . . 17
|
335 | 334 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
336 | 333, 335 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
337 | 279, 304 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . 16
|
338 | 331, 170,
332, 171 | recdivd 10818 |
. . . . . . . . . . . . . . . . . 18
|
339 | 174, 90 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
|
340 | 176, 313 | absrpcld 14187 |
. . . . . . . . . . . . . . . . . . . 20
|
341 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
342 | 304, 341 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . . . 20
|
343 | 340, 342 | lerecd 11891 |
. . . . . . . . . . . . . . . . . . 19
|
344 | 339, 343 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
345 | 338, 344 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . 17
|
346 | 314 | absnegd 14188 |
. . . . . . . . . . . . . . . . . 18
|
347 | 197, 176,
313 | absdivd 14194 |
. . . . . . . . . . . . . . . . . . 19
|
348 | | abs1 14037 |
. . . . . . . . . . . . . . . . . . . 20
|
349 | 348 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . 19
|
350 | 347, 349 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
|
351 | 346, 350 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
352 | 345, 351 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
|
353 | 337, 328,
323, 352 | lesub1dd 10643 |
. . . . . . . . . . . . . . 15
|
354 | 336, 353 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
|
355 | 348 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
|
356 | 327, 197 | abs2difd 14196 |
. . . . . . . . . . . . . . . 16
|
357 | 355, 356 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . 15
|
358 | 197, 314 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . 19
|
359 | 358 | negeqd 10275 |
. . . . . . . . . . . . . . . . . 18
|
360 | 314, 197 | negdi2d 10406 |
. . . . . . . . . . . . . . . . . 18
|
361 | 359, 360 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
362 | 361 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
363 | 315 | absnegd 14188 |
. . . . . . . . . . . . . . . 16
|
364 | 362, 363 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
365 | 357, 364 | breqtrd 4679 |
. . . . . . . . . . . . . 14
|
366 | 326, 329,
330, 354, 365 | letrd 10194 |
. . . . . . . . . . . . 13
|
367 | 305, 322,
323, 325, 366 | lediv2ad 11894 |
. . . . . . . . . . . 12
|
368 | 16, 240 | subcld 10392 |
. . . . . . . . . . . . . . 15
|
369 | 368 | adantr 481 |
. . . . . . . . . . . . . 14
|
370 | 48, 243 | gtned 10172 |
. . . . . . . . . . . . . . . 16
|
371 | 16, 240, 370 | subne0d 10401 |
. . . . . . . . . . . . . . 15
|
372 | 371 | adantr 481 |
. . . . . . . . . . . . . 14
|
373 | 369, 331,
372, 332 | recdivd 10818 |
. . . . . . . . . . . . 13
|
374 | 170, 331 | nncand 10397 |
. . . . . . . . . . . . . . 15
|
375 | 374 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
376 | 170, 369,
369, 372 | divsubdird 10840 |
. . . . . . . . . . . . . 14
|
377 | 375, 376 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
378 | 369, 372 | dividd 10799 |
. . . . . . . . . . . . . 14
|
379 | 378 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
380 | 373, 377,
379 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
381 | 367, 380 | breqtrd 4679 |
. . . . . . . . . . 11
|
382 | 198, 197,
198, 199 | divsubdird 10840 |
. . . . . . . . . . . . . . 15
|
383 | 176, 197 | pncand 10393 |
. . . . . . . . . . . . . . . 16
|
384 | 383 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
385 | 198, 199 | dividd 10799 |
. . . . . . . . . . . . . . . 16
|
386 | 385 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
387 | 382, 384,
386 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . 14
|
388 | 198, 176,
199, 313 | recdivd 10818 |
. . . . . . . . . . . . . 14
|
389 | 319 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
390 | 387, 388,
389 | 3eqtr2d 2662 |
. . . . . . . . . . . . 13
|
391 | 390 | fveq2d 6195 |
. . . . . . . . . . . 12
|
392 | 197, 315,
321 | absdivd 14194 |
. . . . . . . . . . . . 13
|
393 | 348 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
394 | 392, 393 | syl6eq 2672 |
. . . . . . . . . . . 12
|
395 | 391, 394 | eqtrd 2656 |
. . . . . . . . . . 11
|
396 | 368, 371 | reccld 10794 |
. . . . . . . . . . . . . 14
|
397 | 396 | adantr 481 |
. . . . . . . . . . . . 13
|
398 | 248 | recnd 10068 |
. . . . . . . . . . . . . 14
|
399 | 398 | adantr 481 |
. . . . . . . . . . . . 13
|
400 | 170, 397,
399 | subdid 10486 |
. . . . . . . . . . . 12
|
401 | 170, 369,
372 | divrecd 10804 |
. . . . . . . . . . . . . 14
|
402 | 401 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
403 | 170, 171 | recidd 10796 |
. . . . . . . . . . . . 13
|
404 | 402, 403 | oveq12d 6668 |
. . . . . . . . . . . 12
|
405 | 400, 404 | eqtrd 2656 |
. . . . . . . . . . 11
|
406 | 381, 395,
405 | 3brtr4d 4685 |
. . . . . . . . . 10
|
407 | 287, 294,
289, 298, 300, 301, 302, 406 | lemul12ad 10966 |
. . . . . . . . 9
|
408 | 249 | recnd 10068 |
. . . . . . . . . . 11
|
409 | 408 | adantr 481 |
. . . . . . . . . 10
|
410 | 331, 170,
409 | mul12d 10245 |
. . . . . . . . 9
|
411 | 407, 410 | breqtrd 4679 |
. . . . . . . 8
|
412 | 287, 289 | remulcld 10070 |
. . . . . . . . 9
|
413 | 250 | adantr 481 |
. . . . . . . . 9
|
414 | 412, 413,
341 | ledivmuld 11925 |
. . . . . . . 8
|
415 | 411, 414 | mpbird 247 |
. . . . . . 7
|
416 | 293, 415 | eqbrtrd 4675 |
. . . . . 6
|
417 | 261, 267,
416 | chvar 2262 |
. . . . 5
|
418 | 253, 417 | eqbrtrd 4675 |
. . . 4
|
419 | 3, 4, 156, 234, 250, 418 | dvlip 23756 |
. . 3
|
420 | 1, 2, 419 | mpanr12 721 |
. 2
|
421 | | eqidd 2623 |
. . . . . 6
|
422 | | oveq2 6658 |
. . . . . . . 8
|
423 | 422, 186 | sylan9eqr 2678 |
. . . . . . 7
|
424 | 423 | oveq1d 6665 |
. . . . . . . 8
|
425 | 424 | fveq2d 6195 |
. . . . . . 7
|
426 | 423, 425 | oveq12d 6668 |
. . . . . 6
|
427 | 1 | a1i 11 |
. . . . . 6
|
428 | | ovexd 6680 |
. . . . . 6
|
429 | 421, 426,
427, 428 | fvmptd 6288 |
. . . . 5
|
430 | | oveq2 6658 |
. . . . . . . . 9
|
431 | 18 | mul01d 10235 |
. . . . . . . . 9
|
432 | 430, 431 | sylan9eqr 2678 |
. . . . . . . 8
|
433 | 432 | oveq1d 6665 |
. . . . . . . . . . 11
|
434 | | 0p1e1 11132 |
. . . . . . . . . . 11
|
435 | 433, 434 | syl6eq 2672 |
. . . . . . . . . 10
|
436 | 435 | fveq2d 6195 |
. . . . . . . . 9
|
437 | | log1 24332 |
. . . . . . . . 9
|
438 | 436, 437 | syl6eq 2672 |
. . . . . . . 8
|
439 | 432, 438 | oveq12d 6668 |
. . . . . . 7
|
440 | | 0m0e0 11130 |
. . . . . . 7
|
441 | 439, 440 | syl6eq 2672 |
. . . . . 6
|
442 | 2 | a1i 11 |
. . . . . 6
|
443 | 421, 441,
442, 442 | fvmptd 6288 |
. . . . 5
|
444 | 429, 443 | oveq12d 6668 |
. . . 4
|
445 | 18, 147 | addcld 10059 |
. . . . . . 7
|
446 | 12, 14 | dmgmdivn0 24754 |
. . . . . . 7
|
447 | 445, 446 | logcld 24317 |
. . . . . 6
|
448 | 18, 447 | subcld 10392 |
. . . . 5
|
449 | 448 | subid1d 10381 |
. . . 4
|
450 | 444, 449 | eqtr2d 2657 |
. . 3
|
451 | 450 | fveq2d 6195 |
. 2
|
452 | | 1m0e1 11131 |
. . . . . 6
|
453 | 452 | fveq2i 6194 |
. . . . 5
|
454 | 453, 348 | eqtri 2644 |
. . . 4
|
455 | 454 | oveq2i 6661 |
. . 3
|
456 | 240, 408 | mulcld 10060 |
. . . 4
|
457 | 456 | mulid1d 10057 |
. . 3
|
458 | 455, 457 | syl5req 2669 |
. 2
|
459 | 420, 451,
458 | 3brtr4d 4685 |
1
|