Step | Hyp | Ref
| Expression |
1 | | halfcl 12383 |
. . . 4
β’ (π΄ β β β (π΄ / 2) β
β) |
2 | | ax-icn 11115 |
. . . . 5
β’ i β
β |
3 | | ine0 11595 |
. . . . 5
β’ i β
0 |
4 | | divcl 11824 |
. . . . 5
β’ (((π΄ / 2) β β β§ i
β β β§ i β 0) β ((π΄ / 2) / i) β β) |
5 | 2, 3, 4 | mp3an23 1454 |
. . . 4
β’ ((π΄ / 2) β β β
((π΄ / 2) / i) β
β) |
6 | 1, 5 | syl 17 |
. . 3
β’ (π΄ β β β ((π΄ / 2) / i) β
β) |
7 | | sineq0 25896 |
. . 3
β’ (((π΄ / 2) / i) β β β
((sinβ((π΄ / 2) / i))
= 0 β (((π΄ / 2) / i) /
Ο) β β€)) |
8 | 6, 7 | syl 17 |
. 2
β’ (π΄ β β β
((sinβ((π΄ / 2) / i))
= 0 β (((π΄ / 2) / i) /
Ο) β β€)) |
9 | | sinval 16009 |
. . . . . 6
β’ (((π΄ / 2) / i) β β β
(sinβ((π΄ / 2) / i)) =
(((expβ(i Β· ((π΄ / 2) / i))) β (expβ(-i Β·
((π΄ / 2) / i)))) / (2
Β· i))) |
10 | 6, 9 | syl 17 |
. . . . 5
β’ (π΄ β β β
(sinβ((π΄ / 2) / i)) =
(((expβ(i Β· ((π΄ / 2) / i))) β (expβ(-i Β·
((π΄ / 2) / i)))) / (2
Β· i))) |
11 | | divcan2 11826 |
. . . . . . . . . 10
β’ (((π΄ / 2) β β β§ i
β β β§ i β 0) β (i Β· ((π΄ / 2) / i)) = (π΄ / 2)) |
12 | 2, 3, 11 | mp3an23 1454 |
. . . . . . . . 9
β’ ((π΄ / 2) β β β (i
Β· ((π΄ / 2) / i)) =
(π΄ / 2)) |
13 | 1, 12 | syl 17 |
. . . . . . . 8
β’ (π΄ β β β (i
Β· ((π΄ / 2) / i)) =
(π΄ / 2)) |
14 | 13 | fveq2d 6847 |
. . . . . . 7
β’ (π΄ β β β
(expβ(i Β· ((π΄
/ 2) / i))) = (expβ(π΄
/ 2))) |
15 | | mulneg1 11596 |
. . . . . . . . . 10
β’ ((i
β β β§ ((π΄ /
2) / i) β β) β (-i Β· ((π΄ / 2) / i)) = -(i Β· ((π΄ / 2) / i))) |
16 | 2, 6, 15 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β β β (-i
Β· ((π΄ / 2) / i)) =
-(i Β· ((π΄ / 2) /
i))) |
17 | 13 | negeqd 11400 |
. . . . . . . . 9
β’ (π΄ β β β -(i
Β· ((π΄ / 2) / i)) =
-(π΄ / 2)) |
18 | 16, 17 | eqtrd 2773 |
. . . . . . . 8
β’ (π΄ β β β (-i
Β· ((π΄ / 2) / i)) =
-(π΄ / 2)) |
19 | 18 | fveq2d 6847 |
. . . . . . 7
β’ (π΄ β β β
(expβ(-i Β· ((π΄
/ 2) / i))) = (expβ-(π΄ / 2))) |
20 | 14, 19 | oveq12d 7376 |
. . . . . 6
β’ (π΄ β β β
((expβ(i Β· ((π΄
/ 2) / i))) β (expβ(-i Β· ((π΄ / 2) / i)))) = ((expβ(π΄ / 2)) β
(expβ-(π΄ /
2)))) |
21 | 20 | oveq1d 7373 |
. . . . 5
β’ (π΄ β β β
(((expβ(i Β· ((π΄ / 2) / i))) β (expβ(-i Β·
((π΄ / 2) / i)))) / (2
Β· i)) = (((expβ(π΄ / 2)) β (expβ-(π΄ / 2))) / (2 Β·
i))) |
22 | 10, 21 | eqtrd 2773 |
. . . 4
β’ (π΄ β β β
(sinβ((π΄ / 2) / i)) =
(((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) / (2 Β· i))) |
23 | 22 | eqeq1d 2735 |
. . 3
β’ (π΄ β β β
((sinβ((π΄ / 2) / i))
= 0 β (((expβ(π΄
/ 2)) β (expβ-(π΄ / 2))) / (2 Β· i)) =
0)) |
24 | | efcl 15970 |
. . . . . 6
β’ ((π΄ / 2) β β β
(expβ(π΄ / 2)) β
β) |
25 | 1, 24 | syl 17 |
. . . . 5
β’ (π΄ β β β
(expβ(π΄ / 2)) β
β) |
26 | 1 | negcld 11504 |
. . . . . 6
β’ (π΄ β β β -(π΄ / 2) β
β) |
27 | | efcl 15970 |
. . . . . 6
β’ (-(π΄ / 2) β β β
(expβ-(π΄ / 2)) β
β) |
28 | 26, 27 | syl 17 |
. . . . 5
β’ (π΄ β β β
(expβ-(π΄ / 2)) β
β) |
29 | 25, 28 | subcld 11517 |
. . . 4
β’ (π΄ β β β
((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) β β) |
30 | | 2cn 12233 |
. . . . . 6
β’ 2 β
β |
31 | 30, 2 | mulcli 11167 |
. . . . 5
β’ (2
Β· i) β β |
32 | | 2ne0 12262 |
. . . . . 6
β’ 2 β
0 |
33 | 30, 2, 32, 3 | mulne0i 11803 |
. . . . 5
β’ (2
Β· i) β 0 |
34 | | diveq0 11828 |
. . . . 5
β’
((((expβ(π΄ /
2)) β (expβ-(π΄
/ 2))) β β β§ (2 Β· i) β β β§ (2 Β· i)
β 0) β ((((expβ(π΄ / 2)) β (expβ-(π΄ / 2))) / (2 Β· i)) = 0
β ((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) = 0)) |
35 | 31, 33, 34 | mp3an23 1454 |
. . . 4
β’
(((expβ(π΄ /
2)) β (expβ-(π΄
/ 2))) β β β ((((expβ(π΄ / 2)) β (expβ-(π΄ / 2))) / (2 Β· i)) = 0
β ((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) = 0)) |
36 | 29, 35 | syl 17 |
. . 3
β’ (π΄ β β β
((((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) / (2 Β· i)) = 0 β ((expβ(π΄ / 2)) β (expβ-(π΄ / 2))) = 0)) |
37 | | efne0 15984 |
. . . . . . . 8
β’ (-(π΄ / 2) β β β
(expβ-(π΄ / 2)) β
0) |
38 | 26, 37 | syl 17 |
. . . . . . 7
β’ (π΄ β β β
(expβ-(π΄ / 2)) β
0) |
39 | 25, 28, 28, 38 | divsubdird 11975 |
. . . . . 6
β’ (π΄ β β β
(((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) / (expβ-(π΄ /
2))) = (((expβ(π΄ /
2)) / (expβ-(π΄ / 2)))
β ((expβ-(π΄ /
2)) / (expβ-(π΄ /
2))))) |
40 | | efsub 15987 |
. . . . . . . . 9
β’ (((π΄ / 2) β β β§
-(π΄ / 2) β β)
β (expβ((π΄ / 2)
β -(π΄ / 2))) =
((expβ(π΄ / 2)) /
(expβ-(π΄ /
2)))) |
41 | 1, 26, 40 | syl2anc 585 |
. . . . . . . 8
β’ (π΄ β β β
(expβ((π΄ / 2) β
-(π΄ / 2))) =
((expβ(π΄ / 2)) /
(expβ-(π΄ /
2)))) |
42 | 1, 1 | subnegd 11524 |
. . . . . . . . . 10
β’ (π΄ β β β ((π΄ / 2) β -(π΄ / 2)) = ((π΄ / 2) + (π΄ / 2))) |
43 | | 2halves 12386 |
. . . . . . . . . 10
β’ (π΄ β β β ((π΄ / 2) + (π΄ / 2)) = π΄) |
44 | 42, 43 | eqtrd 2773 |
. . . . . . . . 9
β’ (π΄ β β β ((π΄ / 2) β -(π΄ / 2)) = π΄) |
45 | 44 | fveq2d 6847 |
. . . . . . . 8
β’ (π΄ β β β
(expβ((π΄ / 2) β
-(π΄ / 2))) =
(expβπ΄)) |
46 | 41, 45 | eqtr3d 2775 |
. . . . . . 7
β’ (π΄ β β β
((expβ(π΄ / 2)) /
(expβ-(π΄ / 2))) =
(expβπ΄)) |
47 | 28, 38 | dividd 11934 |
. . . . . . 7
β’ (π΄ β β β
((expβ-(π΄ / 2)) /
(expβ-(π΄ / 2))) =
1) |
48 | 46, 47 | oveq12d 7376 |
. . . . . 6
β’ (π΄ β β β
(((expβ(π΄ / 2)) /
(expβ-(π΄ / 2)))
β ((expβ-(π΄ /
2)) / (expβ-(π΄ /
2)))) = ((expβπ΄)
β 1)) |
49 | 39, 48 | eqtrd 2773 |
. . . . 5
β’ (π΄ β β β
(((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) / (expβ-(π΄ /
2))) = ((expβπ΄)
β 1)) |
50 | 49 | eqeq1d 2735 |
. . . 4
β’ (π΄ β β β
((((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) / (expβ-(π΄ /
2))) = 0 β ((expβπ΄) β 1) = 0)) |
51 | 29, 28, 38 | diveq0ad 11946 |
. . . 4
β’ (π΄ β β β
((((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) / (expβ-(π΄ /
2))) = 0 β ((expβ(π΄ / 2)) β (expβ-(π΄ / 2))) = 0)) |
52 | | efcl 15970 |
. . . . 5
β’ (π΄ β β β
(expβπ΄) β
β) |
53 | | ax-1cn 11114 |
. . . . 5
β’ 1 β
β |
54 | | subeq0 11432 |
. . . . 5
β’
(((expβπ΄)
β β β§ 1 β β) β (((expβπ΄) β 1) = 0 β (expβπ΄) = 1)) |
55 | 52, 53, 54 | sylancl 587 |
. . . 4
β’ (π΄ β β β
(((expβπ΄) β 1)
= 0 β (expβπ΄) =
1)) |
56 | 50, 51, 55 | 3bitr3d 309 |
. . 3
β’ (π΄ β β β
(((expβ(π΄ / 2))
β (expβ-(π΄ /
2))) = 0 β (expβπ΄) = 1)) |
57 | 23, 36, 56 | 3bitrd 305 |
. 2
β’ (π΄ β β β
((sinβ((π΄ / 2) / i))
= 0 β (expβπ΄) =
1)) |
58 | | 2cnne0 12368 |
. . . . . 6
β’ (2 β
β β§ 2 β 0) |
59 | 2, 3 | pm3.2i 472 |
. . . . . 6
β’ (i β
β β§ i β 0) |
60 | | divdiv32 11868 |
. . . . . 6
β’ ((π΄ β β β§ (2 β
β β§ 2 β 0) β§ (i β β β§ i β 0)) β ((π΄ / 2) / i) = ((π΄ / i) / 2)) |
61 | 58, 59, 60 | mp3an23 1454 |
. . . . 5
β’ (π΄ β β β ((π΄ / 2) / i) = ((π΄ / i) / 2)) |
62 | 61 | oveq1d 7373 |
. . . 4
β’ (π΄ β β β (((π΄ / 2) / i) / Ο) = (((π΄ / i) / 2) /
Ο)) |
63 | | divcl 11824 |
. . . . . . 7
β’ ((π΄ β β β§ i β
β β§ i β 0) β (π΄ / i) β β) |
64 | 2, 3, 63 | mp3an23 1454 |
. . . . . 6
β’ (π΄ β β β (π΄ / i) β
β) |
65 | | picn 25832 |
. . . . . . . 8
β’ Ο
β β |
66 | | pire 25831 |
. . . . . . . . 9
β’ Ο
β β |
67 | | pipos 25833 |
. . . . . . . . 9
β’ 0 <
Ο |
68 | 66, 67 | gt0ne0ii 11696 |
. . . . . . . 8
β’ Ο β
0 |
69 | 65, 68 | pm3.2i 472 |
. . . . . . 7
β’ (Ο
β β β§ Ο β 0) |
70 | | divdiv1 11871 |
. . . . . . 7
β’ (((π΄ / i) β β β§ (2
β β β§ 2 β 0) β§ (Ο β β β§ Ο β 0))
β (((π΄ / i) / 2) /
Ο) = ((π΄ / i) / (2
Β· Ο))) |
71 | 58, 69, 70 | mp3an23 1454 |
. . . . . 6
β’ ((π΄ / i) β β β
(((π΄ / i) / 2) / Ο) =
((π΄ / i) / (2 Β·
Ο))) |
72 | 64, 71 | syl 17 |
. . . . 5
β’ (π΄ β β β (((π΄ / i) / 2) / Ο) = ((π΄ / i) / (2 Β·
Ο))) |
73 | 30, 65 | mulcli 11167 |
. . . . . . 7
β’ (2
Β· Ο) β β |
74 | 30, 65, 32, 68 | mulne0i 11803 |
. . . . . . 7
β’ (2
Β· Ο) β 0 |
75 | 73, 74 | pm3.2i 472 |
. . . . . 6
β’ ((2
Β· Ο) β β β§ (2 Β· Ο) β 0) |
76 | | divdiv1 11871 |
. . . . . 6
β’ ((π΄ β β β§ (i β
β β§ i β 0) β§ ((2 Β· Ο) β β β§ (2
Β· Ο) β 0)) β ((π΄ / i) / (2 Β· Ο)) = (π΄ / (i Β· (2 Β·
Ο)))) |
77 | 59, 75, 76 | mp3an23 1454 |
. . . . 5
β’ (π΄ β β β ((π΄ / i) / (2 Β· Ο)) =
(π΄ / (i Β· (2
Β· Ο)))) |
78 | 72, 77 | eqtrd 2773 |
. . . 4
β’ (π΄ β β β (((π΄ / i) / 2) / Ο) = (π΄ / (i Β· (2 Β·
Ο)))) |
79 | 62, 78 | eqtrd 2773 |
. . 3
β’ (π΄ β β β (((π΄ / 2) / i) / Ο) = (π΄ / (i Β· (2 Β·
Ο)))) |
80 | 79 | eleq1d 2819 |
. 2
β’ (π΄ β β β ((((π΄ / 2) / i) / Ο) β
β€ β (π΄ / (i
Β· (2 Β· Ο))) β β€)) |
81 | 8, 57, 80 | 3bitr3d 309 |
1
β’ (π΄ β β β
((expβπ΄) = 1 β
(π΄ / (i Β· (2
Β· Ο))) β β€)) |