Metamath Proof Explorer


Theorem tanatan

Description: The arctangent function is an inverse to tan . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion tanatan A dom arctan tan arctan A = A

Proof

Step Hyp Ref Expression
1 atancl A dom arctan arctan A
2 2efiatan A dom arctan e 2 i arctan A = 2 i A + i 1
3 2 oveq1d A dom arctan e 2 i arctan A + 1 = 2 i A + i - 1 + 1
4 2mulicn 2 i
5 4 a1i A dom arctan 2 i
6 atandm A dom arctan A A i A i
7 6 simp1bi A dom arctan A
8 ax-icn i
9 addcl A i A + i
10 7 8 9 sylancl A dom arctan A + i
11 subneg A i A i = A + i
12 7 8 11 sylancl A dom arctan A i = A + i
13 6 simp2bi A dom arctan A i
14 8 negcli i
15 subeq0 A i A i = 0 A = i
16 15 necon3bid A i A i 0 A i
17 7 14 16 sylancl A dom arctan A i 0 A i
18 13 17 mpbird A dom arctan A i 0
19 12 18 eqnetrrd A dom arctan A + i 0
20 5 10 19 divcld A dom arctan 2 i A + i
21 ax-1cn 1
22 npcan 2 i A + i 1 2 i A + i - 1 + 1 = 2 i A + i
23 20 21 22 sylancl A dom arctan 2 i A + i - 1 + 1 = 2 i A + i
24 3 23 eqtrd A dom arctan e 2 i arctan A + 1 = 2 i A + i
25 2muline0 2 i 0
26 25 a1i A dom arctan 2 i 0
27 5 10 26 19 divne0d A dom arctan 2 i A + i 0
28 24 27 eqnetrd A dom arctan e 2 i arctan A + 1 0
29 tanval3 arctan A e 2 i arctan A + 1 0 tan arctan A = e 2 i arctan A 1 i e 2 i arctan A + 1
30 1 28 29 syl2anc A dom arctan tan arctan A = e 2 i arctan A 1 i e 2 i arctan A + 1
31 2 oveq1d A dom arctan e 2 i arctan A 1 = 2 i A + i - 1 - 1
32 21 a1i A dom arctan 1
33 20 32 32 subsub4d A dom arctan 2 i A + i - 1 - 1 = 2 i A + i 1 + 1
34 df-2 2 = 1 + 1
35 34 oveq2i 2 i A + i 2 = 2 i A + i 1 + 1
36 33 35 eqtr4di A dom arctan 2 i A + i - 1 - 1 = 2 i A + i 2
37 31 36 eqtrd A dom arctan e 2 i arctan A 1 = 2 i A + i 2
38 2cn 2
39 mulcl 2 A + i 2 A + i
40 38 10 39 sylancr A dom arctan 2 A + i
41 5 40 10 19 divsubdird A dom arctan 2 i 2 A + i A + i = 2 i A + i 2 A + i A + i
42 mulneg12 2 A -2 A = 2 A
43 38 7 42 sylancr A dom arctan -2 A = 2 A
44 negsub i A i + A = i A
45 8 7 44 sylancr A dom arctan i + A = i A
46 45 oveq1d A dom arctan i + A - i = i - A - i
47 7 negcld A dom arctan A
48 pncan2 i A i + A - i = A
49 8 47 48 sylancr A dom arctan i + A - i = A
50 8 a1i A dom arctan i
51 50 7 50 subsub4d A dom arctan i - A - i = i A + i
52 46 49 51 3eqtr3rd A dom arctan i A + i = A
53 52 oveq2d A dom arctan 2 i A + i = 2 A
54 38 a1i A dom arctan 2
55 54 50 10 subdid A dom arctan 2 i A + i = 2 i 2 A + i
56 43 53 55 3eqtr2rd A dom arctan 2 i 2 A + i = -2 A
57 56 oveq1d A dom arctan 2 i 2 A + i A + i = -2 A A + i
58 54 10 19 divcan4d A dom arctan 2 A + i A + i = 2
59 58 oveq2d A dom arctan 2 i A + i 2 A + i A + i = 2 i A + i 2
60 41 57 59 3eqtr3d A dom arctan -2 A A + i = 2 i A + i 2
61 37 60 eqtr4d A dom arctan e 2 i arctan A 1 = -2 A A + i
62 24 oveq2d A dom arctan i e 2 i arctan A + 1 = i 2 i A + i
63 8 38 8 mul12i i 2 i = 2 i i
64 ixi i i = 1
65 64 oveq2i 2 i i = 2 -1
66 21 negcli 1
67 38 mulm1i -1 2 = 2
68 66 38 67 mulcomli 2 -1 = 2
69 63 65 68 3eqtri i 2 i = 2
70 69 oveq1i i 2 i A + i = 2 A + i
71 50 5 10 19 divassd A dom arctan i 2 i A + i = i 2 i A + i
72 70 71 eqtr3id A dom arctan 2 A + i = i 2 i A + i
73 62 72 eqtr4d A dom arctan i e 2 i arctan A + 1 = 2 A + i
74 61 73 oveq12d A dom arctan e 2 i arctan A 1 i e 2 i arctan A + 1 = -2 A A + i 2 A + i
75 38 negcli 2
76 mulcl 2 A -2 A
77 75 7 76 sylancr A dom arctan -2 A
78 75 a1i A dom arctan 2
79 2ne0 2 0
80 38 79 negne0i 2 0
81 80 a1i A dom arctan 2 0
82 77 78 10 81 19 divcan7d A dom arctan -2 A A + i 2 A + i = -2 A 2
83 7 78 81 divcan3d A dom arctan -2 A 2 = A
84 82 83 eqtrd A dom arctan -2 A A + i 2 A + i = A
85 74 84 eqtrd A dom arctan e 2 i arctan A 1 i e 2 i arctan A + 1 = A
86 30 85 eqtrd A dom arctan tan arctan A = A