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 e. dom arctan -> ( tan ` ( arctan ` A ) ) = A )

Proof

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