Proof of Theorem atanlogsublem
Step | Hyp | Ref
| Expression |
1 | | ax-1cn 9994 |
. . . . . 6
|
2 | | ax-icn 9995 |
. . . . . . 7
|
3 | | simpl 473 |
. . . . . . . . 9
arctan arctan |
4 | | atandm2 24604 |
. . . . . . . . 9
arctan |
5 | 3, 4 | sylib 208 |
. . . . . . . 8
arctan
|
6 | 5 | simp1d 1073 |
. . . . . . 7
arctan |
7 | | mulcl 10020 |
. . . . . . 7
|
8 | 2, 6, 7 | sylancr 695 |
. . . . . 6
arctan
|
9 | | addcl 10018 |
. . . . . 6
|
10 | 1, 8, 9 | sylancr 695 |
. . . . 5
arctan |
11 | 5 | simp3d 1075 |
. . . . 5
arctan |
12 | 10, 11 | logcld 24317 |
. . . 4
arctan |
13 | | subcl 10280 |
. . . . . 6
|
14 | 1, 8, 13 | sylancr 695 |
. . . . 5
arctan |
15 | 5 | simp2d 1074 |
. . . . 5
arctan |
16 | 14, 15 | logcld 24317 |
. . . 4
arctan |
17 | 12, 16 | imsubd 13957 |
. . 3
arctan |
18 | 2 | a1i 11 |
. . . . . . . . . 10
arctan |
19 | 18, 6, 18 | subdid 10486 |
. . . . . . . . 9
arctan
|
20 | | ixi 10656 |
. . . . . . . . . . 11
|
21 | 20 | oveq2i 6661 |
. . . . . . . . . 10
|
22 | | subneg 10330 |
. . . . . . . . . . 11
|
23 | 8, 1, 22 | sylancl 694 |
. . . . . . . . . 10
arctan |
24 | 21, 23 | syl5eq 2668 |
. . . . . . . . 9
arctan |
25 | | addcom 10222 |
. . . . . . . . . 10
|
26 | 8, 1, 25 | sylancl 694 |
. . . . . . . . 9
arctan |
27 | 19, 24, 26 | 3eqtrd 2660 |
. . . . . . . 8
arctan
|
28 | 27 | fveq2d 6195 |
. . . . . . 7
arctan
|
29 | | subcl 10280 |
. . . . . . . . 9
|
30 | 6, 2, 29 | sylancl 694 |
. . . . . . . 8
arctan
|
31 | | resub 13867 |
. . . . . . . . . . . 12
|
32 | 6, 2, 31 | sylancl 694 |
. . . . . . . . . . 11
arctan |
33 | | rei 13896 |
. . . . . . . . . . . . 13
|
34 | 33 | oveq2i 6661 |
. . . . . . . . . . . 12
|
35 | 6 | recld 13934 |
. . . . . . . . . . . . . 14
arctan |
36 | 35 | recnd 10068 |
. . . . . . . . . . . . 13
arctan |
37 | 36 | subid1d 10381 |
. . . . . . . . . . . 12
arctan |
38 | 34, 37 | syl5eq 2668 |
. . . . . . . . . . 11
arctan |
39 | 32, 38 | eqtrd 2656 |
. . . . . . . . . 10
arctan |
40 | | gt0ne0 10493 |
. . . . . . . . . . 11
|
41 | 35, 40 | sylancom 701 |
. . . . . . . . . 10
arctan |
42 | 39, 41 | eqnetrd 2861 |
. . . . . . . . 9
arctan |
43 | | fveq2 6191 |
. . . . . . . . . . 11
|
44 | | re0 13892 |
. . . . . . . . . . 11
|
45 | 43, 44 | syl6eq 2672 |
. . . . . . . . . 10
|
46 | 45 | necon3i 2826 |
. . . . . . . . 9
|
47 | 42, 46 | syl 17 |
. . . . . . . 8
arctan
|
48 | | simpr 477 |
. . . . . . . . . 10
arctan |
49 | | 0re 10040 |
. . . . . . . . . . 11
|
50 | | ltle 10126 |
. . . . . . . . . . 11
|
51 | 49, 35, 50 | sylancr 695 |
. . . . . . . . . 10
arctan
|
52 | 48, 51 | mpd 15 |
. . . . . . . . 9
arctan |
53 | 52, 39 | breqtrrd 4681 |
. . . . . . . 8
arctan
|
54 | | logimul 24360 |
. . . . . . . 8
|
55 | 30, 47, 53, 54 | syl3anc 1326 |
. . . . . . 7
arctan
|
56 | 28, 55 | eqtr3d 2658 |
. . . . . 6
arctan
|
57 | 56 | fveq2d 6195 |
. . . . 5
arctan
|
58 | 30, 47 | logcld 24317 |
. . . . . . 7
arctan |
59 | | halfpire 24216 |
. . . . . . . . 9
|
60 | 59 | recni 10052 |
. . . . . . . 8
|
61 | 2, 60 | mulcli 10045 |
. . . . . . 7
|
62 | | imadd 13874 |
. . . . . . 7
|
63 | 58, 61, 62 | sylancl 694 |
. . . . . 6
arctan
|
64 | | reim 13849 |
. . . . . . . . 9
|
65 | 60, 64 | ax-mp 5 |
. . . . . . . 8
|
66 | | rere 13862 |
. . . . . . . . 9
|
67 | 59, 66 | ax-mp 5 |
. . . . . . . 8
|
68 | 65, 67 | eqtr3i 2646 |
. . . . . . 7
|
69 | 68 | oveq2i 6661 |
. . . . . 6
|
70 | 63, 69 | syl6eq 2672 |
. . . . 5
arctan |
71 | 57, 70 | eqtrd 2656 |
. . . 4
arctan |
72 | | addcl 10018 |
. . . . . . . . . 10
|
73 | 6, 2, 72 | sylancl 694 |
. . . . . . . . 9
arctan
|
74 | | mulcl 10020 |
. . . . . . . . 9
|
75 | 2, 73, 74 | sylancr 695 |
. . . . . . . 8
arctan
|
76 | | reim 13849 |
. . . . . . . . . . 11
|
77 | 73, 76 | syl 17 |
. . . . . . . . . 10
arctan
|
78 | | readd 13866 |
. . . . . . . . . . . 12
|
79 | 6, 2, 78 | sylancl 694 |
. . . . . . . . . . 11
arctan |
80 | 33 | oveq2i 6661 |
. . . . . . . . . . . 12
|
81 | 36 | addid1d 10236 |
. . . . . . . . . . . 12
arctan |
82 | 80, 81 | syl5eq 2668 |
. . . . . . . . . . 11
arctan |
83 | 79, 82 | eqtrd 2656 |
. . . . . . . . . 10
arctan |
84 | 77, 83 | eqtr3d 2658 |
. . . . . . . . 9
arctan |
85 | 48, 84 | breqtrrd 4681 |
. . . . . . . 8
arctan
|
86 | | logneg2 24361 |
. . . . . . . 8
|
87 | 75, 85, 86 | syl2anc 693 |
. . . . . . 7
arctan
|
88 | 18, 6, 18 | adddid 10064 |
. . . . . . . . . . 11
arctan
|
89 | 20 | oveq2i 6661 |
. . . . . . . . . . . 12
|
90 | | negsub 10329 |
. . . . . . . . . . . . 13
|
91 | 8, 1, 90 | sylancl 694 |
. . . . . . . . . . . 12
arctan |
92 | 89, 91 | syl5eq 2668 |
. . . . . . . . . . 11
arctan |
93 | 88, 92 | eqtrd 2656 |
. . . . . . . . . 10
arctan
|
94 | 93 | negeqd 10275 |
. . . . . . . . 9
arctan
|
95 | | negsubdi2 10340 |
. . . . . . . . . 10
|
96 | 8, 1, 95 | sylancl 694 |
. . . . . . . . 9
arctan |
97 | 94, 96 | eqtrd 2656 |
. . . . . . . 8
arctan
|
98 | 97 | fveq2d 6195 |
. . . . . . 7
arctan
|
99 | 83, 41 | eqnetrd 2861 |
. . . . . . . . . . 11
arctan |
100 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
101 | 100, 44 | syl6eq 2672 |
. . . . . . . . . . . 12
|
102 | 101 | necon3i 2826 |
. . . . . . . . . . 11
|
103 | 99, 102 | syl 17 |
. . . . . . . . . 10
arctan
|
104 | 52, 83 | breqtrrd 4681 |
. . . . . . . . . 10
arctan
|
105 | | logimul 24360 |
. . . . . . . . . 10
|
106 | 73, 103, 104, 105 | syl3anc 1326 |
. . . . . . . . 9
arctan
|
107 | 106 | oveq1d 6665 |
. . . . . . . 8
arctan
|
108 | 73, 103 | logcld 24317 |
. . . . . . . . 9
arctan |
109 | 61 | a1i 11 |
. . . . . . . . 9
arctan
|
110 | | picn 24211 |
. . . . . . . . . . 11
|
111 | 2, 110 | mulcli 10045 |
. . . . . . . . . 10
|
112 | 111 | a1i 11 |
. . . . . . . . 9
arctan
|
113 | 108, 109,
112 | addsubassd 10412 |
. . . . . . . 8
arctan
|
114 | 107, 113 | eqtrd 2656 |
. . . . . . 7
arctan
|
115 | 87, 98, 114 | 3eqtr3d 2664 |
. . . . . 6
arctan
|
116 | 115 | fveq2d 6195 |
. . . . 5
arctan
|
117 | 61, 111 | subcli 10357 |
. . . . . . 7
|
118 | | imadd 13874 |
. . . . . . 7
|
119 | 108, 117,
118 | sylancl 694 |
. . . . . 6
arctan
|
120 | | imsub 13875 |
. . . . . . . . 9
|
121 | 61, 111, 120 | mp2an 708 |
. . . . . . . 8
|
122 | | reim 13849 |
. . . . . . . . . . 11
|
123 | 110, 122 | ax-mp 5 |
. . . . . . . . . 10
|
124 | | pire 24210 |
. . . . . . . . . . 11
|
125 | | rere 13862 |
. . . . . . . . . . 11
|
126 | 124, 125 | ax-mp 5 |
. . . . . . . . . 10
|
127 | 123, 126 | eqtr3i 2646 |
. . . . . . . . 9
|
128 | 68, 127 | oveq12i 6662 |
. . . . . . . 8
|
129 | 60 | negcli 10349 |
. . . . . . . . 9
|
130 | 110, 60 | negsubi 10359 |
. . . . . . . . . 10
|
131 | | pidiv2halves 24219 |
. . . . . . . . . . 11
|
132 | 110, 60, 60, 131 | subaddrii 10370 |
. . . . . . . . . 10
|
133 | 130, 132 | eqtri 2644 |
. . . . . . . . 9
|
134 | 60, 110, 129, 133 | subaddrii 10370 |
. . . . . . . 8
|
135 | 121, 128,
134 | 3eqtri 2648 |
. . . . . . 7
|
136 | 135 | oveq2i 6661 |
. . . . . 6
|
137 | 119, 136 | syl6eq 2672 |
. . . . 5
arctan
|
138 | 116, 137 | eqtrd 2656 |
. . . 4
arctan
|
139 | 71, 138 | oveq12d 6668 |
. . 3
arctan
|
140 | 58 | imcld 13935 |
. . . . . 6
arctan |
141 | 140 | recnd 10068 |
. . . . 5
arctan |
142 | 60 | a1i 11 |
. . . . 5
arctan
|
143 | 108 | imcld 13935 |
. . . . . 6
arctan |
144 | 143 | recnd 10068 |
. . . . 5
arctan |
145 | 129 | a1i 11 |
. . . . 5
arctan
|
146 | 141, 142,
144, 145 | addsub4d 10439 |
. . . 4
arctan
|
147 | 60, 60 | subnegi 10360 |
. . . . . 6
|
148 | 147, 131 | eqtri 2644 |
. . . . 5
|
149 | 148 | oveq2i 6661 |
. . . 4
|
150 | 146, 149 | syl6eq 2672 |
. . 3
arctan
|
151 | 17, 139, 150 | 3eqtrd 2660 |
. 2
arctan
|
152 | 140, 143 | resubcld 10458 |
. . . 4
arctan |
153 | | readdcl 10019 |
. . . 4
|
154 | 152, 124,
153 | sylancl 694 |
. . 3
arctan
|
155 | 124 | renegcli 10342 |
. . . . . . 7
|
156 | 155 | recni 10052 |
. . . . . 6
|
157 | 156, 110 | negsubi 10359 |
. . . . 5
|
158 | 155 | a1i 11 |
. . . . . . 7
arctan |
159 | 143 | renegcld 10457 |
. . . . . . 7
arctan |
160 | 30, 47 | logimcld 24318 |
. . . . . . . 8
arctan
|
161 | 160 | simpld 475 |
. . . . . . 7
arctan |
162 | 73, 103 | logimcld 24318 |
. . . . . . . . 9
arctan
|
163 | 162 | simprd 479 |
. . . . . . . 8
arctan |
164 | | leneg 10531 |
. . . . . . . . 9
|
165 | 143, 124,
164 | sylancl 694 |
. . . . . . . 8
arctan |
166 | 163, 165 | mpbid 222 |
. . . . . . 7
arctan |
167 | 158, 158,
140, 159, 161, 166 | ltleaddd 10648 |
. . . . . 6
arctan
|
168 | 141, 144 | negsubd 10398 |
. . . . . 6
arctan |
169 | 167, 168 | breqtrd 4679 |
. . . . 5
arctan
|
170 | 157, 169 | syl5eqbrr 4689 |
. . . 4
arctan
|
171 | 124 | a1i 11 |
. . . . 5
arctan |
172 | 158, 171,
152 | ltsubaddd 10623 |
. . . 4
arctan
|
173 | 170, 172 | mpbid 222 |
. . 3
arctan
|
174 | | 0red 10041 |
. . . . 5
arctan |
175 | 6 | imcld 13935 |
. . . . . . . . . . . . 13
arctan |
176 | | peano2rem 10348 |
. . . . . . . . . . . . 13
|
177 | 175, 176 | syl 17 |
. . . . . . . . . . . 12
arctan |
178 | | peano2re 10209 |
. . . . . . . . . . . . 13
|
179 | 175, 178 | syl 17 |
. . . . . . . . . . . 12
arctan |
180 | 175 | ltm1d 10956 |
. . . . . . . . . . . 12
arctan |
181 | 175 | ltp1d 10954 |
. . . . . . . . . . . 12
arctan |
182 | 177, 175,
179, 180, 181 | lttrd 10198 |
. . . . . . . . . . 11
arctan |
183 | | ltdiv1 10887 |
. . . . . . . . . . . 12
|
184 | 177, 179,
35, 48, 183 | syl112anc 1330 |
. . . . . . . . . . 11
arctan
|
185 | 182, 184 | mpbid 222 |
. . . . . . . . . 10
arctan |
186 | | imsub 13875 |
. . . . . . . . . . . . 13
|
187 | 6, 2, 186 | sylancl 694 |
. . . . . . . . . . . 12
arctan |
188 | | imi 13897 |
. . . . . . . . . . . . 13
|
189 | 188 | oveq2i 6661 |
. . . . . . . . . . . 12
|
190 | 187, 189 | syl6eq 2672 |
. . . . . . . . . . 11
arctan |
191 | 190, 39 | oveq12d 6668 |
. . . . . . . . . 10
arctan
|
192 | | imadd 13874 |
. . . . . . . . . . . . 13
|
193 | 6, 2, 192 | sylancl 694 |
. . . . . . . . . . . 12
arctan |
194 | 188 | oveq2i 6661 |
. . . . . . . . . . . 12
|
195 | 193, 194 | syl6eq 2672 |
. . . . . . . . . . 11
arctan |
196 | 195, 83 | oveq12d 6668 |
. . . . . . . . . 10
arctan
|
197 | 185, 191,
196 | 3brtr4d 4685 |
. . . . . . . . 9
arctan
|
198 | | tanarg 24365 |
. . . . . . . . . 10
|
199 | 30, 42, 198 | syl2anc 693 |
. . . . . . . . 9
arctan
|
200 | | tanarg 24365 |
. . . . . . . . . 10
|
201 | 73, 99, 200 | syl2anc 693 |
. . . . . . . . 9
arctan
|
202 | 197, 199,
201 | 3brtr4d 4685 |
. . . . . . . 8
arctan |
203 | 48, 39 | breqtrrd 4681 |
. . . . . . . . . 10
arctan
|
204 | | argregt0 24356 |
. . . . . . . . . 10
|
205 | 30, 203, 204 | syl2anc 693 |
. . . . . . . . 9
arctan |
206 | 48, 83 | breqtrrd 4681 |
. . . . . . . . . 10
arctan
|
207 | | argregt0 24356 |
. . . . . . . . . 10
|
208 | 73, 206, 207 | syl2anc 693 |
. . . . . . . . 9
arctan |
209 | | tanord 24284 |
. . . . . . . . 9
|
210 | 205, 208,
209 | syl2anc 693 |
. . . . . . . 8
arctan
|
211 | 202, 210 | mpbird 247 |
. . . . . . 7
arctan |
212 | 144 | addid2d 10237 |
. . . . . . 7
arctan
|
213 | 211, 212 | breqtrrd 4681 |
. . . . . 6
arctan |
214 | 140, 143,
174 | ltsubaddd 10623 |
. . . . . 6
arctan
|
215 | 213, 214 | mpbird 247 |
. . . . 5
arctan |
216 | 152, 174,
171, 215 | ltadd1dd 10638 |
. . . 4
arctan
|
217 | 110 | addid2i 10224 |
. . . 4
|
218 | 216, 217 | syl6breq 4694 |
. . 3
arctan
|
219 | 155 | rexri 10097 |
. . . 4
|
220 | 124 | rexri 10097 |
. . . 4
|
221 | | elioo2 12216 |
. . . 4
|
222 | 219, 220,
221 | mp2an 708 |
. . 3
|
223 | 154, 173,
218, 222 | syl3anbrc 1246 |
. 2
arctan
|
224 | 151, 223 | eqeltrd 2701 |
1
arctan |