Proof of Theorem dvatan
Step | Hyp | Ref
| Expression |
1 | | cnelprrecn 9632 |
. . . . 5
    |
2 | 1 | a1i 11 |
. . . 4
     |
3 | | ax-1cn 9597 |
. . . . . . 7
 |
4 | | ax-icn 9598 |
. . . . . . . 8
 |
5 | | atansopn.d |
. . . . . . . . . . . 12
  ![(,] (,]](_ioc.gif)    |
6 | | atansopn.s |
. . . . . . . . . . . 12
         |
7 | 5, 6 | atansssdm 23859 |
. . . . . . . . . . 11
arctan |
8 | | simpr 463 |
. . . . . . . . . . 11
    |
9 | 7, 8 | sseldi 3430 |
. . . . . . . . . 10
  arctan |
10 | | atandm2 23803 |
. . . . . . . . . 10

arctan             |
11 | 9, 10 | sylib 200 |
. . . . . . . . 9
    
         |
12 | 11 | simp1d 1020 |
. . . . . . . 8
    |
13 | | mulcl 9623 |
. . . . . . . 8
 
     |
14 | 4, 12, 13 | sylancr 669 |
. . . . . . 7
  
   |
15 | | subcl 9874 |
. . . . . . 7
  
        |
16 | 3, 14, 15 | sylancr 669 |
. . . . . 6
        |
17 | 11 | simp2d 1021 |
. . . . . 6
        |
18 | 16, 17 | logcld 23520 |
. . . . 5
            |
19 | | addcl 9621 |
. . . . . . 7
  
        |
20 | 3, 14, 19 | sylancr 669 |
. . . . . 6
        |
21 | 11 | simp3d 1022 |
. . . . . 6
        |
22 | 20, 21 | logcld 23520 |
. . . . 5
            |
23 | 18, 22 | subcld 9986 |
. . . 4
                      |
24 | | ovex 6318 |
. . . . 5
           |
25 | 24 | a1i 11 |
. . . 4
              |
26 | | ovex 6318 |
. . . . . . 7
     |
27 | 26 | a1i 11 |
. . . . . 6
        |
28 | 5, 6 | atans2 23857 |
. . . . . . . . . 10

            |
29 | 28 | simp2bi 1024 |
. . . . . . . . 9
       |
30 | 29 | adantl 468 |
. . . . . . . 8
        |
31 | | negex 9873 |
. . . . . . . . 9
  |
32 | 31 | a1i 11 |
. . . . . . . 8
     |
33 | 5 | logdmss 23587 |
. . . . . . . . . 10

    |
34 | | simpr 463 |
. . . . . . . . . 10
    |
35 | 33, 34 | sseldi 3430 |
. . . . . . . . 9
        |
36 | | logf1o 23514 |
. . . . . . . . . . 11
         |
37 | | f1of 5814 |
. . . . . . . . . . 11
                
  |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . 10
         |
39 | 38 | ffvelrni 6021 |
. . . . . . . . 9
           |
40 | | logrncn 23512 |
. . . . . . . . 9
           |
41 | 35, 39, 40 | 3syl 18 |
. . . . . . . 8
        |
42 | | ovex 6318 |
. . . . . . . . 9
   |
43 | 42 | a1i 11 |
. . . . . . . 8
      |
44 | 4 | a1i 11 |
. . . . . . . . . . 11
  |
45 | 44, 13 | sylan 474 |
. . . . . . . . . 10
  
   |
46 | 3, 45, 15 | sylancr 669 |
. . . . . . . . 9
        |
47 | 31 | a1i 11 |
. . . . . . . . 9
     |
48 | | 1cnd 9659 |
. . . . . . . . . . 11
    |
49 | | 0cnd 9636 |
. . . . . . . . . . 11
    |
50 | | 1cnd 9659 |
. . . . . . . . . . . 12
  |
51 | 2, 50 | dvmptc 22912 |
. . . . . . . . . . 11
        |
52 | 4 | a1i 11 |
. . . . . . . . . . 11
    |
53 | | simpr 463 |
. . . . . . . . . . . . 13
    |
54 | 2 | dvmptid 22911 |
. . . . . . . . . . . . 13
        |
55 | 2, 53, 48, 54, 44 | dvmptcmul 22918 |
. . . . . . . . . . . 12
            |
56 | 4 | mulid1i 9645 |
. . . . . . . . . . . . 13
   |
57 | 56 | mpteq2i 4486 |
. . . . . . . . . . . 12
       |
58 | 55, 57 | syl6eq 2501 |
. . . . . . . . . . 11
          |
59 | 2, 48, 49, 51, 45, 52, 58 | dvmptsub 22921 |
. . . . . . . . . 10
              |
60 | | df-neg 9863 |
. . . . . . . . . . 11
    |
61 | 60 | mpteq2i 4486 |
. . . . . . . . . 10
  
     |
62 | 59, 61 | syl6eqr 2503 |
. . . . . . . . 9
             |
63 | | eqid 2451 |
. . . . . . . . . . . 12
  ℂfld   ℂfld |
64 | 63 | cnfldtopon 21803 |
. . . . . . . . . . 11
  ℂfld TopOn   |
65 | 5, 6 | atansopn 23858 |
. . . . . . . . . . 11
  ℂfld |
66 | | toponss 19944 |
. . . . . . . . . . 11
    ℂfld
TopOn    ℂfld   |
67 | 64, 65, 66 | mp2an 678 |
. . . . . . . . . 10
 |
68 | 67 | a1i 11 |
. . . . . . . . 9
  |
69 | 63 | cnfldtop 21804 |
. . . . . . . . . . 11
  ℂfld  |
70 | 64 | toponunii 19947 |
. . . . . . . . . . . 12
   ℂfld |
71 | 70 | restid 15332 |
. . . . . . . . . . 11
   ℂfld    ℂfld
↾t    ℂfld  |
72 | 69, 71 | ax-mp 5 |
. . . . . . . . . 10
   ℂfld ↾t    ℂfld |
73 | 72 | eqcomi 2460 |
. . . . . . . . 9
  ℂfld    ℂfld ↾t   |
74 | 65 | a1i 11 |
. . . . . . . . 9
  ℂfld  |
75 | 2, 46, 47, 62, 68, 73, 63, 74 | dvmptres 22917 |
. . . . . . . 8
             |
76 | | fssres 5749 |
. . . . . . . . . . . . . 14
         
             |
77 | 38, 33, 76 | mp2an 678 |
. . . . . . . . . . . . 13
       |
78 | 77 | a1i 11 |
. . . . . . . . . . . 12
        |
79 | 78 | feqmptd 5918 |
. . . . . . . . . . 11
            |
80 | | fvres 5879 |
. . . . . . . . . . . 12
  
          |
81 | 80 | mpteq2ia 4485 |
. . . . . . . . . . 11
  
            |
82 | 79, 81 | syl6req 2502 |
. . . . . . . . . 10
      
   |
83 | 82 | oveq2d 6306 |
. . . . . . . . 9
              |
84 | 5 | dvlog 23596 |
. . . . . . . . 9
         |
85 | 83, 84 | syl6eq 2501 |
. . . . . . . 8
              |
86 | | fveq2 5865 |
. . . . . . . 8
                   |
87 | | oveq2 6298 |
. . . . . . . 8
         
     |
88 | 2, 2, 30, 32, 41, 43, 75, 85, 86, 87 | dvmptco 22926 |
. . . . . . 7
                         |
89 | | irec 12374 |
. . . . . . . . . 10
    |
90 | 89 | oveq2i 6301 |
. . . . . . . . 9
                    |
91 | 4 | a1i 11 |
. . . . . . . . . . 11
    |
92 | | ine0 10054 |
. . . . . . . . . . . 12
 |
93 | 92 | a1i 11 |
. . . . . . . . . . 11
    |
94 | 16, 91, 17, 93 | recdiv2d 10401 |
. . . . . . . . . 10
                    |
95 | 16, 17 | reccld 10376 |
. . . . . . . . . . 11
          |
96 | 95, 91, 93 | divrecd 10386 |
. . . . . . . . . 10
                      |
97 | | 1cnd 9659 |
. . . . . . . . . . . . . 14
    |
98 | 97, 14, 91 | subdird 10075 |
. . . . . . . . . . . . 13
    
             |
99 | 4 | mulid2i 9646 |
. . . . . . . . . . . . . . 15
   |
100 | 99 | a1i 11 |
. . . . . . . . . . . . . 14
      |
101 | 91, 12, 91 | mul32d 9843 |
. . . . . . . . . . . . . . 15
            |
102 | | ixi 10241 |
. . . . . . . . . . . . . . . . 17
    |
103 | 102 | oveq1i 6300 |
. . . . . . . . . . . . . . . 16
        |
104 | 12 | mulm1d 10070 |
. . . . . . . . . . . . . . . 16
        |
105 | 103, 104 | syl5eq 2497 |
. . . . . . . . . . . . . . 15
    
    |
106 | 101, 105 | eqtrd 2485 |
. . . . . . . . . . . . . 14
         |
107 | 100, 106 | oveq12d 6308 |
. . . . . . . . . . . . 13
    
 
        |
108 | | subneg 9923 |
. . . . . . . . . . . . . 14
 
        |
109 | 4, 12, 108 | sylancr 669 |
. . . . . . . . . . . . 13
  
      |
110 | 98, 107, 109 | 3eqtrd 2489 |
. . . . . . . . . . . 12
    
       |
111 | | addcom 9819 |
. . . . . . . . . . . . 13
 
       |
112 | 4, 12, 111 | sylancr 669 |
. . . . . . . . . . . 12
        |
113 | 110, 112 | eqtrd 2485 |
. . . . . . . . . . 11
    
       |
114 | 113 | oveq2d 6306 |
. . . . . . . . . 10
                |
115 | 94, 96, 114 | 3eqtr3d 2493 |
. . . . . . . . 9
                  |
116 | 90, 115 | syl5eqr 2499 |
. . . . . . . 8
          
      |
117 | 116 | mpteq2dva 4489 |
. . . . . . 7
    
              |
118 | 88, 117 | eqtrd 2485 |
. . . . . 6
                    |
119 | | ovex 6318 |
. . . . . . 7
     |
120 | 119 | a1i 11 |
. . . . . 6
        |
121 | 28 | simp3bi 1025 |
. . . . . . . . 9
       |
122 | 121 | adantl 468 |
. . . . . . . 8
        |
123 | 3, 45, 19 | sylancr 669 |
. . . . . . . . 9
        |
124 | 2, 48, 49, 51, 45, 52, 58 | dvmptadd 22914 |
. . . . . . . . . 10
              |
125 | 4 | addid2i 9821 |
. . . . . . . . . . 11
   |
126 | 125 | mpteq2i 4486 |
. . . . . . . . . 10
       |
127 | 124, 126 | syl6eq 2501 |
. . . . . . . . 9
            |
128 | 2, 123, 52, 127, 68, 73, 63, 74 | dvmptres 22917 |
. . . . . . . 8
            |
129 | | fveq2 5865 |
. . . . . . . 8
                   |
130 | | oveq2 6298 |
. . . . . . . 8
               |
131 | 2, 2, 122, 91, 41, 43, 128, 85, 129, 130 | dvmptco 22926 |
. . . . . . 7
                        |
132 | 97, 20, 91, 21, 93 | divdiv2d 10415 |
. . . . . . . . 9
                    |
133 | 97, 14, 91, 93 | divdird 10421 |
. . . . . . . . . . 11
                  |
134 | 89 | a1i 11 |
. . . . . . . . . . . 12
       |
135 | 12, 91, 93 | divcan3d 10388 |
. . . . . . . . . . . 12
        |
136 | 134, 135 | oveq12d 6308 |
. . . . . . . . . . 11
    
 
        |
137 | | negicn 9876 |
. . . . . . . . . . . . 13
  |
138 | | addcom 9819 |
. . . . . . . . . . . . 13
            |
139 | 137, 12, 138 | sylancr 669 |
. . . . . . . . . . . 12
          |
140 | | negsub 9922 |
. . . . . . . . . . . . 13
     
    |
141 | 12, 4, 140 | sylancl 668 |
. . . . . . . . . . . 12
    
    |
142 | 139, 141 | eqtrd 2485 |
. . . . . . . . . . 11
         |
143 | 133, 136,
142 | 3eqtrd 2489 |
. . . . . . . . . 10
            |
144 | 143 | oveq2d 6306 |
. . . . . . . . 9
                |
145 | 97, 91, 20, 21 | div23d 10420 |
. . . . . . . . 9
                    |
146 | 132, 144,
145 | 3eqtr3rd 2494 |
. . . . . . . 8
                |
147 | 146 | mpteq2dva 4489 |
. . . . . . 7
                  |
148 | 131, 147 | eqtrd 2485 |
. . . . . 6
                    |
149 | 2, 18, 27, 118, 22, 120, 148 | dvmptsub 22921 |
. . . . 5
                                    |
150 | | subcl 9874 |
. . . . . . . . 9
    
  |
151 | 12, 4, 150 | sylancl 668 |
. . . . . . . 8
      |
152 | | addcl 9621 |
. . . . . . . . 9
    
  |
153 | 12, 4, 152 | sylancl 668 |
. . . . . . . 8
      |
154 | 12 | sqcld 12414 |
. . . . . . . . 9
        |
155 | | addcl 9621 |
. . . . . . . . 9
               |
156 | 3, 154, 155 | sylancr 669 |
. . . . . . . 8
          |
157 | | atandm4 23805 |
. . . . . . . . . 10

arctan           |
158 | 157 | simprbi 466 |
. . . . . . . . 9

arctan         |
159 | 9, 158 | syl 17 |
. . . . . . . 8
          |
160 | 151, 153,
156, 159 | divsubdird 10422 |
. . . . . . 7
     
                       
          |
161 | 141 | oveq1d 6305 |
. . . . . . . . . 10
     
           |
162 | 137 | a1i 11 |
. . . . . . . . . . 11
     |
163 | 12, 162, 91 | pnpcand 10023 |
. . . . . . . . . 10
     
        |
164 | 161, 163 | eqtr3d 2487 |
. . . . . . . . 9
    
        |
165 | | 2cn 10680 |
. . . . . . . . . . . 12
 |
166 | 165, 4, 92 | divreci 10352 |
. . . . . . . . . . 11
       |
167 | 89 | oveq2i 6301 |
. . . . . . . . . . 11
        |
168 | 166, 167 | eqtri 2473 |
. . . . . . . . . 10
      |
169 | 137 | 2timesi 10730 |
. . . . . . . . . 10
        |
170 | 137, 4 | negsubi 9952 |
. . . . . . . . . 10
        |
171 | 168, 169,
170 | 3eqtri 2477 |
. . . . . . . . 9
      |
172 | 164, 171 | syl6eqr 2503 |
. . . . . . . 8
    
       |
173 | 172 | oveq1d 6305 |
. . . . . . 7
     
                      |
174 | 151 | mulid1d 9660 |
. . . . . . . . . 10
    
     |
175 | 151, 153 | mulcomd 9664 |
. . . . . . . . . . 11
    
     
     |
176 | | i2 12375 |
. . . . . . . . . . . . . 14
      |
177 | 176 | oveq2i 6301 |
. . . . . . . . . . . . 13
                  |
178 | | subneg 9923 |
. . . . . . . . . . . . . 14
     
                |
179 | 154, 3, 178 | sylancl 668 |
. . . . . . . . . . . . 13
                 |
180 | 177, 179 | syl5eq 2497 |
. . . . . . . . . . . 12
                    |
181 | | subsq 12382 |
. . . . . . . . . . . . 13
                     |
182 | 12, 4, 181 | sylancl 668 |
. . . . . . . . . . . 12
                    |
183 | | addcom 9819 |
. . . . . . . . . . . . 13
     
               |
184 | 154, 3, 183 | sylancl 668 |
. . . . . . . . . . . 12
                |
185 | 180, 182,
184 | 3eqtr3d 2493 |
. . . . . . . . . . 11
    
           |
186 | 175, 185 | eqtrd 2485 |
. . . . . . . . . 10
    
           |
187 | 174, 186 | oveq12d 6308 |
. . . . . . . . 9
     
          
         |
188 | | subneg 9923 |
. . . . . . . . . . . 12
     
    |
189 | 12, 4, 188 | sylancl 668 |
. . . . . . . . . . 11
    
    |
190 | | atandm 23802 |
. . . . . . . . . . . . . 14

arctan  
   |
191 | 9, 190 | sylib 200 |
. . . . . . . . . . . . 13
       |
192 | 191 | simp2d 1021 |
. . . . . . . . . . . 12
     |
193 | | subeq0 9900 |
. . . . . . . . . . . . . 14
       
    |
194 | 193 | necon3bid 2668 |
. . . . . . . . . . . . 13
       
    |
195 | 12, 137, 194 | sylancl 668 |
. . . . . . . . . . . 12
     
    |
196 | 192, 195 | mpbird 236 |
. . . . . . . . . . 11
       |
197 | 189, 196 | eqnetrrd 2692 |
. . . . . . . . . 10
      |
198 | 191 | simp3d 1022 |
. . . . . . . . . . 11
    |
199 | | subeq0 9900 |
. . . . . . . . . . . . 13
     
   |
200 | 199 | necon3bid 2668 |
. . . . . . . . . . . 12
     
   |
201 | 12, 4, 200 | sylancl 668 |
. . . . . . . . . . 11
    
   |
202 | 198, 201 | mpbird 236 |
. . . . . . . . . 10
      |
203 | 97, 153, 151, 197, 202 | divcan5d 10409 |
. . . . . . . . 9
     
              |
204 | 187, 203 | eqtr3d 2487 |
. . . . . . . 8
                  |
205 | 153 | mulid1d 9660 |
. . . . . . . . . 10
    
     |
206 | 205, 185 | oveq12d 6308 |
. . . . . . . . 9
     
          
         |
207 | 97, 151, 153, 202, 197 | divcan5d 10409 |
. . . . . . . . 9
     
              |
208 | 206, 207 | eqtr3d 2487 |
. . . . . . . 8
                  |
209 | 204, 208 | oveq12d 6308 |
. . . . . . 7
     
                              |
210 | 160, 173,
209 | 3eqtr3rd 2494 |
. . . . . 6
              
         |
211 | 210 | mpteq2dva 4489 |
. . . . 5
                          |
212 | 149, 211 | eqtrd 2485 |
. . . 4
                                    |
213 | | halfcl 10838 |
. . . . 5
 
   |
214 | 4, 213 | mp1i 13 |
. . . 4
    |
215 | 2, 23, 25, 212, 214 | dvmptcmul 22918 |
. . 3
                                            |
216 | | df-atan 23793 |
. . . . . . 7
arctan                                |
217 | 216 | reseq1i 5101 |
. . . . . 6
arctan                  
                |
218 | | atanf 23806 |
. . . . . . . . 9
arctan    
     |
219 | 218 | fdmi 5734 |
. . . . . . . 8
arctan    
   |
220 | 7, 219 | sseqtri 3464 |
. . . . . . 7

  
   |
221 | | resmpt 5154 |
. . . . . . 7
            
                        
                           |
222 | 220, 221 | ax-mp 5 |
. . . . . 6
                                                         |
223 | 217, 222 | eqtri 2473 |
. . . . 5
arctan                           |
224 | 223 | a1i 11 |
. . . 4
arctan                            |
225 | 224 | oveq2d 6306 |
. . 3
 arctan                               |
226 | | 2ne0 10702 |
. . . . . . 7
 |
227 | | divcan6 10314 |
. . . . . . 7
               |
228 | 4, 92, 165, 226, 227 | mp4an 679 |
. . . . . 6
       |
229 | 228 | oveq1i 6300 |
. . . . 5
                       |
230 | 4, 213 | mp1i 13 |
. . . . . 6
  
   |
231 | 165, 4, 92 | divcli 10349 |
. . . . . . 7
   |
232 | 231 | a1i 11 |
. . . . . 6
      |
233 | 230, 232,
156, 159 | divassd 10418 |
. . . . 5
                     
          |
234 | 229, 233 | syl5eqr 2499 |
. . . 4
               
          |
235 | 234 | mpteq2dva 4489 |
. . 3
                            |
236 | 215, 225,
235 | 3eqtr4d 2495 |
. 2
 arctan               |
237 | 236 | trud 1453 |
1
 arctan
             |