Step | Hyp | Ref
| Expression |
1 | | nn0uz 11722 |
. . . 4
|
2 | | 0zd 11389 |
. . . 4
|
3 | | 2cn 11091 |
. . . . . 6
|
4 | | ax-icn 9995 |
. . . . . 6
|
5 | | ine0 10465 |
. . . . . 6
|
6 | 3, 4, 5 | divcli 10767 |
. . . . 5
|
7 | 6 | a1i 11 |
. . . 4
|
8 | | 3cn 11095 |
. . . . . . 7
|
9 | | 3ne0 11115 |
. . . . . . 7
|
10 | 4, 8, 9 | divcli 10767 |
. . . . . 6
|
11 | | absdiv 14035 |
. . . . . . . . 9
|
12 | 4, 8, 9, 11 | mp3an 1424 |
. . . . . . . 8
|
13 | | absi 14026 |
. . . . . . . . 9
|
14 | | 3re 11094 |
. . . . . . . . . 10
|
15 | | 0re 10040 |
. . . . . . . . . . 11
|
16 | | 3pos 11114 |
. . . . . . . . . . 11
|
17 | 15, 14, 16 | ltleii 10160 |
. . . . . . . . . 10
|
18 | | absid 14036 |
. . . . . . . . . 10
|
19 | 14, 17, 18 | mp2an 708 |
. . . . . . . . 9
|
20 | 13, 19 | oveq12i 6662 |
. . . . . . . 8
|
21 | 12, 20 | eqtri 2644 |
. . . . . . 7
|
22 | | 1lt3 11196 |
. . . . . . . 8
|
23 | | recgt1 10919 |
. . . . . . . . 9
|
24 | 14, 16, 23 | mp2an 708 |
. . . . . . . 8
|
25 | 22, 24 | mpbi 220 |
. . . . . . 7
|
26 | 21, 25 | eqbrtri 4674 |
. . . . . 6
|
27 | | eqid 2622 |
. . . . . . 7
|
28 | 27 | atantayl3 24666 |
. . . . . 6
arctan |
29 | 10, 26, 28 | mp2an 708 |
. . . . 5
arctan
|
30 | 29 | a1i 11 |
. . . 4
arctan |
31 | | oveq2 6658 |
. . . . . . . . 9
|
32 | | oveq2 6658 |
. . . . . . . . . . . 12
|
33 | 32 | oveq1d 6665 |
. . . . . . . . . . 11
|
34 | 33 | oveq2d 6666 |
. . . . . . . . . 10
|
35 | 34, 33 | oveq12d 6668 |
. . . . . . . . 9
|
36 | 31, 35 | oveq12d 6668 |
. . . . . . . 8
|
37 | | ovex 6678 |
. . . . . . . 8
|
38 | 36, 27, 37 | fvmpt 6282 |
. . . . . . 7
|
39 | 4 | a1i 11 |
. . . . . . . . . . . 12
|
40 | 8 | a1i 11 |
. . . . . . . . . . . 12
|
41 | 9 | a1i 11 |
. . . . . . . . . . . 12
|
42 | | 2nn0 11309 |
. . . . . . . . . . . . . 14
|
43 | | nn0mulcl 11329 |
. . . . . . . . . . . . . 14
|
44 | 42, 43 | mpan 706 |
. . . . . . . . . . . . 13
|
45 | | peano2nn0 11333 |
. . . . . . . . . . . . 13
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . 12
|
47 | 39, 40, 41, 46 | expdivd 13022 |
. . . . . . . . . . 11
|
48 | 47 | oveq2d 6666 |
. . . . . . . . . 10
|
49 | | neg1cn 11124 |
. . . . . . . . . . . 12
|
50 | | expcl 12878 |
. . . . . . . . . . . 12
|
51 | 49, 50 | mpan 706 |
. . . . . . . . . . 11
|
52 | | expcl 12878 |
. . . . . . . . . . . 12
|
53 | 4, 46, 52 | sylancr 695 |
. . . . . . . . . . 11
|
54 | | 3nn 11186 |
. . . . . . . . . . . . 13
|
55 | | nnexpcl 12873 |
. . . . . . . . . . . . 13
|
56 | 54, 46, 55 | sylancr 695 |
. . . . . . . . . . . 12
|
57 | 56 | nncnd 11036 |
. . . . . . . . . . 11
|
58 | 56 | nnne0d 11065 |
. . . . . . . . . . 11
|
59 | 51, 53, 57, 58 | divassd 10836 |
. . . . . . . . . 10
|
60 | | expp1 12867 |
. . . . . . . . . . . . . . 15
|
61 | 4, 44, 60 | sylancr 695 |
. . . . . . . . . . . . . 14
|
62 | | expmul 12905 |
. . . . . . . . . . . . . . . . 17
|
63 | 4, 42, 62 | mp3an12 1414 |
. . . . . . . . . . . . . . . 16
|
64 | | i2 12965 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
66 | 63, 65 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
67 | 66 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
68 | 61, 67 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
69 | 68 | oveq2d 6666 |
. . . . . . . . . . . 12
|
70 | 51, 51, 39 | mulassd 10063 |
. . . . . . . . . . . 12
|
71 | 49 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
72 | | id 22 |
. . . . . . . . . . . . . . . 16
|
73 | 71, 72, 72 | expaddd 13010 |
. . . . . . . . . . . . . . 15
|
74 | | expmul 12905 |
. . . . . . . . . . . . . . . . . 18
|
75 | 49, 42, 74 | mp3an12 1414 |
. . . . . . . . . . . . . . . . 17
|
76 | | neg1sqe1 12959 |
. . . . . . . . . . . . . . . . . 18
|
77 | 76 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
|
78 | 75, 77 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
79 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . 18
|
80 | 79 | 2timesd 11275 |
. . . . . . . . . . . . . . . . 17
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
82 | | nn0z 11400 |
. . . . . . . . . . . . . . . . 17
|
83 | | 1exp 12889 |
. . . . . . . . . . . . . . . . 17
|
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
|
85 | 78, 81, 84 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . 15
|
86 | 73, 85 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
|
87 | 86 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
88 | 4 | mulid2i 10043 |
. . . . . . . . . . . . 13
|
89 | 87, 88 | syl6eq 2672 |
. . . . . . . . . . . 12
|
90 | 69, 70, 89 | 3eqtr2d 2662 |
. . . . . . . . . . 11
|
91 | 90 | oveq1d 6665 |
. . . . . . . . . 10
|
92 | 48, 59, 91 | 3eqtr2d 2662 |
. . . . . . . . 9
|
93 | 92 | oveq1d 6665 |
. . . . . . . 8
|
94 | | expcl 12878 |
. . . . . . . . . 10
|
95 | 10, 46, 94 | sylancr 695 |
. . . . . . . . 9
|
96 | | nn0p1nn 11332 |
. . . . . . . . . . 11
|
97 | 44, 96 | syl 17 |
. . . . . . . . . 10
|
98 | 97 | nncnd 11036 |
. . . . . . . . 9
|
99 | 97 | nnne0d 11065 |
. . . . . . . . 9
|
100 | 51, 95, 98, 99 | divassd 10836 |
. . . . . . . 8
|
101 | 39, 57, 98, 58, 99 | divdiv1d 10832 |
. . . . . . . 8
|
102 | 93, 100, 101 | 3eqtr3d 2664 |
. . . . . . 7
|
103 | 57, 98 | mulcomd 10061 |
. . . . . . . 8
|
104 | 103 | oveq2d 6666 |
. . . . . . 7
|
105 | 38, 102, 104 | 3eqtrd 2660 |
. . . . . 6
|
106 | 97, 56 | nnmulcld 11068 |
. . . . . . . 8
|
107 | 106 | nncnd 11036 |
. . . . . . 7
|
108 | 106 | nnne0d 11065 |
. . . . . . 7
|
109 | 39, 107, 108 | divcld 10801 |
. . . . . 6
|
110 | 105, 109 | eqeltrd 2701 |
. . . . 5
|
111 | 110 | adantl 482 |
. . . 4
|
112 | 33 | oveq2d 6666 |
. . . . . . . . 9
|
113 | | oveq2 6658 |
. . . . . . . . 9
|
114 | 112, 113 | oveq12d 6668 |
. . . . . . . 8
|
115 | 114 | oveq2d 6666 |
. . . . . . 7
|
116 | | log2cnv.1 |
. . . . . . 7
|
117 | | ovex 6678 |
. . . . . . 7
|
118 | 115, 116,
117 | fvmpt 6282 |
. . . . . 6
|
119 | | expp1 12867 |
. . . . . . . . . . . . . . 15
|
120 | 8, 44, 119 | sylancr 695 |
. . . . . . . . . . . . . 14
|
121 | | expmul 12905 |
. . . . . . . . . . . . . . . . 17
|
122 | 8, 42, 121 | mp3an12 1414 |
. . . . . . . . . . . . . . . 16
|
123 | | sq3 12961 |
. . . . . . . . . . . . . . . . 17
|
124 | 123 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
125 | 122, 124 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
126 | 125 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
127 | | 9nn 11192 |
. . . . . . . . . . . . . . . . 17
|
128 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . 17
|
129 | 127, 128 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
130 | 129 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
131 | | mulcom 10022 |
. . . . . . . . . . . . . . 15
|
132 | 130, 8, 131 | sylancl 694 |
. . . . . . . . . . . . . 14
|
133 | 120, 126,
132 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
134 | 90, 133 | oveq12d 6668 |
. . . . . . . . . . . 12
|
135 | 48, 59, 134 | 3eqtr2d 2662 |
. . . . . . . . . . 11
|
136 | 135 | oveq1d 6665 |
. . . . . . . . . 10
|
137 | | nnmulcl 11043 |
. . . . . . . . . . . . 13
|
138 | 54, 129, 137 | sylancr 695 |
. . . . . . . . . . . 12
|
139 | 138 | nncnd 11036 |
. . . . . . . . . . 11
|
140 | 138 | nnne0d 11065 |
. . . . . . . . . . 11
|
141 | 39, 139, 98, 140, 99 | divdiv1d 10832 |
. . . . . . . . . 10
|
142 | 136, 100,
141 | 3eqtr3d 2664 |
. . . . . . . . 9
|
143 | 40, 130, 98 | mul32d 10246 |
. . . . . . . . . 10
|
144 | 143 | oveq2d 6666 |
. . . . . . . . 9
|
145 | 38, 142, 144 | 3eqtrd 2660 |
. . . . . . . 8
|
146 | 145 | oveq2d 6666 |
. . . . . . 7
|
147 | | nnmulcl 11043 |
. . . . . . . . . . . 12
|
148 | 54, 97, 147 | sylancr 695 |
. . . . . . . . . . 11
|
149 | 148, 129 | nnmulcld 11068 |
. . . . . . . . . 10
|
150 | 149 | nncnd 11036 |
. . . . . . . . 9
|
151 | 149 | nnne0d 11065 |
. . . . . . . . 9
|
152 | 39, 150, 151 | divcld 10801 |
. . . . . . . 8
|
153 | | mulcom 10022 |
. . . . . . . 8
|
154 | 152, 6, 153 | sylancl 694 |
. . . . . . 7
|
155 | 3 | a1i 11 |
. . . . . . . 8
|
156 | 5 | a1i 11 |
. . . . . . . 8
|
157 | 155, 39, 150, 156, 151 | dmdcand 10830 |
. . . . . . 7
|
158 | 146, 154,
157 | 3eqtr2d 2662 |
. . . . . 6
|
159 | 118, 158 | eqtr4d 2659 |
. . . . 5
|
160 | 159 | adantl 482 |
. . . 4
|
161 | 1, 2, 7, 30, 111, 160 | isermulc2 14388 |
. . 3
arctan
|
162 | 161 | trud 1493 |
. 2
arctan |
163 | | bndatandm 24656 |
. . . . . . . 8
arctan |
164 | 10, 26, 163 | mp2an 708 |
. . . . . . 7
arctan |
165 | | atanval 24611 |
. . . . . . 7
arctan arctan
|
166 | 164, 165 | ax-mp 5 |
. . . . . 6
arctan
|
167 | | df-4 11081 |
. . . . . . . . . . . . 13
|
168 | 167 | oveq1i 6660 |
. . . . . . . . . . . 12
|
169 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
170 | 8, 169, 8, 9 | divdiri 10782 |
. . . . . . . . . . . 12
|
171 | 8, 9 | dividi 10758 |
. . . . . . . . . . . . 13
|
172 | 171 | oveq1i 6660 |
. . . . . . . . . . . 12
|
173 | 168, 170,
172 | 3eqtri 2648 |
. . . . . . . . . . 11
|
174 | 169, 8, 9 | divcli 10767 |
. . . . . . . . . . . 12
|
175 | 169, 174 | subnegi 10360 |
. . . . . . . . . . 11
|
176 | | divneg 10719 |
. . . . . . . . . . . . . 14
|
177 | 169, 8, 9, 176 | mp3an 1424 |
. . . . . . . . . . . . 13
|
178 | | ixi 10656 |
. . . . . . . . . . . . . 14
|
179 | 178 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
180 | 4, 4, 8, 9 | divassi 10781 |
. . . . . . . . . . . . 13
|
181 | 177, 179,
180 | 3eqtr2i 2650 |
. . . . . . . . . . . 12
|
182 | 181 | oveq2i 6661 |
. . . . . . . . . . 11
|
183 | 173, 175,
182 | 3eqtr2ri 2651 |
. . . . . . . . . 10
|
184 | 183 | fveq2i 6194 |
. . . . . . . . 9
|
185 | 8, 9 | pm3.2i 471 |
. . . . . . . . . . . . 13
|
186 | | divsubdir 10721 |
. . . . . . . . . . . . 13
|
187 | 8, 169, 185, 186 | mp3an 1424 |
. . . . . . . . . . . 12
|
188 | | 3m1e2 11137 |
. . . . . . . . . . . . 13
|
189 | 188 | oveq1i 6660 |
. . . . . . . . . . . 12
|
190 | 171 | oveq1i 6660 |
. . . . . . . . . . . 12
|
191 | 187, 189,
190 | 3eqtr3i 2652 |
. . . . . . . . . . 11
|
192 | 169, 174 | negsubi 10359 |
. . . . . . . . . . 11
|
193 | 181 | oveq2i 6661 |
. . . . . . . . . . 11
|
194 | 191, 192,
193 | 3eqtr2ri 2651 |
. . . . . . . . . 10
|
195 | 194 | fveq2i 6194 |
. . . . . . . . 9
|
196 | 184, 195 | oveq12i 6662 |
. . . . . . . 8
|
197 | | 4re 11097 |
. . . . . . . . . . 11
|
198 | | 4pos 11116 |
. . . . . . . . . . 11
|
199 | 197, 198 | elrpii 11835 |
. . . . . . . . . 10
|
200 | 14, 16 | elrpii 11835 |
. . . . . . . . . 10
|
201 | | rpdivcl 11856 |
. . . . . . . . . 10
|
202 | 199, 200,
201 | mp2an 708 |
. . . . . . . . 9
|
203 | | 2rp 11837 |
. . . . . . . . . 10
|
204 | | rpdivcl 11856 |
. . . . . . . . . 10
|
205 | 203, 200,
204 | mp2an 708 |
. . . . . . . . 9
|
206 | | relogdiv 24339 |
. . . . . . . . 9
|
207 | 202, 205,
206 | mp2an 708 |
. . . . . . . 8
|
208 | | 4cn 11098 |
. . . . . . . . . . 11
|
209 | | 2cnne0 11242 |
. . . . . . . . . . 11
|
210 | | divcan7 10734 |
. . . . . . . . . . 11
|
211 | 208, 209,
185, 210 | mp3an 1424 |
. . . . . . . . . 10
|
212 | | 4d2e2 11184 |
. . . . . . . . . 10
|
213 | 211, 212 | eqtri 2644 |
. . . . . . . . 9
|
214 | 213 | fveq2i 6194 |
. . . . . . . 8
|
215 | 196, 207,
214 | 3eqtr2i 2650 |
. . . . . . 7
|
216 | 215 | oveq2i 6661 |
. . . . . 6
|
217 | 166, 216 | eqtri 2644 |
. . . . 5
arctan
|
218 | 217 | oveq2i 6661 |
. . . 4
arctan
|
219 | | 2ne0 11113 |
. . . . . 6
|
220 | 4, 3, 219 | divcli 10767 |
. . . . 5
|
221 | | logcl 24315 |
. . . . . 6
|
222 | 3, 219, 221 | mp2an 708 |
. . . . 5
|
223 | 6, 220, 222 | mulassi 10049 |
. . . 4
|
224 | 218, 223 | eqtr4i 2647 |
. . 3
arctan
|
225 | | divcan6 10732 |
. . . . 5
|
226 | 3, 219, 4, 5, 225 | mp4an 709 |
. . . 4
|
227 | 226 | oveq1i 6660 |
. . 3
|
228 | 222 | mulid2i 10043 |
. . 3
|
229 | 224, 227,
228 | 3eqtri 2648 |
. 2
arctan
|
230 | 162, 229 | breqtri 4678 |
1
|