Step | Hyp | Ref
| Expression |
1 | | cosne0 25901 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) β 0) |
2 | | atandmtan 26286 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (tanβπ΄) β
dom arctan) |
3 | 1, 2 | syldan 592 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (tanβπ΄) β dom arctan) |
4 | | atanval 26250 |
. . 3
β’
((tanβπ΄)
β dom arctan β (arctanβ(tanβπ΄)) = ((i / 2) Β· ((logβ(1
β (i Β· (tanβπ΄)))) β (logβ(1 + (i Β·
(tanβπ΄))))))) |
5 | 3, 4 | syl 17 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (arctanβ(tanβπ΄)) = ((i / 2) Β· ((logβ(1
β (i Β· (tanβπ΄)))) β (logβ(1 + (i Β·
(tanβπ΄))))))) |
6 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
7 | | ax-icn 11117 |
. . . . . . . 8
β’ i β
β |
8 | | tancl 16018 |
. . . . . . . . 9
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (tanβπ΄) β
β) |
9 | 1, 8 | syldan 592 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (tanβπ΄) β β) |
10 | | mulcl 11142 |
. . . . . . . 8
β’ ((i
β β β§ (tanβπ΄) β β) β (i Β·
(tanβπ΄)) β
β) |
11 | 7, 9, 10 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (tanβπ΄)) β β) |
12 | | addcl 11140 |
. . . . . . 7
β’ ((1
β β β§ (i Β· (tanβπ΄)) β β) β (1 + (i Β·
(tanβπ΄))) β
β) |
13 | 6, 11, 12 | sylancr 588 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 + (i Β· (tanβπ΄))) β
β) |
14 | | atandm2 26243 |
. . . . . . . 8
β’
((tanβπ΄)
β dom arctan β ((tanβπ΄) β β β§ (1 β (i
Β· (tanβπ΄)))
β 0 β§ (1 + (i Β· (tanβπ΄))) β 0)) |
15 | 3, 14 | sylib 217 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((tanβπ΄) β β β§ (1 β (i
Β· (tanβπ΄)))
β 0 β§ (1 + (i Β· (tanβπ΄))) β 0)) |
16 | 15 | simp3d 1145 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 + (i Β· (tanβπ΄))) β 0) |
17 | 13, 16 | logcld 25942 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ(1 + (i Β· (tanβπ΄)))) β
β) |
18 | | subcl 11407 |
. . . . . . 7
β’ ((1
β β β§ (i Β· (tanβπ΄)) β β) β (1 β (i
Β· (tanβπ΄)))
β β) |
19 | 6, 11, 18 | sylancr 588 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 β (i Β· (tanβπ΄))) β
β) |
20 | 15 | simp2d 1144 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 β (i Β· (tanβπ΄))) β 0) |
21 | 19, 20 | logcld 25942 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ(1 β (i Β·
(tanβπ΄)))) β
β) |
22 | 17, 21 | negsubdi2d 11535 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))) = ((logβ(1 β (i Β·
(tanβπ΄)))) β
(logβ(1 + (i Β· (tanβπ΄)))))) |
23 | | efsub 15989 |
. . . . . . . . 9
β’
(((logβ(1 + (i Β· (tanβπ΄)))) β β β§ (logβ(1
β (i Β· (tanβπ΄)))) β β) β
(expβ((logβ(1 + (i Β· (tanβπ΄)))) β (logβ(1 β (i
Β· (tanβπ΄))))))
= ((expβ(logβ(1 + (i Β· (tanβπ΄))))) / (expβ(logβ(1 β (i
Β· (tanβπ΄))))))) |
24 | 17, 21, 23 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄)))))) = ((expβ(logβ(1 + (i
Β· (tanβπ΄)))))
/ (expβ(logβ(1 β (i Β· (tanβπ΄))))))) |
25 | | coscl 16016 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
(cosβπ΄) β
β) |
26 | 25 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) β β) |
27 | | sincl 16015 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
(sinβπ΄) β
β) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (sinβπ΄) β β) |
29 | | mulcl 11142 |
. . . . . . . . . . . . 13
β’ ((i
β β β§ (sinβπ΄) β β) β (i Β·
(sinβπ΄)) β
β) |
30 | 7, 28, 29 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (sinβπ΄)) β β) |
31 | 26, 30, 26, 1 | divdird 11976 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) + (i Β· (sinβπ΄))) / (cosβπ΄)) = (((cosβπ΄) / (cosβπ΄)) + ((i Β· (sinβπ΄)) / (cosβπ΄)))) |
32 | 26, 1 | dividd 11936 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((cosβπ΄) / (cosβπ΄)) = 1) |
33 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β i β β) |
34 | 33, 28, 26, 1 | divassd 11973 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· (sinβπ΄)) / (cosβπ΄)) = (i Β· ((sinβπ΄) / (cosβπ΄)))) |
35 | | tanval 16017 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
36 | 1, 35 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (tanβπ΄) = ((sinβπ΄) / (cosβπ΄))) |
37 | 36 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (tanβπ΄)) = (i Β· ((sinβπ΄) / (cosβπ΄)))) |
38 | 34, 37 | eqtr4d 2780 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· (sinβπ΄)) / (cosβπ΄)) = (i Β· (tanβπ΄))) |
39 | 32, 38 | oveq12d 7380 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) / (cosβπ΄)) + ((i Β· (sinβπ΄)) / (cosβπ΄))) = (1 + (i Β·
(tanβπ΄)))) |
40 | 31, 39 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) + (i Β· (sinβπ΄))) / (cosβπ΄)) = (1 + (i Β· (tanβπ΄)))) |
41 | | efival 16041 |
. . . . . . . . . . . 12
β’ (π΄ β β β
(expβ(i Β· π΄))
= ((cosβπ΄) + (i
Β· (sinβπ΄)))) |
42 | 41 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· π΄)) = ((cosβπ΄) + (i Β· (sinβπ΄)))) |
43 | 42 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) / (cosβπ΄)) = (((cosβπ΄) + (i Β· (sinβπ΄))) / (cosβπ΄))) |
44 | | eflog 25948 |
. . . . . . . . . . 11
β’ (((1 + (i
Β· (tanβπ΄)))
β β β§ (1 + (i Β· (tanβπ΄))) β 0) β (expβ(logβ(1
+ (i Β· (tanβπ΄))))) = (1 + (i Β· (tanβπ΄)))) |
45 | 13, 16, 44 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(logβ(1 + (i Β·
(tanβπ΄))))) = (1 + (i
Β· (tanβπ΄)))) |
46 | 40, 43, 45 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) / (cosβπ΄)) = (expβ(logβ(1 + (i Β·
(tanβπ΄)))))) |
47 | 26, 30, 26, 1 | divsubdird 11977 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) β (i Β· (sinβπ΄))) / (cosβπ΄)) = (((cosβπ΄) / (cosβπ΄)) β ((i Β· (sinβπ΄)) / (cosβπ΄)))) |
48 | 32, 38 | oveq12d 7380 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) / (cosβπ΄)) β ((i Β· (sinβπ΄)) / (cosβπ΄))) = (1 β (i Β·
(tanβπ΄)))) |
49 | 47, 48 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) β (i Β· (sinβπ΄))) / (cosβπ΄)) = (1 β (i Β·
(tanβπ΄)))) |
50 | | negcl 11408 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β -π΄ β
β) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -π΄ β β) |
52 | | efival 16041 |
. . . . . . . . . . . . . 14
β’ (-π΄ β β β
(expβ(i Β· -π΄))
= ((cosβ-π΄) + (i
Β· (sinβ-π΄)))) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· -π΄)) = ((cosβ-π΄) + (i Β· (sinβ-π΄)))) |
54 | | cosneg 16036 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(cosβ-π΄) =
(cosβπ΄)) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβ-π΄) = (cosβπ΄)) |
56 | | sinneg 16035 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(sinβ-π΄) =
-(sinβπ΄)) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (sinβ-π΄) = -(sinβπ΄)) |
58 | 57 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (sinβ-π΄)) = (i Β· -(sinβπ΄))) |
59 | | mulneg2 11599 |
. . . . . . . . . . . . . . . 16
β’ ((i
β β β§ (sinβπ΄) β β) β (i Β·
-(sinβπ΄)) = -(i
Β· (sinβπ΄))) |
60 | 7, 28, 59 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· -(sinβπ΄)) = -(i Β· (sinβπ΄))) |
61 | 58, 60 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (sinβ-π΄)) = -(i Β· (sinβπ΄))) |
62 | 55, 61 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((cosβ-π΄) + (i Β· (sinβ-π΄))) = ((cosβπ΄) + -(i Β·
(sinβπ΄)))) |
63 | 53, 62 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· -π΄)) = ((cosβπ΄) + -(i Β· (sinβπ΄)))) |
64 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β π΄ β β) |
65 | | mulneg2 11599 |
. . . . . . . . . . . . . 14
β’ ((i
β β β§ π΄
β β) β (i Β· -π΄) = -(i Β· π΄)) |
66 | 7, 64, 65 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· -π΄) = -(i Β· π΄)) |
67 | 66 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· -π΄)) = (expβ-(i Β· π΄))) |
68 | 26, 30 | negsubd 11525 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((cosβπ΄) + -(i Β· (sinβπ΄))) = ((cosβπ΄) β (i Β·
(sinβπ΄)))) |
69 | 63, 67, 68 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ-(i Β· π΄)) = ((cosβπ΄) β (i Β· (sinβπ΄)))) |
70 | 69 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ-(i Β· π΄)) / (cosβπ΄)) = (((cosβπ΄) β (i Β· (sinβπ΄))) / (cosβπ΄))) |
71 | | eflog 25948 |
. . . . . . . . . . 11
β’ (((1
β (i Β· (tanβπ΄))) β β β§ (1 β (i
Β· (tanβπ΄)))
β 0) β (expβ(logβ(1 β (i Β· (tanβπ΄))))) = (1 β (i Β·
(tanβπ΄)))) |
72 | 19, 20, 71 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(logβ(1 β (i Β·
(tanβπ΄))))) = (1
β (i Β· (tanβπ΄)))) |
73 | 49, 70, 72 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ-(i Β· π΄)) / (cosβπ΄)) = (expβ(logβ(1 β (i
Β· (tanβπ΄)))))) |
74 | 46, 73 | oveq12d 7380 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄)) / (cosβπ΄)) / ((expβ-(i Β· π΄)) / (cosβπ΄))) = ((expβ(logβ(1
+ (i Β· (tanβπ΄))))) / (expβ(logβ(1 β (i
Β· (tanβπ΄))))))) |
75 | | mulcl 11142 |
. . . . . . . . . . . 12
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
76 | 7, 64, 75 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· π΄) β β) |
77 | | efcl 15972 |
. . . . . . . . . . 11
β’ ((i
Β· π΄) β β
β (expβ(i Β· π΄)) β β) |
78 | 76, 77 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· π΄)) β β) |
79 | 76 | negcld 11506 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -(i Β· π΄) β β) |
80 | | efcl 15972 |
. . . . . . . . . . 11
β’ (-(i
Β· π΄) β β
β (expβ-(i Β· π΄)) β β) |
81 | 79, 80 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ-(i Β· π΄)) β β) |
82 | | efne0 15986 |
. . . . . . . . . . 11
β’ (-(i
Β· π΄) β β
β (expβ-(i Β· π΄)) β 0) |
83 | 79, 82 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ-(i Β· π΄)) β 0) |
84 | 78, 81, 26, 83, 1 | divcan7d 11966 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄)) / (cosβπ΄)) / ((expβ-(i Β· π΄)) / (cosβπ΄))) = ((expβ(i Β·
π΄)) / (expβ-(i
Β· π΄)))) |
85 | | efsub 15989 |
. . . . . . . . . 10
β’ (((i
Β· π΄) β β
β§ -(i Β· π΄)
β β) β (expβ((i Β· π΄) β -(i Β· π΄))) = ((expβ(i Β· π΄)) / (expβ-(i Β·
π΄)))) |
86 | 76, 79, 85 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ((i Β· π΄) β -(i Β· π΄))) = ((expβ(i Β· π΄)) / (expβ-(i Β·
π΄)))) |
87 | 76, 76 | subnegd 11526 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· π΄) β -(i Β· π΄)) = ((i Β· π΄) + (i Β· π΄))) |
88 | 76 | 2timesd 12403 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (i Β· π΄)) = ((i Β· π΄) + (i Β· π΄))) |
89 | 87, 88 | eqtr4d 2780 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· π΄) β -(i Β· π΄)) = (2 Β· (i Β· π΄))) |
90 | 89 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ((i Β· π΄) β -(i Β· π΄))) = (expβ(2 Β· (i Β·
π΄)))) |
91 | 84, 86, 90 | 3eqtr2d 2783 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄)) / (cosβπ΄)) / ((expβ-(i Β· π΄)) / (cosβπ΄))) = (expβ(2 Β· (i
Β· π΄)))) |
92 | 24, 74, 91 | 3eqtr2d 2783 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄)))))) = (expβ(2 Β· (i Β·
π΄)))) |
93 | 92 | fveq2d 6851 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ(expβ((logβ(1 + (i
Β· (tanβπ΄))))
β (logβ(1 β (i Β· (tanβπ΄))))))) = (logβ(expβ(2 Β·
(i Β· π΄))))) |
94 | 64 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β π΄ β β) |
95 | 94 | renegd 15101 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β (ββ-π΄) = -(ββπ΄)) |
96 | 94 | recld 15086 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β (ββπ΄) β
β) |
97 | 96 | renegcld 11589 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β -(ββπ΄) β
β) |
98 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β (ββπ΄) < 0) |
99 | 96 | lt0neg1d 11731 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β ((ββπ΄) < 0 β 0 <
-(ββπ΄))) |
100 | 98, 99 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β 0 < -(ββπ΄)) |
101 | | eliooord 13330 |
. . . . . . . . . . . . . . . . . . 19
β’
((ββπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β (-(Ο / 2) < (ββπ΄) β§ (ββπ΄) < (Ο /
2))) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-(Ο / 2) < (ββπ΄) β§ (ββπ΄) < (Ο /
2))) |
103 | 102 | simpld 496 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -(Ο / 2) < (ββπ΄)) |
104 | 103 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β -(Ο / 2) <
(ββπ΄)) |
105 | | halfpire 25837 |
. . . . . . . . . . . . . . . . 17
β’ (Ο /
2) β β |
106 | | ltnegcon1 11663 |
. . . . . . . . . . . . . . . . 17
β’ (((Ο /
2) β β β§ (ββπ΄) β β) β (-(Ο / 2) <
(ββπ΄) β
-(ββπ΄) <
(Ο / 2))) |
107 | 105, 96, 106 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β (-(Ο / 2) <
(ββπ΄) β
-(ββπ΄) <
(Ο / 2))) |
108 | 104, 107 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β -(ββπ΄) < (Ο /
2)) |
109 | | 0xr 11209 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β* |
110 | 105 | rexri 11220 |
. . . . . . . . . . . . . . . 16
β’ (Ο /
2) β β* |
111 | | elioo2 13312 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β* β§ (Ο / 2) β β*) β
(-(ββπ΄) β
(0(,)(Ο / 2)) β (-(ββπ΄) β β β§ 0 <
-(ββπ΄) β§
-(ββπ΄) <
(Ο / 2)))) |
112 | 109, 110,
111 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
(-(ββπ΄)
β (0(,)(Ο / 2)) β (-(ββπ΄) β β β§ 0 <
-(ββπ΄) β§
-(ββπ΄) <
(Ο / 2))) |
113 | 97, 100, 108, 112 | syl3anbrc 1344 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β -(ββπ΄) β (0(,)(Ο /
2))) |
114 | 95, 113 | eqeltrd 2838 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β (ββ-π΄) β (0(,)(Ο /
2))) |
115 | | tanregt0 25911 |
. . . . . . . . . . . . 13
β’ ((-π΄ β β β§
(ββ-π΄) β
(0(,)(Ο / 2))) β 0 < (ββ(tanβ-π΄))) |
116 | 51, 114, 115 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β 0 <
(ββ(tanβ-π΄))) |
117 | | tanneg 16037 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (tanβ-π΄) =
-(tanβπ΄)) |
118 | 1, 117 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (tanβ-π΄) = -(tanβπ΄)) |
119 | 118 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β (tanβ-π΄) = -(tanβπ΄)) |
120 | 119 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β
(ββ(tanβ-π΄)) = (ββ-(tanβπ΄))) |
121 | 9 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β (tanβπ΄) β
β) |
122 | 121 | renegd 15101 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β
(ββ-(tanβπ΄)) = -(ββ(tanβπ΄))) |
123 | 120, 122 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β
(ββ(tanβ-π΄)) = -(ββ(tanβπ΄))) |
124 | 116, 123 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β 0 <
-(ββ(tanβπ΄))) |
125 | 9 | recld 15086 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(tanβπ΄)) β β) |
126 | 125 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β
(ββ(tanβπ΄)) β β) |
127 | 126 | lt0neg1d 11731 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β
((ββ(tanβπ΄)) < 0 β 0 <
-(ββ(tanβπ΄)))) |
128 | 124, 127 | mpbird 257 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β
(ββ(tanβπ΄)) < 0) |
129 | 128 | lt0ne0d 11727 |
. . . . . . . . 9
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β
(ββ(tanβπ΄)) β 0) |
130 | | atanlogsub 26282 |
. . . . . . . . 9
β’
(((tanβπ΄)
β dom arctan β§ (ββ(tanβπ΄)) β 0) β ((logβ(1 + (i
Β· (tanβπ΄))))
β (logβ(1 β (i Β· (tanβπ΄))))) β ran log) |
131 | 3, 129, 130 | syl2an2r 684 |
. . . . . . . 8
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) < 0) β ((logβ(1 + (i
Β· (tanβπ΄))))
β (logβ(1 β (i Β· (tanβπ΄))))) β ran log) |
132 | | 1re 11162 |
. . . . . . . . . . . . 13
β’ 1 β
β |
133 | | ioossre 13332 |
. . . . . . . . . . . . . 14
β’ (-1(,)1)
β β |
134 | 7 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β i β
β) |
135 | 11 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· (tanβπ΄)) β
β) |
136 | | ine0 11597 |
. . . . . . . . . . . . . . . . 17
β’ i β
0 |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β i β 0) |
138 | | ixi 11791 |
. . . . . . . . . . . . . . . . . . 19
β’ (i
Β· i) = -1 |
139 | 138 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . 18
β’ ((i
Β· i) Β· (tanβπ΄)) = (-1 Β· (tanβπ΄)) |
140 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (tanβπ΄) β β) |
141 | 140 | mulm1d 11614 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (-1 Β· (tanβπ΄)) = -(tanβπ΄)) |
142 | 118 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (tanβ-π΄) = -(tanβπ΄)) |
143 | 141, 142 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (-1 Β· (tanβπ΄)) = (tanβ-π΄)) |
144 | 139, 143 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((i Β· i) Β·
(tanβπ΄)) =
(tanβ-π΄)) |
145 | 134, 134,
140 | mulassd 11185 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((i Β· i) Β·
(tanβπ΄)) = (i
Β· (i Β· (tanβπ΄)))) |
146 | 138 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((i
Β· i) Β· π΄) =
(-1 Β· π΄) |
147 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β π΄ β β) |
148 | 147 | mulm1d 11614 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (-1 Β· π΄) = -π΄) |
149 | 146, 148 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((i Β· i) Β· π΄) = -π΄) |
150 | 134, 134,
147 | mulassd 11185 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((i Β· i) Β· π΄) = (i Β· (i Β·
π΄))) |
151 | 149, 150 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β -π΄ = (i Β· (i Β· π΄))) |
152 | 151 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (tanβ-π΄) = (tanβ(i Β· (i Β· π΄)))) |
153 | 144, 145,
152 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· (i Β·
(tanβπ΄))) =
(tanβ(i Β· (i Β· π΄)))) |
154 | 134, 135,
137, 153 | mvllmuld 11994 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· (tanβπ΄)) = ((tanβ(i Β· (i
Β· π΄))) /
i)) |
155 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· π΄) β β) |
156 | | reim 15001 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β β
(ββπ΄) =
(ββ(i Β· π΄))) |
157 | 156 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) = (ββ(i Β· π΄))) |
158 | 157 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((ββπ΄) = 0 β (ββ(i Β·
π΄)) = 0)) |
159 | 158 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (ββ(i Β·
π΄)) = 0) |
160 | 155, 159 | reim0bd 15092 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· π΄) β β) |
161 | | tanhbnd 16050 |
. . . . . . . . . . . . . . . 16
β’ ((i
Β· π΄) β β
β ((tanβ(i Β· (i Β· π΄))) / i) β (-1(,)1)) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((tanβ(i Β· (i
Β· π΄))) / i) β
(-1(,)1)) |
163 | 154, 162 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· (tanβπ΄)) β
(-1(,)1)) |
164 | 133, 163 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· (tanβπ΄)) β
β) |
165 | | readdcl 11141 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ (i Β· (tanβπ΄)) β β) β (1 + (i Β·
(tanβπ΄))) β
β) |
166 | 132, 164,
165 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (1 + (i Β·
(tanβπ΄))) β
β) |
167 | | df-neg 11395 |
. . . . . . . . . . . . . 14
β’ -1 = (0
β 1) |
168 | | eliooord 13330 |
. . . . . . . . . . . . . . . 16
β’ ((i
Β· (tanβπ΄))
β (-1(,)1) β (-1 < (i Β· (tanβπ΄)) β§ (i Β· (tanβπ΄)) < 1)) |
169 | 163, 168 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (-1 < (i Β·
(tanβπ΄)) β§ (i
Β· (tanβπ΄))
< 1)) |
170 | 169 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β -1 < (i Β·
(tanβπ΄))) |
171 | 167, 170 | eqbrtrrid 5146 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (0 β 1) < (i Β·
(tanβπ΄))) |
172 | | 0red 11165 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β 0 β
β) |
173 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β 1 β
β) |
174 | 172, 173,
164 | ltsubadd2d 11760 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((0 β 1) < (i
Β· (tanβπ΄))
β 0 < (1 + (i Β· (tanβπ΄))))) |
175 | 171, 174 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β 0 < (1 + (i Β·
(tanβπ΄)))) |
176 | 166, 175 | elrpd 12961 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (1 + (i Β·
(tanβπ΄))) β
β+) |
177 | 176 | relogcld 25994 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (logβ(1 + (i Β·
(tanβπ΄)))) β
β) |
178 | 169 | simprd 497 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (i Β· (tanβπ΄)) < 1) |
179 | | difrp 12960 |
. . . . . . . . . . . . 13
β’ (((i
Β· (tanβπ΄))
β β β§ 1 β β) β ((i Β· (tanβπ΄)) < 1 β (1 β (i
Β· (tanβπ΄)))
β β+)) |
180 | 164, 132,
179 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((i Β· (tanβπ΄)) < 1 β (1 β (i
Β· (tanβπ΄)))
β β+)) |
181 | 178, 180 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (1 β (i Β·
(tanβπ΄))) β
β+) |
182 | 181 | relogcld 25994 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β (logβ(1 β (i
Β· (tanβπ΄))))
β β) |
183 | 177, 182 | resubcld 11590 |
. . . . . . . . 9
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))) β β) |
184 | | relogrn 25933 |
. . . . . . . . 9
β’
(((logβ(1 + (i Β· (tanβπ΄)))) β (logβ(1 β (i
Β· (tanβπ΄)))))
β β β ((logβ(1 + (i Β· (tanβπ΄)))) β (logβ(1 β (i
Β· (tanβπ΄)))))
β ran log) |
185 | 183, 184 | syl 17 |
. . . . . . . 8
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (ββπ΄) = 0) β ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))) β ran log) |
186 | 64 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β π΄ β β) |
187 | 186 | recld 15086 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β (ββπ΄) β β) |
188 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β 0 < (ββπ΄)) |
189 | 102 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) < (Ο / 2)) |
190 | 189 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β (ββπ΄) < (Ο / 2)) |
191 | | elioo2 13312 |
. . . . . . . . . . . . 13
β’ ((0
β β* β§ (Ο / 2) β β*) β
((ββπ΄) β
(0(,)(Ο / 2)) β ((ββπ΄) β β β§ 0 <
(ββπ΄) β§
(ββπ΄) < (Ο
/ 2)))) |
192 | 109, 110,
191 | mp2an 691 |
. . . . . . . . . . . 12
β’
((ββπ΄)
β (0(,)(Ο / 2)) β ((ββπ΄) β β β§ 0 <
(ββπ΄) β§
(ββπ΄) < (Ο
/ 2))) |
193 | 187, 188,
190, 192 | syl3anbrc 1344 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β (ββπ΄) β (0(,)(Ο / 2))) |
194 | | tanregt0 25911 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(0(,)(Ο / 2))) β 0 < (ββ(tanβπ΄))) |
195 | 64, 193, 194 | syl2an2r 684 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β 0 <
(ββ(tanβπ΄))) |
196 | 195 | gt0ne0d 11726 |
. . . . . . . . 9
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β (ββ(tanβπ΄)) β 0) |
197 | 3, 196, 130 | syl2an2r 684 |
. . . . . . . 8
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ 0 < (ββπ΄)) β ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))) β ran log) |
198 | | recl 15002 |
. . . . . . . . . 10
β’ (π΄ β β β
(ββπ΄) β
β) |
199 | 198 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) β β) |
200 | | 0re 11164 |
. . . . . . . . 9
β’ 0 β
β |
201 | | lttri4 11246 |
. . . . . . . . 9
β’
(((ββπ΄)
β β β§ 0 β β) β ((ββπ΄) < 0 β¨ (ββπ΄) = 0 β¨ 0 <
(ββπ΄))) |
202 | 199, 200,
201 | sylancl 587 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((ββπ΄) < 0 β¨ (ββπ΄) = 0 β¨ 0 <
(ββπ΄))) |
203 | 131, 185,
197, 202 | mpjao3dan 1432 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))) β ran log) |
204 | | logef 25953 |
. . . . . . 7
β’
(((logβ(1 + (i Β· (tanβπ΄)))) β (logβ(1 β (i
Β· (tanβπ΄)))))
β ran log β (logβ(expβ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))))) = ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄)))))) |
205 | 203, 204 | syl 17 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ(expβ((logβ(1 + (i
Β· (tanβπ΄))))
β (logβ(1 β (i Β· (tanβπ΄))))))) = ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄)))))) |
206 | | 2cn 12235 |
. . . . . . . . 9
β’ 2 β
β |
207 | | mulcl 11142 |
. . . . . . . . 9
β’ ((2
β β β§ (i Β· π΄) β β) β (2 Β· (i
Β· π΄)) β
β) |
208 | 206, 76, 207 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (i Β· π΄)) β β) |
209 | | picn 25832 |
. . . . . . . . . . . 12
β’ Ο
β β |
210 | | 2ne0 12264 |
. . . . . . . . . . . 12
β’ 2 β
0 |
211 | | divneg 11854 |
. . . . . . . . . . . 12
β’ ((Ο
β β β§ 2 β β β§ 2 β 0) β -(Ο / 2) =
(-Ο / 2)) |
212 | 209, 206,
210, 211 | mp3an 1462 |
. . . . . . . . . . 11
β’ -(Ο /
2) = (-Ο / 2) |
213 | 212, 103 | eqbrtrrid 5146 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-Ο / 2) < (ββπ΄)) |
214 | | pire 25831 |
. . . . . . . . . . . . 13
β’ Ο
β β |
215 | 214 | renegcli 11469 |
. . . . . . . . . . . 12
β’ -Ο
β β |
216 | 215 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -Ο β β) |
217 | | 2re 12234 |
. . . . . . . . . . . 12
β’ 2 β
β |
218 | 217 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 2 β β) |
219 | | 2pos 12263 |
. . . . . . . . . . . 12
β’ 0 <
2 |
220 | 219 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < 2) |
221 | | ltdivmul 12037 |
. . . . . . . . . . 11
β’ ((-Ο
β β β§ (ββπ΄) β β β§ (2 β β
β§ 0 < 2)) β ((-Ο / 2) < (ββπ΄) β -Ο < (2 Β·
(ββπ΄)))) |
222 | 216, 199,
218, 220, 221 | syl112anc 1375 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((-Ο / 2) < (ββπ΄) β -Ο < (2 Β·
(ββπ΄)))) |
223 | 213, 222 | mpbid 231 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -Ο < (2 Β· (ββπ΄))) |
224 | | immul2 15029 |
. . . . . . . . . . 11
β’ ((2
β β β§ (i Β· π΄) β β) β (ββ(2
Β· (i Β· π΄))) =
(2 Β· (ββ(i Β· π΄)))) |
225 | 217, 76, 224 | sylancr 588 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(2 Β· (i Β· π΄))) = (2 Β·
(ββ(i Β· π΄)))) |
226 | 157 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (ββπ΄)) = (2 Β· (ββ(i Β·
π΄)))) |
227 | 225, 226 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(2 Β· (i Β· π΄))) = (2 Β·
(ββπ΄))) |
228 | 223, 227 | breqtrrd 5138 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -Ο < (ββ(2 Β· (i
Β· π΄)))) |
229 | | remulcl 11143 |
. . . . . . . . . . 11
β’ ((2
β β β§ (ββπ΄) β β) β (2 Β·
(ββπ΄)) β
β) |
230 | 217, 199,
229 | sylancr 588 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (ββπ΄)) β β) |
231 | 214 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β Ο β β) |
232 | | ltmuldiv2 12036 |
. . . . . . . . . . . 12
β’
(((ββπ΄)
β β β§ Ο β β β§ (2 β β β§ 0 <
2)) β ((2 Β· (ββπ΄)) < Ο β (ββπ΄) < (Ο /
2))) |
233 | 199, 231,
218, 220, 232 | syl112anc 1375 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((2 Β· (ββπ΄)) < Ο β (ββπ΄) < (Ο /
2))) |
234 | 189, 233 | mpbird 257 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (ββπ΄)) < Ο) |
235 | 230, 231,
234 | ltled 11310 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (ββπ΄)) β€ Ο) |
236 | 227, 235 | eqbrtrd 5132 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(2 Β· (i Β· π΄))) β€ Ο) |
237 | | ellogrn 25931 |
. . . . . . . 8
β’ ((2
Β· (i Β· π΄))
β ran log β ((2 Β· (i Β· π΄)) β β β§ -Ο <
(ββ(2 Β· (i Β· π΄))) β§ (ββ(2 Β· (i
Β· π΄))) β€
Ο)) |
238 | 208, 228,
236, 237 | syl3anbrc 1344 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (i Β· π΄)) β ran log) |
239 | | logef 25953 |
. . . . . . 7
β’ ((2
Β· (i Β· π΄))
β ran log β (logβ(expβ(2 Β· (i Β· π΄)))) = (2 Β· (i Β·
π΄))) |
240 | 238, 239 | syl 17 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ(expβ(2 Β· (i
Β· π΄)))) = (2
Β· (i Β· π΄))) |
241 | 93, 205, 240 | 3eqtr3d 2785 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))) = (2 Β· (i Β· π΄))) |
242 | 241 | negeqd 11402 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -((logβ(1 + (i Β·
(tanβπ΄)))) β
(logβ(1 β (i Β· (tanβπ΄))))) = -(2 Β· (i Β· π΄))) |
243 | 22, 242 | eqtr3d 2779 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((logβ(1 β (i Β·
(tanβπ΄)))) β
(logβ(1 + (i Β· (tanβπ΄))))) = -(2 Β· (i Β· π΄))) |
244 | 243 | oveq2d 7378 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i / 2) Β· ((logβ(1 β (i
Β· (tanβπ΄))))
β (logβ(1 + (i Β· (tanβπ΄)))))) = ((i / 2) Β· -(2 Β· (i
Β· π΄)))) |
245 | | halfcl 12385 |
. . . . 5
β’ (i β
β β (i / 2) β β) |
246 | 7, 245 | mp1i 13 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i / 2) β β) |
247 | 206 | a1i 11 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 2 β β) |
248 | 246, 247,
79 | mulassd 11185 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((i / 2) Β· 2) Β· -(i Β·
π΄)) = ((i / 2) Β· (2
Β· -(i Β· π΄)))) |
249 | 7, 206, 210 | divcan1i 11906 |
. . . . 5
β’ ((i / 2)
Β· 2) = i |
250 | 249 | oveq1i 7372 |
. . . 4
β’ (((i / 2)
Β· 2) Β· -(i Β· π΄)) = (i Β· -(i Β· π΄)) |
251 | 33, 33, 51 | mulassd 11185 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· i) Β· -π΄) = (i Β· (i Β· -π΄))) |
252 | 138 | oveq1i 7372 |
. . . . . 6
β’ ((i
Β· i) Β· -π΄) =
(-1 Β· -π΄) |
253 | | mul2neg 11601 |
. . . . . . . 8
β’ ((1
β β β§ π΄
β β) β (-1 Β· -π΄) = (1 Β· π΄)) |
254 | 6, 64, 253 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-1 Β· -π΄) = (1 Β· π΄)) |
255 | | mulid2 11161 |
. . . . . . . 8
β’ (π΄ β β β (1
Β· π΄) = π΄) |
256 | 255 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 Β· π΄) = π΄) |
257 | 254, 256 | eqtrd 2777 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-1 Β· -π΄) = π΄) |
258 | 252, 257 | eqtrid 2789 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· i) Β· -π΄) = π΄) |
259 | 66 | oveq2d 7378 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (i Β· -π΄)) = (i Β· -(i Β· π΄))) |
260 | 251, 258,
259 | 3eqtr3rd 2786 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· -(i Β· π΄)) = π΄) |
261 | 250, 260 | eqtrid 2789 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((i / 2) Β· 2) Β· -(i Β·
π΄)) = π΄) |
262 | | mulneg2 11599 |
. . . . 5
β’ ((2
β β β§ (i Β· π΄) β β) β (2 Β· -(i
Β· π΄)) = -(2 Β·
(i Β· π΄))) |
263 | 206, 76, 262 | sylancr 588 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· -(i Β· π΄)) = -(2 Β· (i Β· π΄))) |
264 | 263 | oveq2d 7378 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i / 2) Β· (2 Β· -(i Β·
π΄))) = ((i / 2) Β·
-(2 Β· (i Β· π΄)))) |
265 | 248, 261,
264 | 3eqtr3rd 2786 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i / 2) Β· -(2 Β· (i Β·
π΄))) = π΄) |
266 | 5, 244, 265 | 3eqtrd 2781 |
1
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (arctanβ(tanβπ΄)) = π΄) |