Step | Hyp | Ref
| Expression |
1 | | sincl 16015 |
. . . 4
β’ (π΄ β β β
(sinβπ΄) β
β) |
2 | 1 | adantr 482 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (sinβπ΄) β β) |
3 | | asinval 26248 |
. . 3
β’
((sinβπ΄)
β β β (arcsinβ(sinβπ΄)) = (-i Β· (logβ((i Β·
(sinβπ΄)) +
(ββ(1 β ((sinβπ΄)β2))))))) |
4 | 2, 3 | syl 17 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (arcsinβ(sinβπ΄)) = (-i Β· (logβ((i Β·
(sinβπ΄)) +
(ββ(1 β ((sinβπ΄)β2))))))) |
5 | | ax-icn 11117 |
. . . . . . . 8
β’ i β
β |
6 | | mulcl 11142 |
. . . . . . . 8
β’ ((i
β β β§ (sinβπ΄) β β) β (i Β·
(sinβπ΄)) β
β) |
7 | 5, 2, 6 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (sinβπ΄)) β β) |
8 | | simpl 484 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β π΄ β β) |
9 | | mulcl 11142 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
10 | 5, 8, 9 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· π΄) β β) |
11 | | efcl 15972 |
. . . . . . . 8
β’ ((i
Β· π΄) β β
β (expβ(i Β· π΄)) β β) |
12 | 10, 11 | syl 17 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· π΄)) β β) |
13 | 7, 12 | pncan3d 11522 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· (sinβπ΄)) + ((expβ(i Β· π΄)) β (i Β·
(sinβπ΄)))) =
(expβ(i Β· π΄))) |
14 | 12, 7 | subcld 11519 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) β (i Β· (sinβπ΄))) β
β) |
15 | | ax-1cn 11116 |
. . . . . . . . 9
β’ 1 β
β |
16 | 2 | sqcld 14056 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((sinβπ΄)β2) β β) |
17 | | subcl 11407 |
. . . . . . . . 9
β’ ((1
β β β§ ((sinβπ΄)β2) β β) β (1 β
((sinβπ΄)β2))
β β) |
18 | 15, 16, 17 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 β ((sinβπ΄)β2)) β β) |
19 | | binom2sub 14130 |
. . . . . . . . . 10
β’
(((expβ(i Β· π΄)) β β β§ (i Β·
(sinβπ΄)) β
β) β (((expβ(i Β· π΄)) β (i Β· (sinβπ΄)))β2) = ((((expβ(i
Β· π΄))β2)
β (2 Β· ((expβ(i Β· π΄)) Β· (i Β· (sinβπ΄))))) + ((i Β·
(sinβπ΄))β2))) |
20 | 12, 7, 19 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄)) β (i Β· (sinβπ΄)))β2) = ((((expβ(i
Β· π΄))β2)
β (2 Β· ((expβ(i Β· π΄)) Β· (i Β· (sinβπ΄))))) + ((i Β·
(sinβπ΄))β2))) |
21 | 12 | sqvald 14055 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄))β2) = ((expβ(i Β· π΄)) Β· (expβ(i
Β· π΄)))) |
22 | | 2cn 12235 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
23 | 22 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 2 β β) |
24 | 23, 12, 7 | mul12d 11371 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· ((expβ(i Β· π΄)) Β· (i Β·
(sinβπ΄)))) =
((expβ(i Β· π΄))
Β· (2 Β· (i Β· (sinβπ΄))))) |
25 | 21, 24 | oveq12d 7380 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄))β2) β (2 Β·
((expβ(i Β· π΄))
Β· (i Β· (sinβπ΄))))) = (((expβ(i Β· π΄)) Β· (expβ(i
Β· π΄))) β
((expβ(i Β· π΄))
Β· (2 Β· (i Β· (sinβπ΄)))))) |
26 | | coscl 16016 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
(cosβπ΄) β
β) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) β β) |
28 | | subsq 14121 |
. . . . . . . . . . . . 13
β’
(((cosβπ΄)
β β β§ (i Β· (sinβπ΄)) β β) β (((cosβπ΄)β2) β ((i Β·
(sinβπ΄))β2)) =
(((cosβπ΄) + (i
Β· (sinβπ΄)))
Β· ((cosβπ΄)
β (i Β· (sinβπ΄))))) |
29 | 27, 7, 28 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄)β2) β ((i Β·
(sinβπ΄))β2)) =
(((cosβπ΄) + (i
Β· (sinβπ΄)))
Β· ((cosβπ΄)
β (i Β· (sinβπ΄))))) |
30 | | sqmul 14031 |
. . . . . . . . . . . . . . . 16
β’ ((i
β β β§ (sinβπ΄) β β) β ((i Β·
(sinβπ΄))β2) =
((iβ2) Β· ((sinβπ΄)β2))) |
31 | 5, 2, 30 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· (sinβπ΄))β2) = ((iβ2) Β·
((sinβπ΄)β2))) |
32 | | i2 14113 |
. . . . . . . . . . . . . . . . 17
β’
(iβ2) = -1 |
33 | 32 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’
((iβ2) Β· ((sinβπ΄)β2)) = (-1 Β· ((sinβπ΄)β2)) |
34 | 16 | mulm1d 11614 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-1 Β· ((sinβπ΄)β2)) = -((sinβπ΄)β2)) |
35 | 33, 34 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((iβ2) Β· ((sinβπ΄)β2)) = -((sinβπ΄)β2)) |
36 | 31, 35 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· (sinβπ΄))β2) = -((sinβπ΄)β2)) |
37 | 36 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄)β2) β ((i Β·
(sinβπ΄))β2)) =
(((cosβπ΄)β2)
β -((sinβπ΄)β2))) |
38 | 27 | sqcld 14056 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((cosβπ΄)β2) β β) |
39 | 38, 16 | subnegd 11526 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄)β2) β -((sinβπ΄)β2)) = (((cosβπ΄)β2) + ((sinβπ΄)β2))) |
40 | 38, 16 | addcomd 11364 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄)β2) + ((sinβπ΄)β2)) = (((sinβπ΄)β2) + ((cosβπ΄)β2))) |
41 | 37, 39, 40 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄)β2) β ((i Β·
(sinβπ΄))β2)) =
(((sinβπ΄)β2) +
((cosβπ΄)β2))) |
42 | | efival 16041 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(expβ(i Β· π΄))
= ((cosβπ΄) + (i
Β· (sinβπ΄)))) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· π΄)) = ((cosβπ΄) + (i Β· (sinβπ΄)))) |
44 | 7 | 2timesd 12403 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (i Β· (sinβπ΄))) = ((i Β·
(sinβπ΄)) + (i
Β· (sinβπ΄)))) |
45 | 43, 44 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) β (2 Β· (i Β·
(sinβπ΄)))) =
(((cosβπ΄) + (i
Β· (sinβπ΄)))
β ((i Β· (sinβπ΄)) + (i Β· (sinβπ΄))))) |
46 | 27, 7, 7 | pnpcan2d 11557 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) + (i Β· (sinβπ΄))) β ((i Β· (sinβπ΄)) + (i Β·
(sinβπ΄)))) =
((cosβπ΄) β (i
Β· (sinβπ΄)))) |
47 | 45, 46 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) β (2 Β· (i Β·
(sinβπ΄)))) =
((cosβπ΄) β (i
Β· (sinβπ΄)))) |
48 | 43, 47 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) Β· ((expβ(i Β· π΄)) β (2 Β· (i
Β· (sinβπ΄)))))
= (((cosβπ΄) + (i
Β· (sinβπ΄)))
Β· ((cosβπ΄)
β (i Β· (sinβπ΄))))) |
49 | | mulcl 11142 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ (i Β· (sinβπ΄)) β β) β (2 Β· (i
Β· (sinβπ΄)))
β β) |
50 | 22, 7, 49 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (2 Β· (i Β· (sinβπ΄))) β
β) |
51 | 12, 12, 50 | subdid 11618 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) Β· ((expβ(i Β· π΄)) β (2 Β· (i
Β· (sinβπ΄)))))
= (((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) β ((expβ(i
Β· π΄)) Β· (2
Β· (i Β· (sinβπ΄)))))) |
52 | 48, 51 | eqtr3d 2779 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((cosβπ΄) + (i Β· (sinβπ΄))) Β· ((cosβπ΄) β (i Β· (sinβπ΄)))) = (((expβ(i Β·
π΄)) Β· (expβ(i
Β· π΄))) β
((expβ(i Β· π΄))
Β· (2 Β· (i Β· (sinβπ΄)))))) |
53 | 29, 41, 52 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((sinβπ΄)β2) + ((cosβπ΄)β2)) = (((expβ(i Β· π΄)) Β· (expβ(i
Β· π΄))) β
((expβ(i Β· π΄))
Β· (2 Β· (i Β· (sinβπ΄)))))) |
54 | | sincossq 16065 |
. . . . . . . . . . . 12
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
55 | 54 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((sinβπ΄)β2) + ((cosβπ΄)β2)) = 1) |
56 | 25, 53, 55 | 3eqtr2d 2783 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄))β2) β (2 Β·
((expβ(i Β· π΄))
Β· (i Β· (sinβπ΄))))) = 1) |
57 | 56, 36 | oveq12d 7380 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((((expβ(i Β· π΄))β2) β (2 Β·
((expβ(i Β· π΄))
Β· (i Β· (sinβπ΄))))) + ((i Β· (sinβπ΄))β2)) = (1 +
-((sinβπ΄)β2))) |
58 | | negsub 11456 |
. . . . . . . . . 10
β’ ((1
β β β§ ((sinβπ΄)β2) β β) β (1 +
-((sinβπ΄)β2)) =
(1 β ((sinβπ΄)β2))) |
59 | 15, 16, 58 | sylancr 588 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 + -((sinβπ΄)β2)) = (1 β ((sinβπ΄)β2))) |
60 | 20, 57, 59 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄)) β (i Β· (sinβπ΄)))β2) = (1 β
((sinβπ΄)β2))) |
61 | | halfre 12374 |
. . . . . . . . . . . 12
β’ (1 / 2)
β β |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 / 2) β β) |
63 | | negicn 11409 |
. . . . . . . . . . . . . . 15
β’ -i β
β |
64 | | mulcl 11142 |
. . . . . . . . . . . . . . 15
β’ ((-i
β β β§ π΄
β β) β (-i Β· π΄) β β) |
65 | 63, 8, 64 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-i Β· π΄) β β) |
66 | | efcl 15972 |
. . . . . . . . . . . . . 14
β’ ((-i
Β· π΄) β β
β (expβ(-i Β· π΄)) β β) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(-i Β· π΄)) β β) |
68 | 12, 67 | addcld 11181 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) β
β) |
69 | 68 | recld 15086 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ((expβ(i Β· π΄)) + (expβ(-i Β·
π΄)))) β
β) |
70 | | halfgt0 12376 |
. . . . . . . . . . . 12
β’ 0 < (1
/ 2) |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (1 / 2)) |
72 | 12 | recld 15086 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(expβ(i Β· π΄))) β
β) |
73 | 67 | recld 15086 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(expβ(-i Β· π΄))) β
β) |
74 | | asinsinlem 26257 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ(expβ(i Β·
π΄)))) |
75 | | negcl 11408 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β -π΄ β
β) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -π΄ β β) |
77 | | reneg 15017 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(ββ-π΄) =
-(ββπ΄)) |
78 | 77 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ-π΄) = -(ββπ΄)) |
79 | | halfpire 25837 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Ο /
2) β β |
80 | 79 | renegcli 11469 |
. . . . . . . . . . . . . . . . . . 19
β’ -(Ο /
2) β β |
81 | | recl 15002 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β
(ββπ΄) β
β) |
82 | | iooneg 13395 |
. . . . . . . . . . . . . . . . . . 19
β’ ((-(Ο
/ 2) β β β§ (Ο / 2) β β β§ (ββπ΄) β β) β
((ββπ΄) β
(-(Ο / 2)(,)(Ο / 2)) β -(ββπ΄) β (-(Ο / 2)(,)--(Ο /
2)))) |
83 | 80, 79, 81, 82 | mp3an12i 1466 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β
((ββπ΄) β
(-(Ο / 2)(,)(Ο / 2)) β -(ββπ΄) β (-(Ο / 2)(,)--(Ο /
2)))) |
84 | 83 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -(ββπ΄) β (-(Ο / 2)(,)--(Ο /
2))) |
85 | 79 | recni 11176 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ο /
2) β β |
86 | 85 | negnegi 11478 |
. . . . . . . . . . . . . . . . . 18
β’ --(Ο /
2) = (Ο / 2) |
87 | 86 | oveq2i 7373 |
. . . . . . . . . . . . . . . . 17
β’ (-(Ο /
2)(,)--(Ο / 2)) = (-(Ο / 2)(,)(Ο / 2)) |
88 | 84, 87 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -(ββπ΄) β (-(Ο / 2)(,)(Ο /
2))) |
89 | 78, 88 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ-π΄) β (-(Ο / 2)(,)(Ο /
2))) |
90 | | asinsinlem 26257 |
. . . . . . . . . . . . . . 15
β’ ((-π΄ β β β§
(ββ-π΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ(expβ(i Β·
-π΄)))) |
91 | 76, 89, 90 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ(expβ(i Β·
-π΄)))) |
92 | | mulneg12 11600 |
. . . . . . . . . . . . . . . . 17
β’ ((i
β β β§ π΄
β β) β (-i Β· π΄) = (i Β· -π΄)) |
93 | 5, 8, 92 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-i Β· π΄) = (i Β· -π΄)) |
94 | 93 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(-i Β· π΄)) = (expβ(i Β· -π΄))) |
95 | 94 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(expβ(-i Β· π΄))) =
(ββ(expβ(i Β· -π΄)))) |
96 | 91, 95 | breqtrrd 5138 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ(expβ(-i Β·
π΄)))) |
97 | 72, 73, 74, 96 | addgt0d 11737 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < ((ββ(expβ(i Β·
π΄))) +
(ββ(expβ(-i Β· π΄))))) |
98 | 12, 67 | readdd 15106 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ((expβ(i Β· π΄)) + (expβ(-i Β·
π΄)))) =
((ββ(expβ(i Β· π΄))) + (ββ(expβ(-i Β·
π΄))))) |
99 | 97, 98 | breqtrrd 5138 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ((expβ(i Β·
π΄)) + (expβ(-i
Β· π΄))))) |
100 | 62, 69, 71, 99 | mulgt0d 11317 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < ((1 / 2) Β·
(ββ((expβ(i Β· π΄)) + (expβ(-i Β· π΄)))))) |
101 | | cosval 16012 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
(cosβπ΄) =
(((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) / 2)) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) = (((expβ(i Β· π΄)) + (expβ(-i Β·
π΄))) / 2)) |
103 | | 2ne0 12264 |
. . . . . . . . . . . . . . 15
β’ 2 β
0 |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 2 β 0) |
105 | 68, 23, 104 | divrec2d 11942 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) / 2) = ((1 / 2) Β·
((expβ(i Β· π΄))
+ (expβ(-i Β· π΄))))) |
106 | 102, 105 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) = ((1 / 2) Β· ((expβ(i
Β· π΄)) +
(expβ(-i Β· π΄))))) |
107 | 106 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(cosβπ΄)) = (ββ((1 / 2) Β·
((expβ(i Β· π΄))
+ (expβ(-i Β· π΄)))))) |
108 | | remul2 15022 |
. . . . . . . . . . . 12
β’ (((1 / 2)
β β β§ ((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) β β) β
(ββ((1 / 2) Β· ((expβ(i Β· π΄)) + (expβ(-i Β· π΄))))) = ((1 / 2) Β·
(ββ((expβ(i Β· π΄)) + (expβ(-i Β· π΄)))))) |
109 | 61, 68, 108 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ((1 / 2) Β·
((expβ(i Β· π΄))
+ (expβ(-i Β· π΄))))) = ((1 / 2) Β·
(ββ((expβ(i Β· π΄)) + (expβ(-i Β· π΄)))))) |
110 | 107, 109 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(cosβπ΄)) = ((1 / 2) Β·
(ββ((expβ(i Β· π΄)) + (expβ(-i Β· π΄)))))) |
111 | 100, 110 | breqtrrd 5138 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ(cosβπ΄))) |
112 | 27, 7, 43 | mvrraddd 11574 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) β (i Β· (sinβπ΄))) = (cosβπ΄)) |
113 | 112 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ((expβ(i Β· π΄)) β (i Β·
(sinβπ΄)))) =
(ββ(cosβπ΄))) |
114 | 111, 113 | breqtrrd 5138 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ((expβ(i Β·
π΄)) β (i Β·
(sinβπ΄))))) |
115 | 14, 18, 60, 114 | eqsqrt2d 15260 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(i Β· π΄)) β (i Β· (sinβπ΄))) = (ββ(1 β
((sinβπ΄)β2)))) |
116 | 115 | oveq2d 7378 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((i Β· (sinβπ΄)) + ((expβ(i Β· π΄)) β (i Β·
(sinβπ΄)))) = ((i
Β· (sinβπ΄)) +
(ββ(1 β ((sinβπ΄)β2))))) |
117 | 13, 116 | eqtr3d 2779 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· π΄)) = ((i Β· (sinβπ΄)) + (ββ(1 β
((sinβπ΄)β2))))) |
118 | 117 | fveq2d 6851 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ(expβ(i Β· π΄))) = (logβ((i Β·
(sinβπ΄)) +
(ββ(1 β ((sinβπ΄)β2)))))) |
119 | | pire 25831 |
. . . . . . . . . 10
β’ Ο
β β |
120 | 119 | renegcli 11469 |
. . . . . . . . 9
β’ -Ο
β β |
121 | 120 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -Ο β β) |
122 | 80 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -(Ο / 2) β β) |
123 | | elioore 13301 |
. . . . . . . . 9
β’
((ββπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β (ββπ΄) β β) |
124 | 123 | adantl 483 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) β β) |
125 | | pirp 25834 |
. . . . . . . . . . 11
β’ Ο
β β+ |
126 | | rphalflt 12951 |
. . . . . . . . . . 11
β’ (Ο
β β+ β (Ο / 2) < Ο) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . 10
β’ (Ο /
2) < Ο |
128 | 79, 119 | ltnegi 11706 |
. . . . . . . . . 10
β’ ((Ο /
2) < Ο β -Ο < -(Ο / 2)) |
129 | 127, 128 | mpbi 229 |
. . . . . . . . 9
β’ -Ο
< -(Ο / 2) |
130 | 129 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -Ο < -(Ο / 2)) |
131 | | eliooord 13330 |
. . . . . . . . . 10
β’
((ββπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β (-(Ο / 2) < (ββπ΄) β§ (ββπ΄) < (Ο /
2))) |
132 | 131 | adantl 483 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-(Ο / 2) < (ββπ΄) β§ (ββπ΄) < (Ο /
2))) |
133 | 132 | simpld 496 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -(Ο / 2) < (ββπ΄)) |
134 | 121, 122,
124, 130, 133 | lttrd 11323 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -Ο < (ββπ΄)) |
135 | | imre 15000 |
. . . . . . . . 9
β’ ((i
Β· π΄) β β
β (ββ(i Β· π΄)) = (ββ(-i Β· (i Β·
π΄)))) |
136 | 10, 135 | syl 17 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(i Β· π΄)) = (ββ(-i Β· (i Β·
π΄)))) |
137 | 5, 5 | mulneg1i 11608 |
. . . . . . . . . . . 12
β’ (-i
Β· i) = -(i Β· i) |
138 | | ixi 11791 |
. . . . . . . . . . . . 13
β’ (i
Β· i) = -1 |
139 | 138 | negeqi 11401 |
. . . . . . . . . . . 12
β’ -(i
Β· i) = --1 |
140 | 15 | negnegi 11478 |
. . . . . . . . . . . 12
β’ --1 =
1 |
141 | 137, 139,
140 | 3eqtri 2769 |
. . . . . . . . . . 11
β’ (-i
Β· i) = 1 |
142 | 141 | oveq1i 7372 |
. . . . . . . . . 10
β’ ((-i
Β· i) Β· π΄) =
(1 Β· π΄) |
143 | 63 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -i β β) |
144 | 5 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β i β β) |
145 | 143, 144,
8 | mulassd 11185 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((-i Β· i) Β· π΄) = (-i Β· (i Β· π΄))) |
146 | | mulid2 11161 |
. . . . . . . . . . 11
β’ (π΄ β β β (1
Β· π΄) = π΄) |
147 | 146 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 Β· π΄) = π΄) |
148 | 142, 145,
147 | 3eqtr3a 2801 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-i Β· (i Β· π΄)) = π΄) |
149 | 148 | fveq2d 6851 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(-i Β· (i Β· π΄))) = (ββπ΄)) |
150 | 136, 149 | eqtrd 2777 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(i Β· π΄)) = (ββπ΄)) |
151 | 134, 150 | breqtrrd 5138 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -Ο < (ββ(i Β· π΄))) |
152 | 119 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β Ο β β) |
153 | 79 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (Ο / 2) β β) |
154 | 132 | simprd 497 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) < (Ο / 2)) |
155 | 127 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (Ο / 2) < Ο) |
156 | 124, 153,
152, 154, 155 | lttrd 11323 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) < Ο) |
157 | 124, 152,
156 | ltled 11310 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) β€ Ο) |
158 | 150, 157 | eqbrtrd 5132 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(i Β· π΄)) β€ Ο) |
159 | | ellogrn 25931 |
. . . . . 6
β’ ((i
Β· π΄) β ran log
β ((i Β· π΄)
β β β§ -Ο < (ββ(i Β· π΄)) β§ (ββ(i Β· π΄)) β€ Ο)) |
160 | 10, 151, 158, 159 | syl3anbrc 1344 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· π΄) β ran log) |
161 | | logef 25953 |
. . . . 5
β’ ((i
Β· π΄) β ran log
β (logβ(expβ(i Β· π΄))) = (i Β· π΄)) |
162 | 160, 161 | syl 17 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ(expβ(i Β· π΄))) = (i Β· π΄)) |
163 | 118, 162 | eqtr3d 2779 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (logβ((i Β· (sinβπ΄)) + (ββ(1 β
((sinβπ΄)β2)))))
= (i Β· π΄)) |
164 | 163 | oveq2d 7378 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-i Β· (logβ((i Β·
(sinβπ΄)) +
(ββ(1 β ((sinβπ΄)β2)))))) = (-i Β· (i Β·
π΄))) |
165 | 4, 164, 148 | 3eqtrd 2781 |
1
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (arcsinβ(sinβπ΄)) = π΄) |