Step | Hyp | Ref
| Expression |
1 | | ax-icn 11117 |
. . . . . 6
β’ i β
β |
2 | | simpl 484 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β π΄ β β) |
3 | | mulcl 11142 |
. . . . . 6
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
4 | 1, 2, 3 | sylancr 588 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· π΄) β β) |
5 | 4 | recld 15086 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(i Β· π΄)) β β) |
6 | 5 | reefcld 15977 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(ββ(i Β· π΄))) β
β) |
7 | | simpr 486 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) β (-(Ο / 2)(,)(Ο /
2))) |
8 | | neghalfpirx 25839 |
. . . . . . 7
β’ -(Ο /
2) β β* |
9 | | halfpire 25837 |
. . . . . . . 8
β’ (Ο /
2) β β |
10 | 9 | rexri 11220 |
. . . . . . 7
β’ (Ο /
2) β β* |
11 | | elioo2 13312 |
. . . . . . 7
β’ ((-(Ο
/ 2) β β* β§ (Ο / 2) β β*)
β ((ββπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β ((ββπ΄) β β β§ -(Ο / 2) <
(ββπ΄) β§
(ββπ΄) < (Ο
/ 2)))) |
12 | 8, 10, 11 | mp2an 691 |
. . . . . 6
β’
((ββπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β ((ββπ΄) β β β§ -(Ο / 2) <
(ββπ΄) β§
(ββπ΄) < (Ο
/ 2))) |
13 | 7, 12 | sylib 217 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((ββπ΄) β β β§ -(Ο / 2) <
(ββπ΄) β§
(ββπ΄) < (Ο
/ 2))) |
14 | 13 | simp1d 1143 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββπ΄) β β) |
15 | 14 | recoscld 16033 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβ(ββπ΄)) β β) |
16 | | efgt0 15992 |
. . . 4
β’
((ββ(i Β· π΄)) β β β 0 <
(expβ(ββ(i Β· π΄)))) |
17 | 5, 16 | syl 17 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (expβ(ββ(i Β·
π΄)))) |
18 | | cosq14gt0 25883 |
. . . 4
β’
((ββπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β 0 < (cosβ(ββπ΄))) |
19 | 18 | adantl 483 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (cosβ(ββπ΄))) |
20 | 6, 15, 17, 19 | mulgt0d 11317 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < ((expβ(ββ(i Β·
π΄))) Β·
(cosβ(ββπ΄)))) |
21 | | efeul 16051 |
. . . . 5
β’ ((i
Β· π΄) β β
β (expβ(i Β· π΄)) = ((expβ(ββ(i Β·
π΄))) Β·
((cosβ(ββ(i Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄))))))) |
22 | 4, 21 | syl 17 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (expβ(i Β· π΄)) = ((expβ(ββ(i Β·
π΄))) Β·
((cosβ(ββ(i Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄))))))) |
23 | 22 | fveq2d 6851 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(expβ(i Β· π΄))) =
(ββ((expβ(ββ(i Β· π΄))) Β· ((cosβ(ββ(i
Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄)))))))) |
24 | 4 | imcld 15087 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(i Β· π΄)) β β) |
25 | 24 | recoscld 16033 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβ(ββ(i Β· π΄))) β
β) |
26 | 25 | recnd 11190 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβ(ββ(i Β· π΄))) β
β) |
27 | 24 | resincld 16032 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (sinβ(ββ(i Β· π΄))) β
β) |
28 | 27 | recnd 11190 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (sinβ(ββ(i Β· π΄))) β
β) |
29 | | mulcl 11142 |
. . . . . 6
β’ ((i
β β β§ (sinβ(ββ(i Β· π΄))) β β) β (i Β·
(sinβ(ββ(i Β· π΄)))) β β) |
30 | 1, 28, 29 | sylancr 588 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (i Β· (sinβ(ββ(i
Β· π΄)))) β
β) |
31 | 26, 30 | addcld 11181 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((cosβ(ββ(i Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄))))) β β) |
32 | 6, 31 | remul2d 15119 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ((expβ(ββ(i
Β· π΄))) Β·
((cosβ(ββ(i Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄))))))) = ((expβ(ββ(i
Β· π΄))) Β·
(ββ((cosβ(ββ(i Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄)))))))) |
33 | 25, 27 | crred 15123 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ((cosβ(ββ(i
Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄)))))) = (cosβ(ββ(i
Β· π΄)))) |
34 | | imre 15000 |
. . . . . . . 8
β’ ((i
Β· π΄) β β
β (ββ(i Β· π΄)) = (ββ(-i Β· (i Β·
π΄)))) |
35 | 4, 34 | syl 17 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(i Β· π΄)) = (ββ(-i Β· (i Β·
π΄)))) |
36 | 1, 1 | mulneg1i 11608 |
. . . . . . . . . . 11
β’ (-i
Β· i) = -(i Β· i) |
37 | | ixi 11791 |
. . . . . . . . . . . 12
β’ (i
Β· i) = -1 |
38 | 37 | negeqi 11401 |
. . . . . . . . . . 11
β’ -(i
Β· i) = --1 |
39 | | negneg1e1 12278 |
. . . . . . . . . . 11
β’ --1 =
1 |
40 | 36, 38, 39 | 3eqtri 2769 |
. . . . . . . . . 10
β’ (-i
Β· i) = 1 |
41 | 40 | oveq1i 7372 |
. . . . . . . . 9
β’ ((-i
Β· i) Β· π΄) =
(1 Β· π΄) |
42 | | negicn 11409 |
. . . . . . . . . . 11
β’ -i β
β |
43 | 42 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β -i β β) |
44 | 1 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β i β β) |
45 | 43, 44, 2 | mulassd 11185 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((-i Β· i) Β· π΄) = (-i Β· (i Β· π΄))) |
46 | | mulid2 11161 |
. . . . . . . . . 10
β’ (π΄ β β β (1
Β· π΄) = π΄) |
47 | 46 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (1 Β· π΄) = π΄) |
48 | 41, 45, 47 | 3eqtr3a 2801 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (-i Β· (i Β· π΄)) = π΄) |
49 | 48 | fveq2d 6851 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(-i Β· (i Β· π΄))) = (ββπ΄)) |
50 | 35, 49 | eqtrd 2777 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(i Β· π΄)) = (ββπ΄)) |
51 | 50 | fveq2d 6851 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβ(ββ(i Β· π΄))) =
(cosβ(ββπ΄))) |
52 | 33, 51 | eqtrd 2777 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ((cosβ(ββ(i
Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄)))))) = (cosβ(ββπ΄))) |
53 | 52 | oveq2d 7378 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((expβ(ββ(i Β· π΄))) Β·
(ββ((cosβ(ββ(i Β· π΄))) + (i Β·
(sinβ(ββ(i Β· π΄))))))) = ((expβ(ββ(i
Β· π΄))) Β·
(cosβ(ββπ΄)))) |
54 | 23, 32, 53 | 3eqtrd 2781 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (ββ(expβ(i Β· π΄))) =
((expβ(ββ(i Β· π΄))) Β· (cosβ(ββπ΄)))) |
55 | 20, 54 | breqtrrd 5138 |
1
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β 0 < (ββ(expβ(i Β·
π΄)))) |