Metamath Proof Explorer


Theorem tanarg

Description: The basic relation between the "arg" function Im o. log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion tanarg A A 0 tan log A = A A

Proof

Step Hyp Ref Expression
1 fveq2 A = 0 A = 0
2 re0 0 = 0
3 1 2 eqtrdi A = 0 A = 0
4 3 necon3i A 0 A 0
5 logcl A A 0 log A
6 4 5 sylan2 A A 0 log A
7 6 imcld A A 0 log A
8 7 recnd A A 0 log A
9 sqcl A A 2
10 9 adantr A A 0 A 2
11 abscl A A
12 11 adantr A A 0 A
13 12 recnd A A 0 A
14 13 sqcld A A 0 A 2
15 absrpcl A A 0 A +
16 4 15 sylan2 A A 0 A +
17 16 rpne0d A A 0 A 0
18 sqne0 A A 2 0 A 0
19 13 18 syl A A 0 A 2 0 A 0
20 17 19 mpbird A A 0 A 2 0
21 10 14 14 20 divdird A A 0 A 2 + A 2 A 2 = A 2 A 2 + A 2 A 2
22 ax-icn i
23 mulcl i log A i log A
24 22 8 23 sylancr A A 0 i log A
25 2z 2
26 efexp i log A 2 e 2 i log A = e i log A 2
27 24 25 26 sylancl A A 0 e 2 i log A = e i log A 2
28 efiarg A A 0 e i log A = A A
29 4 28 sylan2 A A 0 e i log A = A A
30 29 oveq1d A A 0 e i log A 2 = A A 2
31 simpl A A 0 A
32 31 13 17 sqdivd A A 0 A A 2 = A 2 A 2
33 27 30 32 3eqtrrd A A 0 A 2 A 2 = e 2 i log A
34 14 20 dividd A A 0 A 2 A 2 = 1
35 33 34 oveq12d A A 0 A 2 A 2 + A 2 A 2 = e 2 i log A + 1
36 21 35 eqtr2d A A 0 e 2 i log A + 1 = A 2 + A 2 A 2
37 10 14 addcld A A 0 A 2 + A 2
38 22 a1i A A 0 i
39 2cn 2
40 recl A A
41 40 adantr A A 0 A
42 41 recnd A A 0 A
43 42 sqcld A A 0 A 2
44 mulcl 2 A 2 2 A 2
45 39 43 44 sylancr A A 0 2 A 2
46 39 a1i A A 0 2
47 imcl A A
48 47 adantr A A 0 A
49 48 recnd A A 0 A
50 42 49 mulcld A A 0 A A
51 38 46 50 mul12d A A 0 i 2 A A = 2 i A A
52 38 42 49 mul12d A A 0 i A A = A i A
53 52 oveq2d A A 0 2 i A A = 2 A i A
54 51 53 eqtrd A A 0 i 2 A A = 2 A i A
55 mulcl i A i A
56 22 49 55 sylancr A A 0 i A
57 42 56 mulcld A A 0 A i A
58 mulcl 2 A i A 2 A i A
59 39 57 58 sylancr A A 0 2 A i A
60 54 59 eqeltrd A A 0 i 2 A A
61 38 45 60 adddid A A 0 i 2 A 2 + i 2 A A = i 2 A 2 + i i 2 A A
62 mulcl A i A i
63 42 22 62 sylancl A A 0 A i
64 46 63 42 mulassd A A 0 2 A i A = 2 A i A
65 42 sqvald A A 0 A 2 = A A
66 65 oveq1d A A 0 A 2 i = A A i
67 mulcom A 2 i A 2 i = i A 2
68 43 22 67 sylancl A A 0 A 2 i = i A 2
69 42 42 38 mul32d A A 0 A A i = A i A
70 66 68 69 3eqtr3d A A 0 i A 2 = A i A
71 70 oveq2d A A 0 2 i A 2 = 2 A i A
72 46 38 43 mul12d A A 0 2 i A 2 = i 2 A 2
73 64 71 72 3eqtr2d A A 0 2 A i A = i 2 A 2
74 ixi i i = 1
75 74 oveq1i i i 2 A A = -1 2 A A
76 mulcl 2 A 2 A
77 39 49 76 sylancr A A 0 2 A
78 77 42 mulcld A A 0 2 A A
79 38 38 78 mulassd A A 0 i i 2 A A = i i 2 A A
80 75 79 eqtr3id A A 0 -1 2 A A = i i 2 A A
81 78 mulm1d A A 0 -1 2 A A = 2 A A
82 46 49 42 mulassd A A 0 2 A A = 2 A A
83 49 42 mulcomd A A 0 A A = A A
84 83 oveq2d A A 0 2 A A = 2 A A
85 82 84 eqtrd A A 0 2 A A = 2 A A
86 85 oveq2d A A 0 i 2 A A = i 2 A A
87 86 oveq2d A A 0 i i 2 A A = i i 2 A A
88 80 81 87 3eqtr3d A A 0 2 A A = i i 2 A A
89 73 88 oveq12d A A 0 2 A i A + 2 A A = i 2 A 2 + i i 2 A A
90 mulcl 2 A i 2 A i
91 39 63 90 sylancr A A 0 2 A i
92 91 42 mulcld A A 0 2 A i A
93 92 78 negsubd A A 0 2 A i A + 2 A A = 2 A i A 2 A A
94 61 89 93 3eqtr2d A A 0 i 2 A 2 + i 2 A A = 2 A i A 2 A A
95 49 sqcld A A 0 A 2
96 59 95 subcld A A 0 2 A i A A 2
97 43 96 43 95 add4d A A 0 A 2 + 2 A i A A 2 + A 2 + A 2 = A 2 + A 2 + 2 A i A A 2 + A 2
98 replim A A = A + i A
99 98 adantr A A 0 A = A + i A
100 99 oveq1d A A 0 A 2 = A + i A 2
101 binom2 A i A A + i A 2 = A 2 + 2 A i A + i A 2
102 42 56 101 syl2anc A A 0 A + i A 2 = A 2 + 2 A i A + i A 2
103 sqmul i A i A 2 = i 2 A 2
104 22 49 103 sylancr A A 0 i A 2 = i 2 A 2
105 i2 i 2 = 1
106 105 oveq1i i 2 A 2 = -1 A 2
107 104 106 eqtrdi A A 0 i A 2 = -1 A 2
108 95 mulm1d A A 0 -1 A 2 = A 2
109 107 108 eqtrd A A 0 i A 2 = A 2
110 109 oveq2d A A 0 A 2 + 2 A i A + i A 2 = A 2 + 2 A i A + A 2
111 43 59 addcld A A 0 A 2 + 2 A i A
112 111 95 negsubd A A 0 A 2 + 2 A i A + A 2 = A 2 + 2 A i A - A 2
113 102 110 112 3eqtrd A A 0 A + i A 2 = A 2 + 2 A i A - A 2
114 43 59 95 addsubassd A A 0 A 2 + 2 A i A - A 2 = A 2 + 2 A i A - A 2
115 100 113 114 3eqtrd A A 0 A 2 = A 2 + 2 A i A - A 2
116 absvalsq2 A A 2 = A 2 + A 2
117 116 adantr A A 0 A 2 = A 2 + A 2
118 115 117 oveq12d A A 0 A 2 + A 2 = A 2 + 2 A i A A 2 + A 2 + A 2
119 43 2timesd A A 0 2 A 2 = A 2 + A 2
120 59 95 npcand A A 0 2 A i A - A 2 + A 2 = 2 A i A
121 53 51 120 3eqtr4d A A 0 i 2 A A = 2 A i A - A 2 + A 2
122 119 121 oveq12d A A 0 2 A 2 + i 2 A A = A 2 + A 2 + 2 A i A A 2 + A 2
123 97 118 122 3eqtr4d A A 0 A 2 + A 2 = 2 A 2 + i 2 A A
124 123 oveq2d A A 0 i A 2 + A 2 = i 2 A 2 + i 2 A A
125 91 77 42 subdird A A 0 2 A i 2 A A = 2 A i A 2 A A
126 94 124 125 3eqtr4d A A 0 i A 2 + A 2 = 2 A i 2 A A
127 91 77 subcld A A 0 2 A i 2 A
128 mulcom A i A i = i A
129 42 22 128 sylancl A A 0 A i = i A
130 simpr A A 0 A 0
131 eleq1 i A = A i A A
132 48 131 syl5ibrcom A A 0 i A = A i A
133 rimul A i A A = 0
134 41 132 133 syl6an A A 0 i A = A A = 0
135 134 necon3d A A 0 A 0 i A A
136 130 135 mpd A A 0 i A A
137 129 136 eqnetrd A A 0 A i A
138 91 77 subeq0ad A A 0 2 A i 2 A = 0 2 A i = 2 A
139 2ne0 2 0
140 139 a1i A A 0 2 0
141 63 49 46 140 mulcand A A 0 2 A i = 2 A A i = A
142 138 141 bitrd A A 0 2 A i 2 A = 0 A i = A
143 142 necon3bid A A 0 2 A i 2 A 0 A i A
144 137 143 mpbird A A 0 2 A i 2 A 0
145 127 42 144 130 mulne0d A A 0 2 A i 2 A A 0
146 126 145 eqnetrd A A 0 i A 2 + A 2 0
147 oveq2 A 2 + A 2 = 0 i A 2 + A 2 = i 0
148 it0e0 i 0 = 0
149 147 148 eqtrdi A 2 + A 2 = 0 i A 2 + A 2 = 0
150 149 necon3i i A 2 + A 2 0 A 2 + A 2 0
151 146 150 syl A A 0 A 2 + A 2 0
152 37 14 151 20 divne0d A A 0 A 2 + A 2 A 2 0
153 36 152 eqnetrd A A 0 e 2 i log A + 1 0
154 tanval3 log A e 2 i log A + 1 0 tan log A = e 2 i log A 1 i e 2 i log A + 1
155 8 153 154 syl2anc A A 0 tan log A = e 2 i log A 1 i e 2 i log A + 1
156 10 14 14 20 divsubdird A A 0 A 2 A 2 A 2 = A 2 A 2 A 2 A 2
157 33 34 oveq12d A A 0 A 2 A 2 A 2 A 2 = e 2 i log A 1
158 156 157 eqtr2d A A 0 e 2 i log A 1 = A 2 A 2 A 2
159 36 oveq2d A A 0 i e 2 i log A + 1 = i A 2 + A 2 A 2
160 38 37 14 20 divassd A A 0 i A 2 + A 2 A 2 = i A 2 + A 2 A 2
161 159 160 eqtr4d A A 0 i e 2 i log A + 1 = i A 2 + A 2 A 2
162 158 161 oveq12d A A 0 e 2 i log A 1 i e 2 i log A + 1 = A 2 A 2 A 2 i A 2 + A 2 A 2
163 10 14 subcld A A 0 A 2 A 2
164 mulcl i A 2 + A 2 i A 2 + A 2
165 22 37 164 sylancr A A 0 i A 2 + A 2
166 163 165 14 146 20 divcan7d A A 0 A 2 A 2 A 2 i A 2 + A 2 A 2 = A 2 A 2 i A 2 + A 2
167 115 117 oveq12d A A 0 A 2 A 2 = A 2 + 2 A i A A 2 - A 2 + A 2
168 43 96 95 pnpcand A A 0 A 2 + 2 A i A A 2 - A 2 + A 2 = 2 A i A - A 2 - A 2
169 59 95 95 subsub4d A A 0 2 A i A - A 2 - A 2 = 2 A i A A 2 + A 2
170 95 2timesd A A 0 2 A 2 = A 2 + A 2
171 170 oveq2d A A 0 2 A i A 2 A 2 = 2 A i A A 2 + A 2
172 46 63 49 mulassd A A 0 2 A i A = 2 A i A
173 42 38 49 mulassd A A 0 A i A = A i A
174 173 oveq2d A A 0 2 A i A = 2 A i A
175 172 174 eqtr2d A A 0 2 A i A = 2 A i A
176 49 sqvald A A 0 A 2 = A A
177 176 oveq2d A A 0 2 A 2 = 2 A A
178 46 49 49 mulassd A A 0 2 A A = 2 A A
179 177 178 eqtr4d A A 0 2 A 2 = 2 A A
180 175 179 oveq12d A A 0 2 A i A 2 A 2 = 2 A i A 2 A A
181 91 77 49 subdird A A 0 2 A i 2 A A = 2 A i A 2 A A
182 180 181 eqtr4d A A 0 2 A i A 2 A 2 = 2 A i 2 A A
183 169 171 182 3eqtr2d A A 0 2 A i A - A 2 - A 2 = 2 A i 2 A A
184 167 168 183 3eqtrd A A 0 A 2 A 2 = 2 A i 2 A A
185 184 126 oveq12d A A 0 A 2 A 2 i A 2 + A 2 = 2 A i 2 A A 2 A i 2 A A
186 49 42 127 130 144 divcan5d A A 0 2 A i 2 A A 2 A i 2 A A = A A
187 166 185 186 3eqtrd A A 0 A 2 A 2 A 2 i A 2 + A 2 A 2 = A A
188 155 162 187 3eqtrd A A 0 tan log A = A A