Step | Hyp | Ref
| Expression |
1 | | atanval 26389 |
. . . . 5
β’ (π΄ β dom arctan β
(arctanβπ΄) = ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
2 | 1 | oveq2d 7425 |
. . . 4
β’ (π΄ β dom arctan β ((2
Β· i) Β· (arctanβπ΄)) = ((2 Β· i) Β· ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
3 | | 2cn 12287 |
. . . . . 6
β’ 2 β
β |
4 | 3 | a1i 11 |
. . . . 5
β’ (π΄ β dom arctan β 2
β β) |
5 | | ax-icn 11169 |
. . . . . 6
β’ i β
β |
6 | 5 | a1i 11 |
. . . . 5
β’ (π΄ β dom arctan β i
β β) |
7 | | atancl 26386 |
. . . . 5
β’ (π΄ β dom arctan β
(arctanβπ΄) β
β) |
8 | 4, 6, 7 | mulassd 11237 |
. . . 4
β’ (π΄ β dom arctan β ((2
Β· i) Β· (arctanβπ΄)) = (2 Β· (i Β·
(arctanβπ΄)))) |
9 | | halfcl 12437 |
. . . . . . . . . 10
β’ (i β
β β (i / 2) β β) |
10 | 5, 9 | ax-mp 5 |
. . . . . . . . 9
β’ (i / 2)
β β |
11 | 3, 5, 10 | mulassi 11225 |
. . . . . . . 8
β’ ((2
Β· i) Β· (i / 2)) = (2 Β· (i Β· (i /
2))) |
12 | 3, 5, 10 | mul12i 11409 |
. . . . . . . 8
β’ (2
Β· (i Β· (i / 2))) = (i Β· (2 Β· (i /
2))) |
13 | | 2ne0 12316 |
. . . . . . . . . . 11
β’ 2 β
0 |
14 | 5, 3, 13 | divcan2i 11957 |
. . . . . . . . . 10
β’ (2
Β· (i / 2)) = i |
15 | 14 | oveq2i 7420 |
. . . . . . . . 9
β’ (i
Β· (2 Β· (i / 2))) = (i Β· i) |
16 | | ixi 11843 |
. . . . . . . . 9
β’ (i
Β· i) = -1 |
17 | 15, 16 | eqtri 2761 |
. . . . . . . 8
β’ (i
Β· (2 Β· (i / 2))) = -1 |
18 | 11, 12, 17 | 3eqtri 2765 |
. . . . . . 7
β’ ((2
Β· i) Β· (i / 2)) = -1 |
19 | 18 | oveq1i 7419 |
. . . . . 6
β’ (((2
Β· i) Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) = (-1
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
20 | | ax-1cn 11168 |
. . . . . . . . . 10
β’ 1 β
β |
21 | | atandm2 26382 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
22 | 21 | simp1bi 1146 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β π΄ β
β) |
23 | | mulcl 11194 |
. . . . . . . . . . 11
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
24 | 5, 22, 23 | sylancr 588 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β (i
Β· π΄) β
β) |
25 | | subcl 11459 |
. . . . . . . . . 10
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
26 | 20, 24, 25 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β β) |
27 | 21 | simp2bi 1147 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β 0) |
28 | 26, 27 | logcld 26079 |
. . . . . . . 8
β’ (π΄ β dom arctan β
(logβ(1 β (i Β· π΄))) β β) |
29 | | addcl 11192 |
. . . . . . . . . 10
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
30 | 20, 24, 29 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
β) |
31 | 21 | simp3bi 1148 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
0) |
32 | 30, 31 | logcld 26079 |
. . . . . . . 8
β’ (π΄ β dom arctan β
(logβ(1 + (i Β· π΄))) β β) |
33 | 28, 32 | subcld 11571 |
. . . . . . 7
β’ (π΄ β dom arctan β
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β
β) |
34 | 33 | mulm1d 11666 |
. . . . . 6
β’ (π΄ β dom arctan β (-1
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = -((logβ(1
β (i Β· π΄)))
β (logβ(1 + (i Β· π΄))))) |
35 | 19, 34 | eqtrid 2785 |
. . . . 5
β’ (π΄ β dom arctan β (((2
Β· i) Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) =
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
36 | | 2mulicn 12435 |
. . . . . . 7
β’ (2
Β· i) β β |
37 | 36 | a1i 11 |
. . . . . 6
β’ (π΄ β dom arctan β (2
Β· i) β β) |
38 | 10 | a1i 11 |
. . . . . 6
β’ (π΄ β dom arctan β (i /
2) β β) |
39 | 37, 38, 33 | mulassd 11237 |
. . . . 5
β’ (π΄ β dom arctan β (((2
Β· i) Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) = ((2
Β· i) Β· ((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))))) |
40 | 28, 32 | negsubdi2d 11587 |
. . . . 5
β’ (π΄ β dom arctan β
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) = ((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄))))) |
41 | 35, 39, 40 | 3eqtr3d 2781 |
. . . 4
β’ (π΄ β dom arctan β ((2
Β· i) Β· ((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄)))))) =
((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) |
42 | 2, 8, 41 | 3eqtr3d 2781 |
. . 3
β’ (π΄ β dom arctan β (2
Β· (i Β· (arctanβπ΄))) = ((logβ(1 + (i Β· π΄))) β (logβ(1
β (i Β· π΄))))) |
43 | 42 | fveq2d 6896 |
. 2
β’ (π΄ β dom arctan β
(expβ(2 Β· (i Β· (arctanβπ΄)))) = (expβ((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄)))))) |
44 | | efsub 16043 |
. . 3
β’
(((logβ(1 + (i Β· π΄))) β β β§ (logβ(1
β (i Β· π΄)))
β β) β (expβ((logβ(1 + (i Β· π΄))) β (logβ(1
β (i Β· π΄)))))
= ((expβ(logβ(1 + (i Β· π΄)))) / (expβ(logβ(1 β (i
Β· π΄)))))) |
45 | 32, 28, 44 | syl2anc 585 |
. 2
β’ (π΄ β dom arctan β
(expβ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) =
((expβ(logβ(1 + (i Β· π΄)))) / (expβ(logβ(1 β (i
Β· π΄)))))) |
46 | | eflog 26085 |
. . . . 5
β’ (((1 + (i
Β· π΄)) β β
β§ (1 + (i Β· π΄))
β 0) β (expβ(logβ(1 + (i Β· π΄)))) = (1 + (i Β· π΄))) |
47 | 30, 31, 46 | syl2anc 585 |
. . . 4
β’ (π΄ β dom arctan β
(expβ(logβ(1 + (i Β· π΄)))) = (1 + (i Β· π΄))) |
48 | | eflog 26085 |
. . . . 5
β’ (((1
β (i Β· π΄))
β β β§ (1 β (i Β· π΄)) β 0) β (expβ(logβ(1
β (i Β· π΄)))) =
(1 β (i Β· π΄))) |
49 | 26, 27, 48 | syl2anc 585 |
. . . 4
β’ (π΄ β dom arctan β
(expβ(logβ(1 β (i Β· π΄)))) = (1 β (i Β· π΄))) |
50 | 47, 49 | oveq12d 7427 |
. . 3
β’ (π΄ β dom arctan β
((expβ(logβ(1 + (i Β· π΄)))) / (expβ(logβ(1 β (i
Β· π΄))))) = ((1 + (i
Β· π΄)) / (1 β
(i Β· π΄)))) |
51 | | negsub 11508 |
. . . . . . . 8
β’ ((i
β β β§ π΄
β β) β (i + -π΄) = (i β π΄)) |
52 | 5, 22, 51 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom arctan β (i +
-π΄) = (i β π΄)) |
53 | 6 | mulridd 11231 |
. . . . . . . 8
β’ (π΄ β dom arctan β (i
Β· 1) = i) |
54 | 16 | oveq1i 7419 |
. . . . . . . . 9
β’ ((i
Β· i) Β· π΄) =
(-1 Β· π΄) |
55 | 6, 6, 22 | mulassd 11237 |
. . . . . . . . 9
β’ (π΄ β dom arctan β ((i
Β· i) Β· π΄) =
(i Β· (i Β· π΄))) |
56 | 22 | mulm1d 11666 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (-1
Β· π΄) = -π΄) |
57 | 54, 55, 56 | 3eqtr3a 2797 |
. . . . . . . 8
β’ (π΄ β dom arctan β (i
Β· (i Β· π΄)) =
-π΄) |
58 | 53, 57 | oveq12d 7427 |
. . . . . . 7
β’ (π΄ β dom arctan β ((i
Β· 1) + (i Β· (i Β· π΄))) = (i + -π΄)) |
59 | 6, 22, 6 | pnpcan2d 11609 |
. . . . . . 7
β’ (π΄ β dom arctan β ((i +
i) β (π΄ + i)) = (i
β π΄)) |
60 | 52, 58, 59 | 3eqtr4d 2783 |
. . . . . 6
β’ (π΄ β dom arctan β ((i
Β· 1) + (i Β· (i Β· π΄))) = ((i + i) β (π΄ + i))) |
61 | 20 | a1i 11 |
. . . . . . 7
β’ (π΄ β dom arctan β 1
β β) |
62 | 6, 61, 24 | adddid 11238 |
. . . . . 6
β’ (π΄ β dom arctan β (i
Β· (1 + (i Β· π΄))) = ((i Β· 1) + (i Β· (i
Β· π΄)))) |
63 | 6 | 2timesd 12455 |
. . . . . . 7
β’ (π΄ β dom arctan β (2
Β· i) = (i + i)) |
64 | 63 | oveq1d 7424 |
. . . . . 6
β’ (π΄ β dom arctan β ((2
Β· i) β (π΄ +
i)) = ((i + i) β (π΄ +
i))) |
65 | 60, 62, 64 | 3eqtr4d 2783 |
. . . . 5
β’ (π΄ β dom arctan β (i
Β· (1 + (i Β· π΄))) = ((2 Β· i) β (π΄ + i))) |
66 | 6, 61, 24 | subdid 11670 |
. . . . . 6
β’ (π΄ β dom arctan β (i
Β· (1 β (i Β· π΄))) = ((i Β· 1) β (i Β· (i
Β· π΄)))) |
67 | 53, 57 | oveq12d 7427 |
. . . . . . 7
β’ (π΄ β dom arctan β ((i
Β· 1) β (i Β· (i Β· π΄))) = (i β -π΄)) |
68 | | subneg 11509 |
. . . . . . . 8
β’ ((i
β β β§ π΄
β β) β (i β -π΄) = (i + π΄)) |
69 | 5, 22, 68 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom arctan β (i
β -π΄) = (i + π΄)) |
70 | 67, 69 | eqtrd 2773 |
. . . . . 6
β’ (π΄ β dom arctan β ((i
Β· 1) β (i Β· (i Β· π΄))) = (i + π΄)) |
71 | | addcom 11400 |
. . . . . . 7
β’ ((i
β β β§ π΄
β β) β (i + π΄) = (π΄ + i)) |
72 | 5, 22, 71 | sylancr 588 |
. . . . . 6
β’ (π΄ β dom arctan β (i +
π΄) = (π΄ + i)) |
73 | 66, 70, 72 | 3eqtrd 2777 |
. . . . 5
β’ (π΄ β dom arctan β (i
Β· (1 β (i Β· π΄))) = (π΄ + i)) |
74 | 65, 73 | oveq12d 7427 |
. . . 4
β’ (π΄ β dom arctan β ((i
Β· (1 + (i Β· π΄))) / (i Β· (1 β (i Β·
π΄)))) = (((2 Β· i)
β (π΄ + i)) / (π΄ + i))) |
75 | | ine0 11649 |
. . . . . 6
β’ i β
0 |
76 | 75 | a1i 11 |
. . . . 5
β’ (π΄ β dom arctan β i β
0) |
77 | 30, 26, 6, 27, 76 | divcan5d 12016 |
. . . 4
β’ (π΄ β dom arctan β ((i
Β· (1 + (i Β· π΄))) / (i Β· (1 β (i Β·
π΄)))) = ((1 + (i Β·
π΄)) / (1 β (i
Β· π΄)))) |
78 | | addcl 11192 |
. . . . . 6
β’ ((π΄ β β β§ i β
β) β (π΄ + i)
β β) |
79 | 22, 5, 78 | sylancl 587 |
. . . . 5
β’ (π΄ β dom arctan β (π΄ + i) β
β) |
80 | | subneg 11509 |
. . . . . . 7
β’ ((π΄ β β β§ i β
β) β (π΄ β
-i) = (π΄ +
i)) |
81 | 22, 5, 80 | sylancl 587 |
. . . . . 6
β’ (π΄ β dom arctan β (π΄ β -i) = (π΄ + i)) |
82 | | atandm 26381 |
. . . . . . . 8
β’ (π΄ β dom arctan β (π΄ β β β§ π΄ β -i β§ π΄ β i)) |
83 | 82 | simp2bi 1147 |
. . . . . . 7
β’ (π΄ β dom arctan β π΄ β -i) |
84 | | negicn 11461 |
. . . . . . . 8
β’ -i β
β |
85 | | subeq0 11486 |
. . . . . . . . 9
β’ ((π΄ β β β§ -i β
β) β ((π΄ β
-i) = 0 β π΄ =
-i)) |
86 | 85 | necon3bid 2986 |
. . . . . . . 8
β’ ((π΄ β β β§ -i β
β) β ((π΄ β
-i) β 0 β π΄ β
-i)) |
87 | 22, 84, 86 | sylancl 587 |
. . . . . . 7
β’ (π΄ β dom arctan β
((π΄ β -i) β 0
β π΄ β
-i)) |
88 | 83, 87 | mpbird 257 |
. . . . . 6
β’ (π΄ β dom arctan β (π΄ β -i) β
0) |
89 | 81, 88 | eqnetrrd 3010 |
. . . . 5
β’ (π΄ β dom arctan β (π΄ + i) β 0) |
90 | 37, 79, 79, 89 | divsubdird 12029 |
. . . 4
β’ (π΄ β dom arctan β (((2
Β· i) β (π΄ +
i)) / (π΄ + i)) = (((2
Β· i) / (π΄ + i))
β ((π΄ + i) / (π΄ + i)))) |
91 | 74, 77, 90 | 3eqtr3d 2781 |
. . 3
β’ (π΄ β dom arctan β ((1 +
(i Β· π΄)) / (1
β (i Β· π΄))) =
(((2 Β· i) / (π΄ + i))
β ((π΄ + i) / (π΄ + i)))) |
92 | 79, 89 | dividd 11988 |
. . . 4
β’ (π΄ β dom arctan β
((π΄ + i) / (π΄ + i)) = 1) |
93 | 92 | oveq2d 7425 |
. . 3
β’ (π΄ β dom arctan β (((2
Β· i) / (π΄ + i))
β ((π΄ + i) / (π΄ + i))) = (((2 Β· i) /
(π΄ + i)) β
1)) |
94 | 50, 91, 93 | 3eqtrd 2777 |
. 2
β’ (π΄ β dom arctan β
((expβ(logβ(1 + (i Β· π΄)))) / (expβ(logβ(1 β (i
Β· π΄))))) = (((2
Β· i) / (π΄ + i))
β 1)) |
95 | 43, 45, 94 | 3eqtrd 2777 |
1
β’ (π΄ β dom arctan β
(expβ(2 Β· (i Β· (arctanβπ΄)))) = (((2 Β· i) / (π΄ + i)) β 1)) |