Proof of Theorem efiatan2
Step | Hyp | Ref
| Expression |
1 | | ax-icn 9598 |
. . . . 5
 |
2 | | atancl 23807 |
. . . . 5

arctan arctan    |
3 | | mulcl 9623 |
. . . . 5
  arctan   
arctan     |
4 | 1, 2, 3 | sylancr 669 |
. . . 4

arctan  arctan     |
5 | | efcl 14137 |
. . . 4
  arctan  
    arctan      |
6 | 4, 5 | syl 17 |
. . 3

arctan     arctan      |
7 | | ax-1cn 9597 |
. . . . 5
 |
8 | | atandm2 23803 |
. . . . . . 7

arctan             |
9 | 8 | simp1bi 1023 |
. . . . . 6

arctan   |
10 | 9 | sqcld 12414 |
. . . . 5

arctan       |
11 | | addcl 9621 |
. . . . 5
               |
12 | 7, 10, 11 | sylancr 669 |
. . . 4

arctan         |
13 | 12 | sqrtcld 13499 |
. . 3

arctan             |
14 | 12 | sqsqrtd 13501 |
. . . . 5

arctan                       |
15 | | atandm4 23805 |
. . . . . 6

arctan           |
16 | 15 | simprbi 466 |
. . . . 5

arctan         |
17 | 14, 16 | eqnetrd 2691 |
. . . 4

arctan                 |
18 | | sqne0 12341 |
. . . . 5
                         
             |
19 | 13, 18 | syl 17 |
. . . 4

arctan               
             |
20 | 17, 19 | mpbid 214 |
. . 3

arctan             |
21 | 6, 13, 20 | divcan4d 10389 |
. 2

arctan      
arctan                             
arctan      |
22 | | halfcn 10829 |
. . . . . . 7
   |
23 | 12, 16 | logcld 23520 |
. . . . . . 7

arctan             |
24 | | mulcl 9623 |
. . . . . . 7
                               |
25 | 22, 23, 24 | sylancr 669 |
. . . . . 6

arctan                 |
26 | | efadd 14148 |
. . . . . 6
   arctan                       arctan                       
arctan                         |
27 | 4, 25, 26 | syl2anc 667 |
. . . . 5

arctan      arctan                        arctan                         |
28 | | 2cn 10680 |
. . . . . . . . . . . 12
 |
29 | 28 | a1i 11 |
. . . . . . . . . . 11

arctan   |
30 | | mulcl 9623 |
. . . . . . . . . . . . . 14
 
     |
31 | 1, 9, 30 | sylancr 669 |
. . . . . . . . . . . . 13

arctan     |
32 | | addcl 9621 |
. . . . . . . . . . . . 13
  
        |
33 | 7, 31, 32 | sylancr 669 |
. . . . . . . . . . . 12

arctan       |
34 | 8 | simp3bi 1025 |
. . . . . . . . . . . 12

arctan       |
35 | 33, 34 | logcld 23520 |
. . . . . . . . . . 11

arctan           |
36 | 29, 35, 4 | subdid 10074 |
. . . . . . . . . 10

arctan           
arctan                  arctan       |
37 | | atanval 23810 |
. . . . . . . . . . . . 13

arctan arctan                          |
38 | 37 | oveq2d 6306 |
. . . . . . . . . . . 12

arctan    arctan     
 
      
                |
39 | 1 | a1i 11 |
. . . . . . . . . . . . 13

arctan   |
40 | 29, 39, 2 | mulassd 9666 |
. . . . . . . . . . . 12

arctan    arctan     arctan      |
41 | | halfcl 10838 |
. . . . . . . . . . . . . . . . . 18
 
   |
42 | 1, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
   |
43 | 28, 1, 42 | mulassi 9652 |
. . . . . . . . . . . . . . . 16
       
     |
44 | 28, 1, 42 | mul12i 9828 |
. . . . . . . . . . . . . . . 16
  
          |
45 | | 2ne0 10702 |
. . . . . . . . . . . . . . . . . . 19
 |
46 | 1, 28, 45 | divcan2i 10350 |
. . . . . . . . . . . . . . . . . 18
     |
47 | 46 | oveq2i 6301 |
. . . . . . . . . . . . . . . . 17
         |
48 | | ixi 10241 |
. . . . . . . . . . . . . . . . 17
    |
49 | 47, 48 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
        |
50 | 43, 44, 49 | 3eqtri 2477 |
. . . . . . . . . . . . . . 15
        |
51 | 50 | oveq1i 6300 |
. . . . . . . . . . . . . 14
   
                                            |
52 | | subcl 9874 |
. . . . . . . . . . . . . . . . . 18
  
        |
53 | 7, 31, 52 | sylancr 669 |
. . . . . . . . . . . . . . . . 17

arctan       |
54 | 8 | simp2bi 1024 |
. . . . . . . . . . . . . . . . 17

arctan       |
55 | 53, 54 | logcld 23520 |
. . . . . . . . . . . . . . . 16

arctan     
     |
56 | 55, 35 | subcld 9986 |
. . . . . . . . . . . . . . 15

arctan                     |
57 | 56 | mulm1d 10070 |
. . . . . . . . . . . . . 14

arctan                            
              |
58 | 51, 57 | syl5eq 2497 |
. . . . . . . . . . . . 13

arctan    
                            
              |
59 | | 2mulicn 10836 |
. . . . . . . . . . . . . . 15
   |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . 14

arctan     |
61 | 42 | a1i 11 |
. . . . . . . . . . . . . 14

arctan     |
62 | 60, 61, 56 | mulassd 9666 |
. . . . . . . . . . . . 13

arctan    
                                                  |
63 | 55, 35 | negsubdi2d 10002 |
. . . . . . . . . . . . 13

arctan                                 
      |
64 | 58, 62, 63 | 3eqtr3d 2493 |
. . . . . . . . . . . 12

arctan                                               |
65 | 38, 40, 64 | 3eqtr3d 2493 |
. . . . . . . . . . 11

arctan   arctan                        |
66 | 65 | oveq2d 6306 |
. . . . . . . . . 10

arctan             
arctan                             
       |
67 | | mulcl 9623 |
. . . . . . . . . . . . 13
                       |
68 | 28, 35, 67 | sylancr 669 |
. . . . . . . . . . . 12

arctan             |
69 | 68, 35, 55 | subsubd 10014 |
. . . . . . . . . . 11

arctan                         
                              
      |
70 | 35 | 2timesd 10855 |
. . . . . . . . . . . . . 14

arctan                               |
71 | 70 | oveq1d 6305 |
. . . . . . . . . . . . 13

arctan                                                   |
72 | 35, 35 | pncand 9987 |
. . . . . . . . . . . . 13

arctan                                       |
73 | 71, 72 | eqtrd 2485 |
. . . . . . . . . . . 12

arctan                               |
74 | 73 | oveq1d 6305 |
. . . . . . . . . . 11

arctan                                                   |
75 | | atanlogadd 23840 |
. . . . . . . . . . . . 13

arctan                     |
76 | | logef 23531 |
. . . . . . . . . . . . 13
              
   
                   
                          |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12

arctan                    
                          |
78 | | efadd 14148 |
. . . . . . . . . . . . . . 15
                                   
                                 |
79 | 35, 55, 78 | syl2anc 667 |
. . . . . . . . . . . . . 14

arctan                 
                                 |
80 | | eflog 23526 |
. . . . . . . . . . . . . . . 16
                             |
81 | 33, 34, 80 | syl2anc 667 |
. . . . . . . . . . . . . . 15

arctan                   |
82 | | eflog 23526 |
. . . . . . . . . . . . . . . 16
   
   
                     |
83 | 53, 54, 82 | syl2anc 667 |
. . . . . . . . . . . . . . 15

arctan                   |
84 | 81, 83 | oveq12d 6308 |
. . . . . . . . . . . . . 14

arctan                                       |
85 | | sq1 12369 |
. . . . . . . . . . . . . . . . 17
     |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . 16

arctan       |
87 | | sqmul 12338 |
. . . . . . . . . . . . . . . . . 18
 
                   |
88 | 1, 9, 87 | sylancr 669 |
. . . . . . . . . . . . . . . . 17

arctan                   |
89 | | i2 12375 |
. . . . . . . . . . . . . . . . . . 19
      |
90 | 89 | oveq1i 6300 |
. . . . . . . . . . . . . . . . . 18
                  |
91 | 10 | mulm1d 10070 |
. . . . . . . . . . . . . . . . . 18

arctan               |
92 | 90, 91 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17

arctan                  |
93 | 88, 92 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16

arctan              |
94 | 86, 93 | oveq12d 6308 |
. . . . . . . . . . . . . . 15

arctan                      |
95 | | subsq 12382 |
. . . . . . . . . . . . . . . 16
  
                          |
96 | 7, 31, 95 | sylancr 669 |
. . . . . . . . . . . . . . 15

arctan                         |
97 | | subneg 9923 |
. . . . . . . . . . . . . . . 16
                      |
98 | 7, 10, 97 | sylancr 669 |
. . . . . . . . . . . . . . 15

arctan                |
99 | 94, 96, 98 | 3eqtr3d 2493 |
. . . . . . . . . . . . . 14

arctan                   |
100 | 79, 84, 99 | 3eqtrd 2489 |
. . . . . . . . . . . . 13

arctan                 
             |
101 | 100 | fveq2d 5869 |
. . . . . . . . . . . 12

arctan                    
                  |
102 | 77, 101 | eqtr3d 2487 |
. . . . . . . . . . 11

arctan                               |
103 | 69, 74, 102 | 3eqtrd 2489 |
. . . . . . . . . 10

arctan                         
                 |
104 | 36, 66, 103 | 3eqtrd 2489 |
. . . . . . . . 9

arctan           
arctan                 |
105 | 104 | oveq1d 6305 |
. . . . . . . 8

arctan             arctan                    |
106 | 35, 4 | subcld 9986 |
. . . . . . . . 9

arctan           arctan      |
107 | 45 | a1i 11 |
. . . . . . . . 9

arctan   |
108 | 106, 29, 107 | divcan3d 10388 |
. . . . . . . 8

arctan             arctan                arctan      |
109 | 23, 29, 107 | divrec2d 10387 |
. . . . . . . 8

arctan                             |
110 | 105, 108,
109 | 3eqtr3d 2493 |
. . . . . . 7

arctan           arctan                    |
111 | 35, 4, 25 | subaddd 10004 |
. . . . . . 7

arctan            arctan                    arctan                             |
112 | 110, 111 | mpbid 214 |
. . . . . 6

arctan   arctan                            |
113 | 112 | fveq2d 5869 |
. . . . 5

arctan      arctan                                 |
114 | 27, 113 | eqtr3d 2487 |
. . . 4

arctan      arctan                                     |
115 | 22 | a1i 11 |
. . . . . . 7

arctan     |
116 | 12, 16, 115 | cxpefd 23657 |
. . . . . 6

arctan                                |
117 | | cxpsqrt 23648 |
. . . . . . 7
                              |
118 | 12, 117 | syl 17 |
. . . . . 6

arctan                        |
119 | 116, 118 | eqtr3d 2487 |
. . . . 5

arctan                               |
120 | 119 | oveq2d 6306 |
. . . 4

arctan      arctan                            arctan                 |
121 | 114, 120,
81 | 3eqtr3d 2493 |
. . 3

arctan      arctan                     |
122 | 121 | oveq1d 6305 |
. 2

arctan      
arctan                                            |
123 | 21, 122 | eqtr3d 2487 |
1

arctan     arctan                      |