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 ( 𝐴 ∈ dom arctan → ( tan ‘ ( arctan ‘ 𝐴 ) ) = 𝐴 )

Proof

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