Step | Hyp | Ref
| Expression |
1 | | sinval 16009 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(sinβπ΄) =
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
2 | 1 | eqeq1d 2735 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
((sinβπ΄) = 0 β
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) =
0)) |
3 | | ax-icn 11115 |
. . . . . . . . . . . . . . . . . . . 20
β’ i β
β |
4 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
5 | 3, 4 | mpan 689 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β (i
Β· π΄) β
β) |
6 | | efcl 15970 |
. . . . . . . . . . . . . . . . . . 19
β’ ((i
Β· π΄) β β
β (expβ(i Β· π΄)) β β) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β
(expβ(i Β· π΄))
β β) |
8 | | negicn 11407 |
. . . . . . . . . . . . . . . . . . . 20
β’ -i β
β |
9 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((-i
β β β§ π΄
β β) β (-i Β· π΄) β β) |
10 | 8, 9 | mpan 689 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β (-i
Β· π΄) β
β) |
11 | | efcl 15970 |
. . . . . . . . . . . . . . . . . . 19
β’ ((-i
Β· π΄) β β
β (expβ(-i Β· π΄)) β β) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β
(expβ(-i Β· π΄))
β β) |
13 | 7, 12 | subcld 11517 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) β β) |
14 | | 2mulicn 12381 |
. . . . . . . . . . . . . . . . . 18
β’ (2
Β· i) β β |
15 | | 2muline0 12382 |
. . . . . . . . . . . . . . . . . 18
β’ (2
Β· i) β 0 |
16 | | diveq0 11828 |
. . . . . . . . . . . . . . . . . 18
β’
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) β β β§ (2
Β· i) β β β§ (2 Β· i) β 0) β ((((expβ(i
Β· π΄)) β
(expβ(-i Β· π΄))) / (2 Β· i)) = 0 β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) = 0)) |
17 | 14, 15, 16 | mp3an23 1454 |
. . . . . . . . . . . . . . . . 17
β’
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) β β β
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) = 0 β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) = 0)) |
18 | 13, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) = 0 β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) = 0)) |
19 | 7, 12 | subeq0ad 11527 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) = 0 β (expβ(i
Β· π΄)) =
(expβ(-i Β· π΄)))) |
20 | 2, 18, 19 | 3bitrd 305 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((sinβπ΄) = 0 β
(expβ(i Β· π΄))
= (expβ(-i Β· π΄)))) |
21 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’
((expβ(i Β· π΄)) = (expβ(-i Β· π΄)) β ((expβ(i
Β· π΄)) Β·
(expβ(i Β· π΄)))
= ((expβ(i Β· π΄)) Β· (expβ(-i Β· π΄)))) |
22 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
β |
23 | | mul12 11325 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((i
β β β§ 2 β β β§ π΄ β β) β (i Β· (2
Β· π΄)) = (2 Β·
(i Β· π΄))) |
24 | 3, 22, 23 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β β β (i
Β· (2 Β· π΄)) =
(2 Β· (i Β· π΄))) |
25 | 5 | 2timesd 12401 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β β β (2
Β· (i Β· π΄)) =
((i Β· π΄) + (i
Β· π΄))) |
26 | 24, 25 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β β (i
Β· (2 Β· π΄)) =
((i Β· π΄) + (i
Β· π΄))) |
27 | 26 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β
(expβ(i Β· (2 Β· π΄))) = (expβ((i Β· π΄) + (i Β· π΄)))) |
28 | | efadd 15981 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((i
Β· π΄) β β
β§ (i Β· π΄) β
β) β (expβ((i Β· π΄) + (i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(i
Β· π΄)))) |
29 | 5, 5, 28 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β
(expβ((i Β· π΄)
+ (i Β· π΄))) =
((expβ(i Β· π΄))
Β· (expβ(i Β· π΄)))) |
30 | 27, 29 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β
((expβ(i Β· π΄))
Β· (expβ(i Β· π΄))) = (expβ(i Β· (2 Β·
π΄)))) |
31 | | efadd 15981 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((i
Β· π΄) β β
β§ (-i Β· π΄)
β β) β (expβ((i Β· π΄) + (-i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(-i
Β· π΄)))) |
32 | 5, 10, 31 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β
(expβ((i Β· π΄)
+ (-i Β· π΄))) =
((expβ(i Β· π΄))
Β· (expβ(-i Β· π΄)))) |
33 | 3 | negidi 11475 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (i + -i)
= 0 |
34 | 33 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((i + -i)
Β· π΄) = (0 Β·
π΄) |
35 | | adddir 11151 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((i
β β β§ -i β β β§ π΄ β β) β ((i + -i) Β·
π΄) = ((i Β· π΄) + (-i Β· π΄))) |
36 | 3, 8, 35 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β β β ((i + -i)
Β· π΄) = ((i Β·
π΄) + (-i Β· π΄))) |
37 | | mul02 11338 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β β β (0
Β· π΄) =
0) |
38 | 34, 36, 37 | 3eqtr3a 2797 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β β β ((i
Β· π΄) + (-i Β·
π΄)) = 0) |
39 | 38 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β β
(expβ((i Β· π΄)
+ (-i Β· π΄))) =
(expβ0)) |
40 | | ef0 15978 |
. . . . . . . . . . . . . . . . . . . 20
β’
(expβ0) = 1 |
41 | 39, 40 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β
(expβ((i Β· π΄)
+ (-i Β· π΄))) =
1) |
42 | 32, 41 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β
((expβ(i Β· π΄))
Β· (expβ(-i Β· π΄))) = 1) |
43 | 30, 42 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) = ((expβ(i Β·
π΄)) Β· (expβ(-i
Β· π΄))) β
(expβ(i Β· (2 Β· π΄))) = 1)) |
44 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’
((expβ(i Β· (2 Β· π΄))) = 1 β (absβ(expβ(i
Β· (2 Β· π΄))))
= (absβ1)) |
45 | 43, 44 | syl6bi 253 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) = ((expβ(i Β·
π΄)) Β· (expβ(-i
Β· π΄))) β
(absβ(expβ(i Β· (2 Β· π΄)))) = (absβ1))) |
46 | 21, 45 | syl5 34 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((expβ(i Β· π΄))
= (expβ(-i Β· π΄)) β (absβ(expβ(i Β·
(2 Β· π΄)))) =
(absβ1))) |
47 | 20, 46 | sylbid 239 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
((sinβπ΄) = 0 β
(absβ(expβ(i Β· (2 Β· π΄)))) = (absβ1))) |
48 | | abs1 15188 |
. . . . . . . . . . . . . . . 16
β’
(absβ1) = 1 |
49 | 48 | eqeq2i 2746 |
. . . . . . . . . . . . . . 15
β’
((absβ(expβ(i Β· (2 Β· π΄)))) = (absβ1) β
(absβ(expβ(i Β· (2 Β· π΄)))) = 1) |
50 | | 2re 12232 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
51 | | 2ne0 12262 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
0 |
52 | | mulre 15012 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ 2 β
β β§ 2 β 0) β (π΄ β β β (2 Β· π΄) β
β)) |
53 | 50, 51, 52 | mp3an23 1454 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β (π΄ β β β (2
Β· π΄) β
β)) |
54 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
β β β§ π΄
β β) β (2 Β· π΄) β β) |
55 | 22, 54 | mpan 689 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β (2
Β· π΄) β
β) |
56 | | absefib 16085 |
. . . . . . . . . . . . . . . . 17
β’ ((2
Β· π΄) β β
β ((2 Β· π΄)
β β β (absβ(expβ(i Β· (2 Β· π΄)))) = 1)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β ((2
Β· π΄) β β
β (absβ(expβ(i Β· (2 Β· π΄)))) = 1)) |
58 | 53, 57 | bitr2d 280 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((absβ(expβ(i Β· (2 Β· π΄)))) = 1 β π΄ β β)) |
59 | 49, 58 | bitrid 283 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
((absβ(expβ(i Β· (2 Β· π΄)))) = (absβ1) β π΄ β
β)) |
60 | 47, 59 | sylibd 238 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
((sinβπ΄) = 0 β
π΄ β
β)) |
61 | 60 | imp 408 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
π΄ β
β) |
62 | | pirp 25834 |
. . . . . . . . . . . 12
β’ Ο
β β+ |
63 | | modval 13782 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ Ο
β β+) β (π΄ mod Ο) = (π΄ β (Ο Β·
(ββ(π΄ /
Ο))))) |
64 | 61, 62, 63 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) = (π΄ β (Ο Β·
(ββ(π΄ /
Ο))))) |
65 | | picn 25832 |
. . . . . . . . . . . . 13
β’ Ο
β β |
66 | | pire 25831 |
. . . . . . . . . . . . . . . . 17
β’ Ο
β β |
67 | | pipos 25833 |
. . . . . . . . . . . . . . . . . 18
β’ 0 <
Ο |
68 | 66, 67 | gt0ne0ii 11696 |
. . . . . . . . . . . . . . . . 17
β’ Ο β
0 |
69 | | redivcl 11879 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ Ο
β β β§ Ο β 0) β (π΄ / Ο) β β) |
70 | 66, 68, 69 | mp3an23 1454 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β (π΄ / Ο) β
β) |
71 | 61, 70 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ / Ο) β
β) |
72 | 71 | flcld 13709 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(ββ(π΄ / Ο))
β β€) |
73 | 72 | zcnd 12613 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(ββ(π΄ / Ο))
β β) |
74 | | mulcl 11140 |
. . . . . . . . . . . . 13
β’ ((Ο
β β β§ (ββ(π΄ / Ο)) β β) β (Ο
Β· (ββ(π΄
/ Ο))) β β) |
75 | 65, 73, 74 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(Ο Β· (ββ(π΄ / Ο))) β β) |
76 | | negsub 11454 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ (Ο
Β· (ββ(π΄
/ Ο))) β β) β (π΄ + -(Ο Β· (ββ(π΄ / Ο)))) = (π΄ β (Ο Β·
(ββ(π΄ /
Ο))))) |
77 | 75, 76 | syldan 592 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ + -(Ο Β·
(ββ(π΄ /
Ο)))) = (π΄ β (Ο
Β· (ββ(π΄
/ Ο))))) |
78 | | mulcom 11142 |
. . . . . . . . . . . . . . 15
β’ ((Ο
β β β§ (ββ(π΄ / Ο)) β β) β (Ο
Β· (ββ(π΄
/ Ο))) = ((ββ(π΄ / Ο)) Β· Ο)) |
79 | 65, 73, 78 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(Ο Β· (ββ(π΄ / Ο))) = ((ββ(π΄ / Ο)) Β·
Ο)) |
80 | 79 | negeqd 11400 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
-(Ο Β· (ββ(π΄ / Ο))) = -((ββ(π΄ / Ο)) Β·
Ο)) |
81 | | mulneg1 11596 |
. . . . . . . . . . . . . 14
β’
(((ββ(π΄
/ Ο)) β β β§ Ο β β) β
(-(ββ(π΄ /
Ο)) Β· Ο) = -((ββ(π΄ / Ο)) Β· Ο)) |
82 | 73, 65, 81 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(-(ββ(π΄ /
Ο)) Β· Ο) = -((ββ(π΄ / Ο)) Β· Ο)) |
83 | 80, 82 | eqtr4d 2776 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
-(Ο Β· (ββ(π΄ / Ο))) = (-(ββ(π΄ / Ο)) Β·
Ο)) |
84 | 83 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ + -(Ο Β·
(ββ(π΄ /
Ο)))) = (π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο))) |
85 | 64, 77, 84 | 3eqtr2d 2779 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) = (π΄ + (-(ββ(π΄ / Ο)) Β·
Ο))) |
86 | 85 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(sinβ(π΄ mod Ο)) =
(sinβ(π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο)))) |
87 | 86 | fveq2d 6847 |
. . . . . . . 8
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβ(π΄
mod Ο))) = (absβ(sinβ(π΄ + (-(ββ(π΄ / Ο)) Β·
Ο))))) |
88 | 72 | znegcld 12614 |
. . . . . . . . 9
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
-(ββ(π΄ / Ο))
β β€) |
89 | | abssinper 25893 |
. . . . . . . . 9
β’ ((π΄ β β β§
-(ββ(π΄ / Ο))
β β€) β (absβ(sinβ(π΄ + (-(ββ(π΄ / Ο)) Β· Ο)))) =
(absβ(sinβπ΄))) |
90 | 88, 89 | syldan 592 |
. . . . . . . 8
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβ(π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο)))) = (absβ(sinβπ΄))) |
91 | | simpr 486 |
. . . . . . . . 9
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(sinβπ΄) =
0) |
92 | 91 | fveq2d 6847 |
. . . . . . . 8
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβπ΄)) =
(absβ0)) |
93 | 87, 90, 92 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβ(π΄
mod Ο))) = (absβ0)) |
94 | | abs0 15176 |
. . . . . . 7
β’
(absβ0) = 0 |
95 | 93, 94 | eqtrdi 2789 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβ(π΄
mod Ο))) = 0) |
96 | | modcl 13784 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ Ο
β β+) β (π΄ mod Ο) β β) |
97 | 61, 62, 96 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) β
β) |
98 | | modlt 13791 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ Ο
β β+) β (π΄ mod Ο) < Ο) |
99 | 61, 62, 98 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) <
Ο) |
100 | 97, 99 | jca 513 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((π΄ mod Ο) β
β β§ (π΄ mod Ο)
< Ο)) |
101 | 100 | biantrurd 534 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(0 < (π΄ mod Ο) β
(((π΄ mod Ο) β
β β§ (π΄ mod Ο)
< Ο) β§ 0 < (π΄
mod Ο)))) |
102 | | 0re 11162 |
. . . . . . . . . . . 12
β’ 0 β
β |
103 | | rexr 11206 |
. . . . . . . . . . . . 13
β’ (0 β
β β 0 β β*) |
104 | | rexr 11206 |
. . . . . . . . . . . . 13
β’ (Ο
β β β Ο β β*) |
105 | | elioo2 13311 |
. . . . . . . . . . . . 13
β’ ((0
β β* β§ Ο β β*) β
((π΄ mod Ο) β
(0(,)Ο) β ((π΄ mod
Ο) β β β§ 0 < (π΄ mod Ο) β§ (π΄ mod Ο) < Ο))) |
106 | 103, 104,
105 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((0
β β β§ Ο β β) β ((π΄ mod Ο) β (0(,)Ο) β ((π΄ mod Ο) β β β§
0 < (π΄ mod Ο) β§
(π΄ mod Ο) <
Ο))) |
107 | 102, 66, 106 | mp2an 691 |
. . . . . . . . . . 11
β’ ((π΄ mod Ο) β (0(,)Ο)
β ((π΄ mod Ο) β
β β§ 0 < (π΄ mod
Ο) β§ (π΄ mod Ο)
< Ο)) |
108 | | 3anan32 1098 |
. . . . . . . . . . 11
β’ (((π΄ mod Ο) β β β§
0 < (π΄ mod Ο) β§
(π΄ mod Ο) < Ο)
β (((π΄ mod Ο)
β β β§ (π΄ mod
Ο) < Ο) β§ 0 < (π΄ mod Ο))) |
109 | 107, 108 | bitri 275 |
. . . . . . . . . 10
β’ ((π΄ mod Ο) β (0(,)Ο)
β (((π΄ mod Ο)
β β β§ (π΄ mod
Ο) < Ο) β§ 0 < (π΄ mod Ο))) |
110 | 101, 109 | bitr4di 289 |
. . . . . . . . 9
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(0 < (π΄ mod Ο) β
(π΄ mod Ο) β
(0(,)Ο))) |
111 | | sinq12gt0 25880 |
. . . . . . . . . 10
β’ ((π΄ mod Ο) β (0(,)Ο)
β 0 < (sinβ(π΄
mod Ο))) |
112 | | elioore 13300 |
. . . . . . . . . . . 12
β’ ((π΄ mod Ο) β (0(,)Ο)
β (π΄ mod Ο) β
β) |
113 | 112 | resincld 16030 |
. . . . . . . . . . 11
β’ ((π΄ mod Ο) β (0(,)Ο)
β (sinβ(π΄ mod
Ο)) β β) |
114 | | ltle 11248 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ (sinβ(π΄ mod Ο)) β β) β (0 <
(sinβ(π΄ mod Ο))
β 0 β€ (sinβ(π΄
mod Ο)))) |
115 | 102, 113,
114 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ mod Ο) β (0(,)Ο)
β (0 < (sinβ(π΄ mod Ο)) β 0 β€ (sinβ(π΄ mod Ο)))) |
116 | 111, 115 | mpd 15 |
. . . . . . . . . . 11
β’ ((π΄ mod Ο) β (0(,)Ο)
β 0 β€ (sinβ(π΄
mod Ο))) |
117 | 113, 116 | absidd 15313 |
. . . . . . . . . 10
β’ ((π΄ mod Ο) β (0(,)Ο)
β (absβ(sinβ(π΄ mod Ο))) = (sinβ(π΄ mod Ο))) |
118 | 111, 117 | breqtrrd 5134 |
. . . . . . . . 9
β’ ((π΄ mod Ο) β (0(,)Ο)
β 0 < (absβ(sinβ(π΄ mod Ο)))) |
119 | 110, 118 | syl6bi 253 |
. . . . . . . 8
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(0 < (π΄ mod Ο) β
0 < (absβ(sinβ(π΄ mod Ο))))) |
120 | | ltne 11257 |
. . . . . . . . 9
β’ ((0
β β β§ 0 < (absβ(sinβ(π΄ mod Ο)))) β
(absβ(sinβ(π΄
mod Ο))) β 0) |
121 | 102, 120 | mpan 689 |
. . . . . . . 8
β’ (0 <
(absβ(sinβ(π΄
mod Ο))) β (absβ(sinβ(π΄ mod Ο))) β 0) |
122 | 119, 121 | syl6 35 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(0 < (π΄ mod Ο) β
(absβ(sinβ(π΄
mod Ο))) β 0)) |
123 | 122 | necon2bd 2956 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((absβ(sinβ(π΄
mod Ο))) = 0 β Β¬ 0 < (π΄ mod Ο))) |
124 | 95, 123 | mpd 15 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Β¬ 0 < (π΄ mod
Ο)) |
125 | | modge0 13790 |
. . . . . . . 8
β’ ((π΄ β β β§ Ο
β β+) β 0 β€ (π΄ mod Ο)) |
126 | 61, 62, 125 | sylancl 587 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β 0
β€ (π΄ mod
Ο)) |
127 | | leloe 11246 |
. . . . . . . 8
β’ ((0
β β β§ (π΄ mod
Ο) β β) β (0 β€ (π΄ mod Ο) β (0 < (π΄ mod Ο) β¨ 0 = (π΄ mod Ο)))) |
128 | 102, 97, 127 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(0 β€ (π΄ mod Ο) β
(0 < (π΄ mod Ο) β¨ 0
= (π΄ mod
Ο)))) |
129 | 126, 128 | mpbid 231 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(0 < (π΄ mod Ο) β¨ 0
= (π΄ mod
Ο))) |
130 | 129 | ord 863 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(Β¬ 0 < (π΄ mod Ο)
β 0 = (π΄ mod
Ο))) |
131 | 124, 130 | mpd 15 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) = 0) β 0
= (π΄ mod
Ο)) |
132 | 131 | eqcomd 2739 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) =
0) |
133 | | mod0 13787 |
. . . 4
β’ ((π΄ β β β§ Ο
β β+) β ((π΄ mod Ο) = 0 β (π΄ / Ο) β β€)) |
134 | 61, 62, 133 | sylancl 587 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((π΄ mod Ο) = 0 β
(π΄ / Ο) β
β€)) |
135 | 132, 134 | mpbid 231 |
. 2
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ / Ο) β
β€) |
136 | | divcan1 11827 |
. . . . 5
β’ ((π΄ β β β§ Ο
β β β§ Ο β 0) β ((π΄ / Ο) Β· Ο) = π΄) |
137 | 65, 68, 136 | mp3an23 1454 |
. . . 4
β’ (π΄ β β β ((π΄ / Ο) Β· Ο) = π΄) |
138 | 137 | fveq2d 6847 |
. . 3
β’ (π΄ β β β
(sinβ((π΄ / Ο)
Β· Ο)) = (sinβπ΄)) |
139 | | sinkpi 25894 |
. . 3
β’ ((π΄ / Ο) β β€ β
(sinβ((π΄ / Ο)
Β· Ο)) = 0) |
140 | 138, 139 | sylan9req 2794 |
. 2
β’ ((π΄ β β β§ (π΄ / Ο) β β€) β
(sinβπ΄) =
0) |
141 | 135, 140 | impbida 800 |
1
β’ (π΄ β β β
((sinβπ΄) = 0 β
(π΄ / Ο) β
β€)) |