Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β π΄ β
β) |
2 | | simpr 486 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β 0) |
3 | | fveq2 6847 |
. . . . . 6
β’ (π΄ = -i β (ββπ΄) =
(ββ-i)) |
4 | | ax-icn 11117 |
. . . . . . . 8
β’ i β
β |
5 | 4 | renegi 15072 |
. . . . . . 7
β’
(ββ-i) = -(ββi) |
6 | | rei 15048 |
. . . . . . . 8
β’
(ββi) = 0 |
7 | 6 | negeqi 11401 |
. . . . . . 7
β’
-(ββi) = -0 |
8 | | neg0 11454 |
. . . . . . 7
β’ -0 =
0 |
9 | 5, 7, 8 | 3eqtri 2769 |
. . . . . 6
β’
(ββ-i) = 0 |
10 | 3, 9 | eqtrdi 2793 |
. . . . 5
β’ (π΄ = -i β (ββπ΄) = 0) |
11 | 10 | necon3i 2977 |
. . . 4
β’
((ββπ΄)
β 0 β π΄ β
-i) |
12 | 2, 11 | syl 17 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β π΄ β
-i) |
13 | | fveq2 6847 |
. . . . . 6
β’ (π΄ = i β (ββπ΄) =
(ββi)) |
14 | 13, 6 | eqtrdi 2793 |
. . . . 5
β’ (π΄ = i β (ββπ΄) = 0) |
15 | 14 | necon3i 2977 |
. . . 4
β’
((ββπ΄)
β 0 β π΄ β
i) |
16 | 2, 15 | syl 17 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β π΄ β
i) |
17 | | atandm 26242 |
. . 3
β’ (π΄ β dom arctan β (π΄ β β β§ π΄ β -i β§ π΄ β i)) |
18 | 1, 12, 16, 17 | syl3anbrc 1344 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β 0)
β π΄ β dom
arctan) |
19 | | halfcl 12385 |
. . . . . 6
β’ (i β
β β (i / 2) β β) |
20 | 4, 19 | ax-mp 5 |
. . . . 5
β’ (i / 2)
β β |
21 | | ax-1cn 11116 |
. . . . . . . 8
β’ 1 β
β |
22 | | mulcl 11142 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
23 | 4, 1, 22 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· π΄)
β β) |
24 | | subcl 11407 |
. . . . . . . 8
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
25 | 21, 23, 24 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 β (i Β· π΄)) β β) |
26 | | atandm2 26243 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
27 | 18, 26 | sylib 217 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (π΄ β β
β§ (1 β (i Β· π΄)) β 0 β§ (1 + (i Β· π΄)) β 0)) |
28 | 27 | simp2d 1144 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 β (i Β· π΄)) β 0) |
29 | 25, 28 | logcld 25942 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(1 β (i Β· π΄))) β β) |
30 | | addcl 11140 |
. . . . . . . 8
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
31 | 21, 23, 30 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 + (i Β· π΄))
β β) |
32 | 27 | simp3d 1145 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 + (i Β· π΄))
β 0) |
33 | 31, 32 | logcld 25942 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(1 + (i Β· π΄))) β β) |
34 | 29, 33 | subcld 11519 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β
β) |
35 | | cjmul 15034 |
. . . . 5
β’ (((i / 2)
β β β§ ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β β)
β (ββ((i / 2) Β· ((logβ(1 β (i Β·
π΄))) β (logβ(1
+ (i Β· π΄)))))) =
((ββ(i / 2)) Β· (ββ((logβ(1 β (i
Β· π΄))) β
(logβ(1 + (i Β· π΄))))))) |
36 | 20, 34, 35 | sylancr 588 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ((i / 2) Β· ((logβ(1 β (i Β·
π΄))) β (logβ(1
+ (i Β· π΄)))))) =
((ββ(i / 2)) Β· (ββ((logβ(1 β (i
Β· π΄))) β
(logβ(1 + (i Β· π΄))))))) |
37 | | 2ne0 12264 |
. . . . . . . 8
β’ 2 β
0 |
38 | | 2cn 12235 |
. . . . . . . . 9
β’ 2 β
β |
39 | 4, 38 | cjdivi 15083 |
. . . . . . . 8
β’ (2 β 0
β (ββ(i / 2)) = ((ββi) /
(ββ2))) |
40 | 37, 39 | ax-mp 5 |
. . . . . . 7
β’
(ββ(i / 2)) = ((ββi) /
(ββ2)) |
41 | | divneg 11854 |
. . . . . . . . 9
β’ ((i
β β β§ 2 β β β§ 2 β 0) β -(i / 2) = (-i /
2)) |
42 | 4, 38, 37, 41 | mp3an 1462 |
. . . . . . . 8
β’ -(i / 2)
= (-i / 2) |
43 | | cji 15051 |
. . . . . . . . 9
β’
(ββi) = -i |
44 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
45 | | cjre 15031 |
. . . . . . . . . 10
β’ (2 β
β β (ββ2) = 2) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . 9
β’
(ββ2) = 2 |
47 | 43, 46 | oveq12i 7374 |
. . . . . . . 8
β’
((ββi) / (ββ2)) = (-i / 2) |
48 | 42, 47 | eqtr4i 2768 |
. . . . . . 7
β’ -(i / 2)
= ((ββi) / (ββ2)) |
49 | 40, 48 | eqtr4i 2768 |
. . . . . 6
β’
(ββ(i / 2)) = -(i / 2) |
50 | 49 | oveq1i 7372 |
. . . . 5
β’
((ββ(i / 2)) Β· (ββ((logβ(1
β (i Β· π΄)))
β (logβ(1 + (i Β· π΄)))))) = (-(i / 2) Β·
(ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
51 | 34 | cjcld 15088 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) β
β) |
52 | | mulneg12 11600 |
. . . . . 6
β’ (((i / 2)
β β β§ (ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) β
β) β (-(i / 2) Β· (ββ((logβ(1 β (i
Β· π΄))) β
(logβ(1 + (i Β· π΄)))))) = ((i / 2) Β·
-(ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
53 | 20, 51, 52 | sylancr 588 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (-(i / 2) Β· (ββ((logβ(1 β (i Β·
π΄))) β (logβ(1
+ (i Β· π΄)))))) = ((i
/ 2) Β· -(ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))))) |
54 | 50, 53 | eqtrid 2789 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββ(i / 2)) Β· (ββ((logβ(1
β (i Β· π΄)))
β (logβ(1 + (i Β· π΄)))))) = ((i / 2) Β·
-(ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
55 | | cjsub 15041 |
. . . . . . . . 9
β’
(((logβ(1 β (i Β· π΄))) β β β§ (logβ(1 + (i
Β· π΄))) β
β) β (ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) =
((ββ(logβ(1 β (i Β· π΄)))) β (ββ(logβ(1 +
(i Β· π΄)))))) |
56 | 29, 33, 55 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) =
((ββ(logβ(1 β (i Β· π΄)))) β (ββ(logβ(1 +
(i Β· π΄)))))) |
57 | | imsub 15027 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ (i Β· π΄) β β) β (ββ(1
β (i Β· π΄))) =
((ββ1) β (ββ(i Β· π΄)))) |
58 | 21, 23, 57 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 β (i Β· π΄))) = ((ββ1) β
(ββ(i Β· π΄)))) |
59 | | reim 15001 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(ββπ΄) =
(ββ(i Β· π΄))) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄) =
(ββ(i Β· π΄))) |
61 | 60 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββ1) β (ββπ΄)) = ((ββ1) β
(ββ(i Β· π΄)))) |
62 | 58, 61 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 β (i Β· π΄))) = ((ββ1) β
(ββπ΄))) |
63 | | df-neg 11395 |
. . . . . . . . . . . . . 14
β’
-(ββπ΄) =
(0 β (ββπ΄)) |
64 | | im1 15047 |
. . . . . . . . . . . . . . 15
β’
(ββ1) = 0 |
65 | 64 | oveq1i 7372 |
. . . . . . . . . . . . . 14
β’
((ββ1) β (ββπ΄)) = (0 β (ββπ΄)) |
66 | 63, 65 | eqtr4i 2768 |
. . . . . . . . . . . . 13
β’
-(ββπ΄) =
((ββ1) β (ββπ΄)) |
67 | 62, 66 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 β (i Β· π΄))) = -(ββπ΄)) |
68 | | recl 15002 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(ββπ΄) β
β) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β β) |
70 | 69 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β β) |
71 | 70, 2 | negne0d 11517 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β -(ββπ΄)
β 0) |
72 | 67, 71 | eqnetrd 3012 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 β (i Β· π΄))) β 0) |
73 | | logcj 25977 |
. . . . . . . . . . 11
β’ (((1
β (i Β· π΄))
β β β§ (ββ(1 β (i Β· π΄))) β 0) β
(logβ(ββ(1 β (i Β· π΄)))) = (ββ(logβ(1 β
(i Β· π΄))))) |
74 | 25, 72, 73 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(ββ(1 β (i Β· π΄)))) = (ββ(logβ(1 β
(i Β· π΄))))) |
75 | | cjsub 15041 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ (i Β· π΄) β β) β (ββ(1
β (i Β· π΄))) =
((ββ1) β (ββ(i Β· π΄)))) |
76 | 21, 23, 75 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 β (i Β· π΄))) = ((ββ1) β
(ββ(i Β· π΄)))) |
77 | | 1re 11162 |
. . . . . . . . . . . . . 14
β’ 1 β
β |
78 | | cjre 15031 |
. . . . . . . . . . . . . 14
β’ (1 β
β β (ββ1) = 1) |
79 | 77, 78 | mp1i 13 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ1) = 1) |
80 | | cjmul 15034 |
. . . . . . . . . . . . . . 15
β’ ((i
β β β§ π΄
β β) β (ββ(i Β· π΄)) = ((ββi) Β·
(ββπ΄))) |
81 | 4, 1, 80 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(i Β· π΄)) = ((ββi) Β·
(ββπ΄))) |
82 | 43 | oveq1i 7372 |
. . . . . . . . . . . . . . 15
β’
((ββi) Β· (ββπ΄)) = (-i Β· (ββπ΄)) |
83 | | cjcl 14997 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(ββπ΄) β
β) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β β) |
85 | | mulneg1 11598 |
. . . . . . . . . . . . . . . 16
β’ ((i
β β β§ (ββπ΄) β β) β (-i Β·
(ββπ΄)) = -(i
Β· (ββπ΄))) |
86 | 4, 84, 85 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (-i Β· (ββπ΄)) = -(i Β· (ββπ΄))) |
87 | 82, 86 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββi) Β· (ββπ΄)) = -(i Β· (ββπ΄))) |
88 | 81, 87 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(i Β· π΄)) = -(i Β· (ββπ΄))) |
89 | 79, 88 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββ1) β (ββ(i Β· π΄))) = (1 β -(i Β·
(ββπ΄)))) |
90 | | mulcl 11142 |
. . . . . . . . . . . . . 14
β’ ((i
β β β§ (ββπ΄) β β) β (i Β·
(ββπ΄)) β
β) |
91 | 4, 84, 90 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (ββπ΄)) β β) |
92 | | subneg 11457 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ (i Β· (ββπ΄)) β β) β (1 β -(i
Β· (ββπ΄))) = (1 + (i Β· (ββπ΄)))) |
93 | 21, 91, 92 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 β -(i Β· (ββπ΄))) = (1 + (i Β· (ββπ΄)))) |
94 | 76, 89, 93 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 β (i Β· π΄))) = (1 + (i Β· (ββπ΄)))) |
95 | 94 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(ββ(1 β (i Β· π΄)))) = (logβ(1 + (i Β·
(ββπ΄))))) |
96 | 74, 95 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(logβ(1 β (i Β· π΄)))) = (logβ(1 + (i Β·
(ββπ΄))))) |
97 | | imadd 15026 |
. . . . . . . . . . . . . 14
β’ ((1
β β β§ (i Β· π΄) β β) β (ββ(1 +
(i Β· π΄))) =
((ββ1) + (ββ(i Β· π΄)))) |
98 | 21, 23, 97 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 + (i Β· π΄))) = ((ββ1) + (ββ(i
Β· π΄)))) |
99 | 60 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (0 + (ββπ΄)) = (0 + (ββ(i Β· π΄)))) |
100 | 64 | oveq1i 7372 |
. . . . . . . . . . . . . 14
β’
((ββ1) + (ββ(i Β· π΄))) = (0 + (ββ(i Β· π΄))) |
101 | 99, 100 | eqtr4di 2795 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (0 + (ββπ΄)) = ((ββ1) + (ββ(i
Β· π΄)))) |
102 | 70 | addid2d 11363 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (0 + (ββπ΄)) = (ββπ΄)) |
103 | 98, 101, 102 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 + (i Β· π΄))) = (ββπ΄)) |
104 | 103, 2 | eqnetrd 3012 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 + (i Β· π΄))) β 0) |
105 | | logcj 25977 |
. . . . . . . . . . 11
β’ (((1 + (i
Β· π΄)) β β
β§ (ββ(1 + (i Β· π΄))) β 0) β
(logβ(ββ(1 + (i Β· π΄)))) = (ββ(logβ(1 + (i
Β· π΄))))) |
106 | 31, 104, 105 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(ββ(1 + (i Β· π΄)))) = (ββ(logβ(1 + (i
Β· π΄))))) |
107 | | cjadd 15033 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ (i Β· π΄) β β) β (ββ(1
+ (i Β· π΄))) =
((ββ1) + (ββ(i Β· π΄)))) |
108 | 21, 23, 107 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 + (i Β· π΄))) = ((ββ1) +
(ββ(i Β· π΄)))) |
109 | 79, 88 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββ1) + (ββ(i Β· π΄))) = (1 + -(i Β·
(ββπ΄)))) |
110 | | negsub 11456 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ (i Β· (ββπ΄)) β β) β (1 + -(i Β·
(ββπ΄))) = (1
β (i Β· (ββπ΄)))) |
111 | 21, 91, 110 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 + -(i Β· (ββπ΄))) = (1 β (i Β·
(ββπ΄)))) |
112 | 108, 109,
111 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(1 + (i Β· π΄))) = (1 β (i Β·
(ββπ΄)))) |
113 | 112 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(ββ(1 + (i Β· π΄)))) = (logβ(1 β (i Β·
(ββπ΄))))) |
114 | 106, 113 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(logβ(1 + (i Β· π΄)))) = (logβ(1 β (i Β·
(ββπ΄))))) |
115 | 96, 114 | oveq12d 7380 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββ(logβ(1 β (i Β· π΄)))) β (ββ(logβ(1 +
(i Β· π΄))))) =
((logβ(1 + (i Β· (ββπ΄)))) β (logβ(1 β (i
Β· (ββπ΄)))))) |
116 | 56, 115 | eqtrd 2777 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = ((logβ(1 +
(i Β· (ββπ΄)))) β (logβ(1 β (i
Β· (ββπ΄)))))) |
117 | 116 | negeqd 11402 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β -(ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = -((logβ(1 +
(i Β· (ββπ΄)))) β (logβ(1 β (i
Β· (ββπ΄)))))) |
118 | | addcl 11140 |
. . . . . . . . 9
β’ ((1
β β β§ (i Β· (ββπ΄)) β β) β (1 + (i Β·
(ββπ΄))) β
β) |
119 | 21, 91, 118 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 + (i Β· (ββπ΄))) β β) |
120 | | atandmcj 26275 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β
(ββπ΄) β
dom arctan) |
121 | 18, 120 | syl 17 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β dom arctan) |
122 | | atandm2 26243 |
. . . . . . . . . 10
β’
((ββπ΄)
β dom arctan β ((ββπ΄) β β β§ (1 β (i
Β· (ββπ΄))) β 0 β§ (1 + (i Β·
(ββπ΄))) β
0)) |
123 | 122 | simp3bi 1148 |
. . . . . . . . 9
β’
((ββπ΄)
β dom arctan β (1 + (i Β· (ββπ΄))) β 0) |
124 | 121, 123 | syl 17 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 + (i Β· (ββπ΄))) β 0) |
125 | 119, 124 | logcld 25942 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(1 + (i Β· (ββπ΄)))) β β) |
126 | | subcl 11407 |
. . . . . . . . 9
β’ ((1
β β β§ (i Β· (ββπ΄)) β β) β (1 β (i
Β· (ββπ΄))) β β) |
127 | 21, 91, 126 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 β (i Β· (ββπ΄))) β β) |
128 | 122 | simp2bi 1147 |
. . . . . . . . 9
β’
((ββπ΄)
β dom arctan β (1 β (i Β· (ββπ΄))) β 0) |
129 | 121, 128 | syl 17 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (1 β (i Β· (ββπ΄))) β 0) |
130 | 127, 129 | logcld 25942 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβ(1 β (i Β· (ββπ΄)))) β β) |
131 | 125, 130 | negsubdi2d 11535 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β -((logβ(1 + (i Β· (ββπ΄)))) β (logβ(1 β (i
Β· (ββπ΄))))) = ((logβ(1 β (i Β·
(ββπ΄))))
β (logβ(1 + (i Β· (ββπ΄)))))) |
132 | 117, 131 | eqtrd 2777 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β -(ββ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = ((logβ(1
β (i Β· (ββπ΄)))) β (logβ(1 + (i Β·
(ββπ΄)))))) |
133 | 132 | oveq2d 7378 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((i / 2) Β· -(ββ((logβ(1 β (i Β·
π΄))) β (logβ(1
+ (i Β· π΄)))))) = ((i
/ 2) Β· ((logβ(1 β (i Β· (ββπ΄)))) β (logβ(1 + (i
Β· (ββπ΄))))))) |
134 | 36, 54, 133 | 3eqtrd 2781 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ((i / 2) Β· ((logβ(1 β (i Β·
π΄))) β (logβ(1
+ (i Β· π΄)))))) = ((i
/ 2) Β· ((logβ(1 β (i Β· (ββπ΄)))) β (logβ(1 + (i
Β· (ββπ΄))))))) |
135 | | atanval 26250 |
. . . . 5
β’ (π΄ β dom arctan β
(arctanβπ΄) = ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
136 | 18, 135 | syl 17 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (arctanβπ΄) =
((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
137 | 136 | fveq2d 6851 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(arctanβπ΄)) = (ββ((i / 2) Β·
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
138 | | atanval 26250 |
. . . 4
β’
((ββπ΄)
β dom arctan β (arctanβ(ββπ΄)) = ((i / 2) Β· ((logβ(1
β (i Β· (ββπ΄)))) β (logβ(1 + (i Β·
(ββπ΄))))))) |
139 | 121, 138 | syl 17 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (arctanβ(ββπ΄)) = ((i / 2) Β· ((logβ(1
β (i Β· (ββπ΄)))) β (logβ(1 + (i Β·
(ββπ΄))))))) |
140 | 134, 137,
139 | 3eqtr4d 2787 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(arctanβπ΄)) = (arctanβ(ββπ΄))) |
141 | 18, 140 | jca 513 |
1
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (π΄ β dom arctan
β§ (ββ(arctanβπ΄)) = (arctanβ(ββπ΄)))) |