Step | Hyp | Ref
| Expression |
1 | | atancl 26247 |
. . 3
β’ (π΄ β dom arctan β
(arctanβπ΄) β
β) |
2 | | 2efiatan 26284 |
. . . . . 6
β’ (π΄ β dom arctan β
(expβ(2 Β· (i Β· (arctanβπ΄)))) = (((2 Β· i) / (π΄ + i)) β 1)) |
3 | 2 | oveq1d 7377 |
. . . . 5
β’ (π΄ β dom arctan β
((expβ(2 Β· (i Β· (arctanβπ΄)))) + 1) = ((((2 Β· i) / (π΄ + i)) β 1) +
1)) |
4 | | 2mulicn 12383 |
. . . . . . . 8
β’ (2
Β· i) β β |
5 | 4 | a1i 11 |
. . . . . . 7
β’ (π΄ β dom arctan β (2
Β· i) β β) |
6 | | atandm 26242 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (π΄ β β β§ π΄ β -i β§ π΄ β i)) |
7 | 6 | simp1bi 1146 |
. . . . . . . 8
β’ (π΄ β dom arctan β π΄ β
β) |
8 | | ax-icn 11117 |
. . . . . . . 8
β’ i β
β |
9 | | addcl 11140 |
. . . . . . . 8
β’ ((π΄ β β β§ i β
β) β (π΄ + i)
β β) |
10 | 7, 8, 9 | sylancl 587 |
. . . . . . 7
β’ (π΄ β dom arctan β (π΄ + i) β
β) |
11 | | subneg 11457 |
. . . . . . . . 9
β’ ((π΄ β β β§ i β
β) β (π΄ β
-i) = (π΄ +
i)) |
12 | 7, 8, 11 | sylancl 587 |
. . . . . . . 8
β’ (π΄ β dom arctan β (π΄ β -i) = (π΄ + i)) |
13 | 6 | simp2bi 1147 |
. . . . . . . . 9
β’ (π΄ β dom arctan β π΄ β -i) |
14 | 8 | negcli 11476 |
. . . . . . . . . 10
β’ -i β
β |
15 | | subeq0 11434 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ -i β
β) β ((π΄ β
-i) = 0 β π΄ =
-i)) |
16 | 15 | necon3bid 2989 |
. . . . . . . . . 10
β’ ((π΄ β β β§ -i β
β) β ((π΄ β
-i) β 0 β π΄ β
-i)) |
17 | 7, 14, 16 | sylancl 587 |
. . . . . . . . 9
β’ (π΄ β dom arctan β
((π΄ β -i) β 0
β π΄ β
-i)) |
18 | 13, 17 | mpbird 257 |
. . . . . . . 8
β’ (π΄ β dom arctan β (π΄ β -i) β
0) |
19 | 12, 18 | eqnetrrd 3013 |
. . . . . . 7
β’ (π΄ β dom arctan β (π΄ + i) β 0) |
20 | 5, 10, 19 | divcld 11938 |
. . . . . 6
β’ (π΄ β dom arctan β ((2
Β· i) / (π΄ + i))
β β) |
21 | | ax-1cn 11116 |
. . . . . 6
β’ 1 β
β |
22 | | npcan 11417 |
. . . . . 6
β’ ((((2
Β· i) / (π΄ + i))
β β β§ 1 β β) β ((((2 Β· i) / (π΄ + i)) β 1) + 1) = ((2
Β· i) / (π΄ +
i))) |
23 | 20, 21, 22 | sylancl 587 |
. . . . 5
β’ (π΄ β dom arctan β ((((2
Β· i) / (π΄ + i))
β 1) + 1) = ((2 Β· i) / (π΄ + i))) |
24 | 3, 23 | eqtrd 2777 |
. . . 4
β’ (π΄ β dom arctan β
((expβ(2 Β· (i Β· (arctanβπ΄)))) + 1) = ((2 Β· i) / (π΄ + i))) |
25 | | 2muline0 12384 |
. . . . . 6
β’ (2
Β· i) β 0 |
26 | 25 | a1i 11 |
. . . . 5
β’ (π΄ β dom arctan β (2
Β· i) β 0) |
27 | 5, 10, 26, 19 | divne0d 11954 |
. . . 4
β’ (π΄ β dom arctan β ((2
Β· i) / (π΄ + i)) β
0) |
28 | 24, 27 | eqnetrd 3012 |
. . 3
β’ (π΄ β dom arctan β
((expβ(2 Β· (i Β· (arctanβπ΄)))) + 1) β 0) |
29 | | tanval3 16023 |
. . 3
β’
(((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 585 |
. 2
β’ (π΄ β dom arctan β
(tanβ(arctanβπ΄)) = (((expβ(2 Β· (i Β·
(arctanβπ΄)))) β
1) / (i Β· ((expβ(2 Β· (i Β· (arctanβπ΄)))) + 1)))) |
31 | 2 | oveq1d 7377 |
. . . . . 6
β’ (π΄ β dom arctan β
((expβ(2 Β· (i Β· (arctanβπ΄)))) β 1) = ((((2 Β· i) / (π΄ + i)) β 1) β
1)) |
32 | 21 | a1i 11 |
. . . . . . . 8
β’ (π΄ β dom arctan β 1
β β) |
33 | 20, 32, 32 | subsub4d 11550 |
. . . . . . 7
β’ (π΄ β dom arctan β ((((2
Β· i) / (π΄ + i))
β 1) β 1) = (((2 Β· i) / (π΄ + i)) β (1 + 1))) |
34 | | df-2 12223 |
. . . . . . . 8
β’ 2 = (1 +
1) |
35 | 34 | oveq2i 7373 |
. . . . . . 7
β’ (((2
Β· i) / (π΄ + i))
β 2) = (((2 Β· i) / (π΄ + i)) β (1 + 1)) |
36 | 33, 35 | eqtr4di 2795 |
. . . . . 6
β’ (π΄ β dom arctan β ((((2
Β· i) / (π΄ + i))
β 1) β 1) = (((2 Β· i) / (π΄ + i)) β 2)) |
37 | 31, 36 | eqtrd 2777 |
. . . . 5
β’ (π΄ β dom arctan β
((expβ(2 Β· (i Β· (arctanβπ΄)))) β 1) = (((2 Β· i) / (π΄ + i)) β
2)) |
38 | | 2cn 12235 |
. . . . . . . 8
β’ 2 β
β |
39 | | mulcl 11142 |
. . . . . . . 8
β’ ((2
β β β§ (π΄ +
i) β β) β (2 Β· (π΄ + i)) β β) |
40 | 38, 10, 39 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom arctan β (2
Β· (π΄ + i)) β
β) |
41 | 5, 40, 10, 19 | divsubdird 11977 |
. . . . . 6
β’ (π΄ β dom arctan β (((2
Β· i) β (2 Β· (π΄ + i))) / (π΄ + i)) = (((2 Β· i) / (π΄ + i)) β ((2 Β·
(π΄ + i)) / (π΄ + i)))) |
42 | | mulneg12 11600 |
. . . . . . . . 9
β’ ((2
β β β§ π΄
β β) β (-2 Β· π΄) = (2 Β· -π΄)) |
43 | 38, 7, 42 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β dom arctan β (-2
Β· π΄) = (2 Β·
-π΄)) |
44 | | negsub 11456 |
. . . . . . . . . . . 12
β’ ((i
β β β§ π΄
β β) β (i + -π΄) = (i β π΄)) |
45 | 8, 7, 44 | sylancr 588 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β (i +
-π΄) = (i β π΄)) |
46 | 45 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β ((i +
-π΄) β i) = ((i
β π΄) β
i)) |
47 | 7 | negcld 11506 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β -π΄ β
β) |
48 | | pncan2 11415 |
. . . . . . . . . . 11
β’ ((i
β β β§ -π΄
β β) β ((i + -π΄) β i) = -π΄) |
49 | 8, 47, 48 | sylancr 588 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β ((i +
-π΄) β i) = -π΄) |
50 | 8 | a1i 11 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β i
β β) |
51 | 50, 7, 50 | subsub4d 11550 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β ((i
β π΄) β i) = (i
β (π΄ +
i))) |
52 | 46, 49, 51 | 3eqtr3rd 2786 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (i
β (π΄ + i)) = -π΄) |
53 | 52 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β dom arctan β (2
Β· (i β (π΄ +
i))) = (2 Β· -π΄)) |
54 | 38 | a1i 11 |
. . . . . . . . 9
β’ (π΄ β dom arctan β 2
β β) |
55 | 54, 50, 10 | subdid 11618 |
. . . . . . . 8
β’ (π΄ β dom arctan β (2
Β· (i β (π΄ +
i))) = ((2 Β· i) β (2 Β· (π΄ + i)))) |
56 | 43, 53, 55 | 3eqtr2rd 2784 |
. . . . . . 7
β’ (π΄ β dom arctan β ((2
Β· i) β (2 Β· (π΄ + i))) = (-2 Β· π΄)) |
57 | 56 | oveq1d 7377 |
. . . . . 6
β’ (π΄ β dom arctan β (((2
Β· i) β (2 Β· (π΄ + i))) / (π΄ + i)) = ((-2 Β· π΄) / (π΄ + i))) |
58 | 54, 10, 19 | divcan4d 11944 |
. . . . . . 7
β’ (π΄ β dom arctan β ((2
Β· (π΄ + i)) / (π΄ + i)) = 2) |
59 | 58 | oveq2d 7378 |
. . . . . 6
β’ (π΄ β dom arctan β (((2
Β· i) / (π΄ + i))
β ((2 Β· (π΄ +
i)) / (π΄ + i))) = (((2
Β· i) / (π΄ + i))
β 2)) |
60 | 41, 57, 59 | 3eqtr3d 2785 |
. . . . 5
β’ (π΄ β dom arctan β ((-2
Β· π΄) / (π΄ + i)) = (((2 Β· i) /
(π΄ + i)) β
2)) |
61 | 37, 60 | eqtr4d 2780 |
. . . 4
β’ (π΄ β dom arctan β
((expβ(2 Β· (i Β· (arctanβπ΄)))) β 1) = ((-2 Β· π΄) / (π΄ + i))) |
62 | 24 | oveq2d 7378 |
. . . . 5
β’ (π΄ β dom arctan β (i
Β· ((expβ(2 Β· (i Β· (arctanβπ΄)))) + 1)) = (i Β· ((2 Β· i) /
(π΄ + i)))) |
63 | 8, 38, 8 | mul12i 11357 |
. . . . . . . 8
β’ (i
Β· (2 Β· i)) = (2 Β· (i Β· i)) |
64 | | ixi 11791 |
. . . . . . . . 9
β’ (i
Β· i) = -1 |
65 | 64 | oveq2i 7373 |
. . . . . . . 8
β’ (2
Β· (i Β· i)) = (2 Β· -1) |
66 | 21 | negcli 11476 |
. . . . . . . . 9
β’ -1 β
β |
67 | 38 | mulm1i 11607 |
. . . . . . . . 9
β’ (-1
Β· 2) = -2 |
68 | 66, 38, 67 | mulcomli 11171 |
. . . . . . . 8
β’ (2
Β· -1) = -2 |
69 | 63, 65, 68 | 3eqtri 2769 |
. . . . . . 7
β’ (i
Β· (2 Β· i)) = -2 |
70 | 69 | oveq1i 7372 |
. . . . . 6
β’ ((i
Β· (2 Β· i)) / (π΄ + i)) = (-2 / (π΄ + i)) |
71 | 50, 5, 10, 19 | divassd 11973 |
. . . . . 6
β’ (π΄ β dom arctan β ((i
Β· (2 Β· i)) / (π΄ + i)) = (i Β· ((2 Β· i) /
(π΄ + i)))) |
72 | 70, 71 | eqtr3id 2791 |
. . . . 5
β’ (π΄ β dom arctan β (-2 /
(π΄ + i)) = (i Β· ((2
Β· i) / (π΄ +
i)))) |
73 | 62, 72 | eqtr4d 2780 |
. . . 4
β’ (π΄ β dom arctan β (i
Β· ((expβ(2 Β· (i Β· (arctanβπ΄)))) + 1)) = (-2 / (π΄ + i))) |
74 | 61, 73 | oveq12d 7380 |
. . 3
β’ (π΄ β dom arctan β
(((expβ(2 Β· (i Β· (arctanβπ΄)))) β 1) / (i Β· ((expβ(2
Β· (i Β· (arctanβπ΄)))) + 1))) = (((-2 Β· π΄) / (π΄ + i)) / (-2 / (π΄ + i)))) |
75 | 38 | negcli 11476 |
. . . . . 6
β’ -2 β
β |
76 | | mulcl 11142 |
. . . . . 6
β’ ((-2
β β β§ π΄
β β) β (-2 Β· π΄) β β) |
77 | 75, 7, 76 | sylancr 588 |
. . . . 5
β’ (π΄ β dom arctan β (-2
Β· π΄) β
β) |
78 | 75 | a1i 11 |
. . . . 5
β’ (π΄ β dom arctan β -2
β β) |
79 | | 2ne0 12264 |
. . . . . . 7
β’ 2 β
0 |
80 | 38, 79 | negne0i 11483 |
. . . . . 6
β’ -2 β
0 |
81 | 80 | a1i 11 |
. . . . 5
β’ (π΄ β dom arctan β -2
β 0) |
82 | 77, 78, 10, 81, 19 | divcan7d 11966 |
. . . 4
β’ (π΄ β dom arctan β (((-2
Β· π΄) / (π΄ + i)) / (-2 / (π΄ + i))) = ((-2 Β· π΄) / -2)) |
83 | 7, 78, 81 | divcan3d 11943 |
. . . 4
β’ (π΄ β dom arctan β ((-2
Β· π΄) / -2) = π΄) |
84 | 82, 83 | eqtrd 2777 |
. . 3
β’ (π΄ β dom arctan β (((-2
Β· π΄) / (π΄ + i)) / (-2 / (π΄ + i))) = π΄) |
85 | 74, 84 | eqtrd 2777 |
. 2
β’ (π΄ β dom arctan β
(((expβ(2 Β· (i Β· (arctanβπ΄)))) β 1) / (i Β· ((expβ(2
Β· (i Β· (arctanβπ΄)))) + 1))) = π΄) |
86 | 30, 85 | eqtrd 2777 |
1
β’ (π΄ β dom arctan β
(tanβ(arctanβπ΄)) = π΄) |