Metamath Proof Explorer


Theorem cosatan

Description: The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion cosatan A dom arctan cos arctan A = 1 1 + A 2

Proof

Step Hyp Ref Expression
1 atancl A dom arctan arctan A
2 cosval arctan A cos arctan A = e i arctan A + e i arctan A 2
3 1 2 syl A dom arctan cos arctan A = e i arctan A + e i arctan A 2
4 efiatan2 A dom arctan e i arctan A = 1 + i A 1 + A 2
5 ax-icn i
6 mulneg12 i arctan A i arctan A = i arctan A
7 5 1 6 sylancr A dom arctan i arctan A = i arctan A
8 atanneg A dom arctan arctan A = arctan A
9 8 oveq2d A dom arctan i arctan A = i arctan A
10 7 9 eqtr4d A dom arctan i arctan A = i arctan A
11 10 fveq2d A dom arctan e i arctan A = e i arctan A
12 atandmneg A dom arctan A dom arctan
13 efiatan2 A dom arctan e i arctan A = 1 + i A 1 + A 2
14 12 13 syl A dom arctan e i arctan A = 1 + i A 1 + A 2
15 atandm4 A dom arctan A 1 + A 2 0
16 15 simplbi A dom arctan A
17 mulneg2 i A i A = i A
18 5 16 17 sylancr A dom arctan i A = i A
19 18 oveq2d A dom arctan 1 + i A = 1 + i A
20 ax-1cn 1
21 mulcl i A i A
22 5 16 21 sylancr A dom arctan i A
23 negsub 1 i A 1 + i A = 1 i A
24 20 22 23 sylancr A dom arctan 1 + i A = 1 i A
25 19 24 eqtrd A dom arctan 1 + i A = 1 i A
26 sqneg A A 2 = A 2
27 16 26 syl A dom arctan A 2 = A 2
28 27 oveq2d A dom arctan 1 + A 2 = 1 + A 2
29 28 fveq2d A dom arctan 1 + A 2 = 1 + A 2
30 25 29 oveq12d A dom arctan 1 + i A 1 + A 2 = 1 i A 1 + A 2
31 11 14 30 3eqtrd A dom arctan e i arctan A = 1 i A 1 + A 2
32 4 31 oveq12d A dom arctan e i arctan A + e i arctan A = 1 + i A 1 + A 2 + 1 i A 1 + A 2
33 addcl 1 i A 1 + i A
34 20 22 33 sylancr A dom arctan 1 + i A
35 subcl 1 i A 1 i A
36 20 22 35 sylancr A dom arctan 1 i A
37 16 sqcld A dom arctan A 2
38 addcl 1 A 2 1 + A 2
39 20 37 38 sylancr A dom arctan 1 + A 2
40 39 sqrtcld A dom arctan 1 + A 2
41 39 sqsqrtd A dom arctan 1 + A 2 2 = 1 + A 2
42 15 simprbi A dom arctan 1 + A 2 0
43 41 42 eqnetrd A dom arctan 1 + A 2 2 0
44 sqne0 1 + A 2 1 + A 2 2 0 1 + A 2 0
45 40 44 syl A dom arctan 1 + A 2 2 0 1 + A 2 0
46 43 45 mpbid A dom arctan 1 + A 2 0
47 34 36 40 46 divdird A dom arctan 1 + i A + 1 i A 1 + A 2 = 1 + i A 1 + A 2 + 1 i A 1 + A 2
48 20 a1i A dom arctan 1
49 48 22 48 ppncand A dom arctan 1 + i A + 1 i A = 1 + 1
50 df-2 2 = 1 + 1
51 49 50 eqtr4di A dom arctan 1 + i A + 1 i A = 2
52 51 oveq1d A dom arctan 1 + i A + 1 i A 1 + A 2 = 2 1 + A 2
53 32 47 52 3eqtr2d A dom arctan e i arctan A + e i arctan A = 2 1 + A 2
54 53 oveq1d A dom arctan e i arctan A + e i arctan A 2 = 2 1 + A 2 2
55 2cnd A dom arctan 2
56 2ne0 2 0
57 56 a1i A dom arctan 2 0
58 55 40 55 46 57 divdiv32d A dom arctan 2 1 + A 2 2 = 2 2 1 + A 2
59 2div2e1 2 2 = 1
60 59 oveq1i 2 2 1 + A 2 = 1 1 + A 2
61 58 60 eqtrdi A dom arctan 2 1 + A 2 2 = 1 1 + A 2
62 3 54 61 3eqtrd A dom arctan cos arctan A = 1 1 + A 2