Step | Hyp | Ref
| Expression |
1 | | pire 25831 |
. . . . 5
β’ Ο
β β |
2 | | pipos 25833 |
. . . . 5
β’ 0 <
Ο |
3 | 1, 2 | elrpii 12923 |
. . . 4
β’ Ο
β β+ |
4 | | 2ne0 12262 |
. . . . . 6
β’ 2 β
0 |
5 | 4 | a1i 11 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) = 0) β 2
β 0) |
6 | | 2cn 12233 |
. . . . . . 7
β’ 2 β
β |
7 | | 2re 12232 |
. . . . . . . 8
β’ 2 β
β |
8 | 7 | a1i 11 |
. . . . . . 7
β’ (2 β
β β 2 β β) |
9 | 6, 8 | ax-mp 5 |
. . . . . 6
β’ 2 β
β |
10 | 9 | a1i 11 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) = 0) β 2
β β) |
11 | | id 22 |
. . . . . 6
β’ (π΄ β β β π΄ β
β) |
12 | 11 | adantr 482 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
π΄ β
β) |
13 | 6 | a1i 11 |
. . . . . . 7
β’ (π΄ β β β 2 β
β) |
14 | 13, 11 | mulcld 11180 |
. . . . . 6
β’ (π΄ β β β (2
Β· π΄) β
β) |
15 | | ax-icn 11115 |
. . . . . . . . . . . . . . 15
β’ i β
β |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β i β
β) |
17 | 13, 16, 11 | mul12d 11369 |
. . . . . . . . . . . . 13
β’ (π΄ β β β (2
Β· (i Β· π΄)) =
(i Β· (2 Β· π΄))) |
18 | 16, 11 | mulcld 11180 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β (i
Β· π΄) β
β) |
19 | 18 | 2timesd 12401 |
. . . . . . . . . . . . 13
β’ (π΄ β β β (2
Β· (i Β· π΄)) =
((i Β· π΄) + (i
Β· π΄))) |
20 | 17, 19 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ (π΄ β β β (i
Β· (2 Β· π΄)) =
((i Β· π΄) + (i
Β· π΄))) |
21 | 20 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π΄ β β β
(expβ(i Β· (2 Β· π΄))) = (expβ((i Β· π΄) + (i Β· π΄)))) |
22 | | efadd 15981 |
. . . . . . . . . . . 12
β’ (((i
Β· π΄) β β
β§ (i Β· π΄) β
β) β (expβ((i Β· π΄) + (i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(i
Β· π΄)))) |
23 | 18, 18, 22 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π΄ β β β
(expβ((i Β· π΄)
+ (i Β· π΄))) =
((expβ(i Β· π΄))
Β· (expβ(i Β· π΄)))) |
24 | 21, 23 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π΄ β β β
(expβ(i Β· (2 Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(i
Β· π΄)))) |
25 | 24 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(expβ(i Β· (2 Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(i
Β· π΄)))) |
26 | | sinval 16009 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(sinβπ΄) =
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
27 | | id 22 |
. . . . . . . . . . . . . . 15
β’
((sinβπ΄) = 0
β (sinβπ΄) =
0) |
28 | 26, 27 | sylan9req 2794 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) =
0) |
29 | | efcl 15970 |
. . . . . . . . . . . . . . . . . 18
β’ ((i
Β· π΄) β β
β (expβ(i Β· π΄)) β β) |
30 | 18, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(expβ(i Β· π΄))
β β) |
31 | | negicn 11407 |
. . . . . . . . . . . . . . . . . . . 20
β’ -i β
β |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β -i β
β) |
33 | 32, 11 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β (-i
Β· π΄) β
β) |
34 | | efcl 15970 |
. . . . . . . . . . . . . . . . . 18
β’ ((-i
Β· π΄) β β
β (expβ(-i Β· π΄)) β β) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(expβ(-i Β· π΄))
β β) |
36 | 30, 35 | subcld 11517 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) β β) |
37 | | 2mulicn 12381 |
. . . . . . . . . . . . . . . . 17
β’ (2
Β· i) β β |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β (2
Β· i) β β) |
39 | | 2muline0 12382 |
. . . . . . . . . . . . . . . . 17
β’ (2
Β· i) β 0 |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β (2
Β· i) β 0) |
41 | 36, 38, 40 | diveq0ad 11946 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) = 0 β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) = 0)) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) = 0 β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) = 0)) |
43 | 28, 42 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) = 0) |
44 | 30, 35 | subeq0ad 11527 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) = 0 β (expβ(i
Β· π΄)) =
(expβ(-i Β· π΄)))) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) = 0 β (expβ(i
Β· π΄)) =
(expβ(-i Β· π΄)))) |
46 | 43, 45 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(expβ(i Β· π΄))
= (expβ(-i Β· π΄))) |
47 | 46 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((expβ(i Β· π΄))
Β· (expβ(i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(-i
Β· π΄)))) |
48 | | efadd 15981 |
. . . . . . . . . . . . 13
β’ (((i
Β· π΄) β β
β§ (-i Β· π΄)
β β) β (expβ((i Β· π΄) + (-i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(-i
Β· π΄)))) |
49 | 18, 33, 48 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π΄ β β β
(expβ((i Β· π΄)
+ (-i Β· π΄))) =
((expβ(i Β· π΄))
Β· (expβ(-i Β· π΄)))) |
50 | 49 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(expβ((i Β· π΄)
+ (-i Β· π΄))) =
((expβ(i Β· π΄))
Β· (expβ(-i Β· π΄)))) |
51 | 47, 50 | eqtr4d 2776 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((expβ(i Β· π΄))
Β· (expβ(i Β· π΄))) = (expβ((i Β· π΄) + (-i Β· π΄)))) |
52 | 16, 32, 11 | adddird 11185 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β ((i + -i)
Β· π΄) = ((i Β·
π΄) + (-i Β· π΄))) |
53 | 15 | negidi 11475 |
. . . . . . . . . . . . . . 15
β’ (i + -i)
= 0 |
54 | 53 | oveq1i 7368 |
. . . . . . . . . . . . . 14
β’ ((i + -i)
Β· π΄) = (0 Β·
π΄) |
55 | 52, 54 | eqtr3di 2788 |
. . . . . . . . . . . . 13
β’ (π΄ β β β ((i
Β· π΄) + (-i Β·
π΄)) = (0 Β· π΄)) |
56 | 11 | mul02d 11358 |
. . . . . . . . . . . . 13
β’ (π΄ β β β (0
Β· π΄) =
0) |
57 | 55, 56 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π΄ β β β ((i
Β· π΄) + (-i Β·
π΄)) = 0) |
58 | 57 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π΄ β β β
(expβ((i Β· π΄)
+ (-i Β· π΄))) =
(expβ0)) |
59 | 58 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(expβ((i Β· π΄)
+ (-i Β· π΄))) =
(expβ0)) |
60 | | ef0 15978 |
. . . . . . . . . . 11
β’
(expβ0) = 1 |
61 | 60 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(expβ0) = 1) |
62 | 51, 59, 61 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((expβ(i Β· π΄))
Β· (expβ(i Β· π΄))) = 1) |
63 | 25, 62 | eqtrd 2773 |
. . . . . . . 8
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(expβ(i Β· (2 Β· π΄))) = 1) |
64 | 63 | fveq2d 6847 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(expβ(i Β· (2 Β· π΄)))) = (absβ1)) |
65 | | abs1 15188 |
. . . . . . 7
β’
(absβ1) = 1 |
66 | 64, 65 | eqtrdi 2789 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(expβ(i Β· (2 Β· π΄)))) = 1) |
67 | | absefib 16085 |
. . . . . . . 8
β’ ((2
Β· π΄) β β
β ((2 Β· π΄)
β β β (absβ(expβ(i Β· (2 Β· π΄)))) = 1)) |
68 | 67 | biimparc 481 |
. . . . . . 7
β’
(((absβ(expβ(i Β· (2 Β· π΄)))) = 1 β§ (2 Β· π΄) β β) β (2 Β· π΄) β
β) |
69 | 68 | ancoms 460 |
. . . . . 6
β’ (((2
Β· π΄) β β
β§ (absβ(expβ(i Β· (2 Β· π΄)))) = 1) β (2 Β· π΄) β
β) |
70 | 14, 66, 69 | syl2an2r 684 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(2 Β· π΄) β
β) |
71 | | mulre 15012 |
. . . . . . 7
β’ ((π΄ β β β§ 2 β
β β§ 2 β 0) β (π΄ β β β (2 Β· π΄) β
β)) |
72 | 71 | 4animp1 42867 |
. . . . . 6
β’ ((((π΄ β β β§ 2 β
β) β§ 2 β 0) β§ (2 Β· π΄) β β) β π΄ β β) |
73 | 72 | 4an31 42868 |
. . . . 5
β’ ((((2
β 0 β§ 2 β β) β§ π΄ β β) β§ (2 Β· π΄) β β) β π΄ β
β) |
74 | 5, 10, 12, 70, 73 | syl1111anc 839 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
π΄ β
β) |
75 | 3 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Ο β β+) |
76 | 74, 75 | modcld 13786 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) β
β) |
77 | 76 | recnd 11188 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) β
β) |
78 | 77 | sincld 16017 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(sinβ(π΄ mod Ο))
β β) |
79 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Ο β β) |
80 | | 0re 11162 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
β |
81 | 80, 1, 2 | ltleii 11283 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β€
Ο |
82 | | gt0ne0 11625 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((Ο
β β β§ 0 < Ο) β Ο β 0) |
83 | 82 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Ο
β β β§ 0 < Ο β§ 0 β€ Ο) β Ο β
0) |
84 | 83 | 3com23 1127 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Ο
β β β§ 0 β€ Ο β§ 0 < Ο) β Ο β
0) |
85 | 1, 81, 2, 84 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . 20
β’ Ο β
0 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Ο β 0) |
87 | 74, 79, 86 | redivcld 11988 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ / Ο) β
β) |
88 | 87 | flcld 13709 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(ββ(π΄ / Ο))
β β€) |
89 | 88 | znegcld 12614 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
-(ββ(π΄ / Ο))
β β€) |
90 | | abssinper 25893 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β β§
-(ββ(π΄ / Ο))
β β€) β (absβ(sinβ(π΄ + (-(ββ(π΄ / Ο)) Β· Ο)))) =
(absβ(sinβπ΄))) |
91 | 90 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§
-(ββ(π΄ / Ο))
β β€) β (absβ(sinβπ΄)) = (absβ(sinβ(π΄ + (-(ββ(π΄ / Ο)) Β·
Ο))))) |
92 | 91 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β
(-(ββ(π΄ /
Ο)) β β€ β (absβ(sinβπ΄)) = (absβ(sinβ(π΄ + (-(ββ(π΄ / Ο)) Β·
Ο)))))) |
93 | 92 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(-(ββ(π΄ /
Ο)) β β€ β (absβ(sinβπ΄)) = (absβ(sinβ(π΄ + (-(ββ(π΄ / Ο)) Β·
Ο)))))) |
94 | 89, 93 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβπ΄)) =
(absβ(sinβ(π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο))))) |
95 | 88 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(ββ(π΄ / Ο))
β β) |
96 | 95 | negcld 11504 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
-(ββ(π΄ / Ο))
β β) |
97 | 1 | recni 11174 |
. . . . . . . . . . . . . . . . . . . . 21
β’ Ο
β β |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Ο β β) |
99 | 96, 98 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(-(ββ(π΄ /
Ο)) Β· Ο) β β) |
100 | 98, 95 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(Ο Β· (ββ(π΄ / Ο))) β β) |
101 | 100 | negcld 11504 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
-(Ο Β· (ββ(π΄ / Ο))) β β) |
102 | 95, 98 | mulneg1d 11613 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(-(ββ(π΄ /
Ο)) Β· Ο) = -((ββ(π΄ / Ο)) Β· Ο)) |
103 | 95, 98 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((ββ(π΄ / Ο))
Β· Ο) = (Ο Β· (ββ(π΄ / Ο)))) |
104 | 103 | negeqd 11400 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
-((ββ(π΄ /
Ο)) Β· Ο) = -(Ο Β· (ββ(π΄ / Ο)))) |
105 | 102, 104 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(-(ββ(π΄ /
Ο)) Β· Ο) = -(Ο Β· (ββ(π΄ / Ο)))) |
106 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((-(ββ(π΄
/ Ο)) Β· Ο) = -(Ο Β· (ββ(π΄ / Ο))) β (π΄ + (-(ββ(π΄ / Ο)) Β· Ο)) = (π΄ + -(Ο Β·
(ββ(π΄ /
Ο))))) |
107 | 106 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((-(ββ(π΄ / Ο)) Β· Ο) = -(Ο Β·
(ββ(π΄ / Ο)))
β§ -(Ο Β· (ββ(π΄ / Ο))) β β) β§
(-(ββ(π΄ /
Ο)) Β· Ο) β β) β§ π΄ β β) β (π΄ + (-(ββ(π΄ / Ο)) Β· Ο)) = (π΄ + -(Ο Β·
(ββ(π΄ /
Ο))))) |
108 | 107 | 4an4132 42869 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β β§
(-(ββ(π΄ /
Ο)) Β· Ο) β β) β§ -(Ο Β·
(ββ(π΄ / Ο)))
β β) β§ (-(ββ(π΄ / Ο)) Β· Ο) = -(Ο Β·
(ββ(π΄ /
Ο)))) β (π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο)) = (π΄
+ -(Ο Β· (ββ(π΄ / Ο))))) |
109 | 12, 99, 101, 105, 108 | syl1111anc 839 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο)) = (π΄
+ -(Ο Β· (ββ(π΄ / Ο))))) |
110 | 12, 100 | negsubd 11523 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ + -(Ο Β·
(ββ(π΄ /
Ο)))) = (π΄ β (Ο
Β· (ββ(π΄
/ Ο))))) |
111 | 109, 110 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο)) = (π΄
β (Ο Β· (ββ(π΄ / Ο))))) |
112 | 111 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(sinβ(π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο))) = (sinβ(π΄ β (Ο Β·
(ββ(π΄ /
Ο)))))) |
113 | 112 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβ(π΄ +
(-(ββ(π΄ /
Ο)) Β· Ο)))) = (absβ(sinβ(π΄ β (Ο Β·
(ββ(π΄ /
Ο))))))) |
114 | 94, 113 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβπ΄)) =
(absβ(sinβ(π΄
β (Ο Β· (ββ(π΄ / Ο))))))) |
115 | | modval 13782 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§ Ο
β β+) β (π΄ mod Ο) = (π΄ β (Ο Β·
(ββ(π΄ /
Ο))))) |
116 | 115 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ Ο
β β+) β (sinβ(π΄ mod Ο)) = (sinβ(π΄ β (Ο Β·
(ββ(π΄ /
Ο)))))) |
117 | 116 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ Ο
β β+) β (absβ(sinβ(π΄ mod Ο))) = (absβ(sinβ(π΄ β (Ο Β·
(ββ(π΄ /
Ο))))))) |
118 | 3, 117 | mpan2 690 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(absβ(sinβ(π΄
mod Ο))) = (absβ(sinβ(π΄ β (Ο Β·
(ββ(π΄ /
Ο))))))) |
119 | 74, 118 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβ(π΄
mod Ο))) = (absβ(sinβ(π΄ β (Ο Β·
(ββ(π΄ /
Ο))))))) |
120 | 114, 119 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβπ΄)) =
(absβ(sinβ(π΄
mod Ο)))) |
121 | 27 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’
((sinβπ΄) = 0
β (absβ(sinβπ΄)) = (absβ0)) |
122 | | abs0 15176 |
. . . . . . . . . . . . . . 15
β’
(absβ0) = 0 |
123 | 121, 122 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’
((sinβπ΄) = 0
β (absβ(sinβπ΄)) = 0) |
124 | 123 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβπ΄)) =
0) |
125 | 120, 124 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(absβ(sinβ(π΄
mod Ο))) = 0) |
126 | 78, 125 | abs00d 15337 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(sinβ(π΄ mod Ο)) =
0) |
127 | | notnotb 315 |
. . . . . . . . . . . . 13
β’
((sinβ(π΄ mod
Ο)) = 0 β Β¬ Β¬ (sinβ(π΄ mod Ο)) = 0) |
128 | 127 | bicomi 223 |
. . . . . . . . . . . 12
β’ (Β¬
Β¬ (sinβ(π΄ mod
Ο)) = 0 β (sinβ(π΄ mod Ο)) = 0) |
129 | | ltne 11257 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β β§ 0 < (sinβ(π΄ mod Ο))) β (sinβ(π΄ mod Ο)) β
0) |
130 | 129 | neneqd 2945 |
. . . . . . . . . . . . . . 15
β’ ((0
β β β§ 0 < (sinβ(π΄ mod Ο))) β Β¬ (sinβ(π΄ mod Ο)) =
0) |
131 | 130 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (0 <
(sinβ(π΄ mod Ο))
β (0 β β β Β¬ (sinβ(π΄ mod Ο)) = 0)) |
132 | 80, 131 | mpi 20 |
. . . . . . . . . . . . 13
β’ (0 <
(sinβ(π΄ mod Ο))
β Β¬ (sinβ(π΄
mod Ο)) = 0) |
133 | 132 | con3i 154 |
. . . . . . . . . . . 12
β’ (Β¬
Β¬ (sinβ(π΄ mod
Ο)) = 0 β Β¬ 0 < (sinβ(π΄ mod Ο))) |
134 | 128, 133 | sylbir 234 |
. . . . . . . . . . 11
β’
((sinβ(π΄ mod
Ο)) = 0 β Β¬ 0 < (sinβ(π΄ mod Ο))) |
135 | 126, 134 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Β¬ 0 < (sinβ(π΄
mod Ο))) |
136 | | sinq12gt0 25880 |
. . . . . . . . . 10
β’ ((π΄ mod Ο) β (0(,)Ο)
β 0 < (sinβ(π΄
mod Ο))) |
137 | 135, 136 | nsyl 140 |
. . . . . . . . 9
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Β¬ (π΄ mod Ο) β
(0(,)Ο)) |
138 | 80 | rexri 11218 |
. . . . . . . . . . 11
β’ 0 β
β* |
139 | 1 | rexri 11218 |
. . . . . . . . . . 11
β’ Ο
β β* |
140 | | elioo2 13311 |
. . . . . . . . . . 11
β’ ((0
β β* β§ Ο β β*) β
((π΄ mod Ο) β
(0(,)Ο) β ((π΄ mod
Ο) β β β§ 0 < (π΄ mod Ο) β§ (π΄ mod Ο) < Ο))) |
141 | 138, 139,
140 | mp2an 691 |
. . . . . . . . . 10
β’ ((π΄ mod Ο) β (0(,)Ο)
β ((π΄ mod Ο) β
β β§ 0 < (π΄ mod
Ο) β§ (π΄ mod Ο)
< Ο)) |
142 | 141 | notbii 320 |
. . . . . . . . 9
β’ (Β¬
(π΄ mod Ο) β
(0(,)Ο) β Β¬ ((π΄
mod Ο) β β β§ 0 < (π΄ mod Ο) β§ (π΄ mod Ο) < Ο)) |
143 | 137, 142 | sylib 217 |
. . . . . . . 8
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Β¬ ((π΄ mod Ο) β
β β§ 0 < (π΄ mod
Ο) β§ (π΄ mod Ο)
< Ο)) |
144 | | 3anan12 1097 |
. . . . . . . . 9
β’ (((π΄ mod Ο) β β β§
0 < (π΄ mod Ο) β§
(π΄ mod Ο) < Ο)
β (0 < (π΄ mod Ο)
β§ ((π΄ mod Ο) β
β β§ (π΄ mod Ο)
< Ο))) |
145 | 144 | notbii 320 |
. . . . . . . 8
β’ (Β¬
((π΄ mod Ο) β
β β§ 0 < (π΄ mod
Ο) β§ (π΄ mod Ο)
< Ο) β Β¬ (0 < (π΄ mod Ο) β§ ((π΄ mod Ο) β β β§ (π΄ mod Ο) <
Ο))) |
146 | 143, 145 | sylib 217 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Β¬ (0 < (π΄ mod Ο)
β§ ((π΄ mod Ο) β
β β§ (π΄ mod Ο)
< Ο))) |
147 | | modlt 13791 |
. . . . . . . . . 10
β’ ((π΄ β β β§ Ο
β β+) β (π΄ mod Ο) < Ο) |
148 | 147 | ancoms 460 |
. . . . . . . . 9
β’ ((Ο
β β+ β§ π΄ β β) β (π΄ mod Ο) < Ο) |
149 | 3, 74, 148 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) <
Ο) |
150 | 76, 149 | jca 513 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
((π΄ mod Ο) β
β β§ (π΄ mod Ο)
< Ο)) |
151 | | not12an2impnot1 42938 |
. . . . . . 7
β’ ((Β¬
(0 < (π΄ mod Ο) β§
((π΄ mod Ο) β
β β§ (π΄ mod Ο)
< Ο)) β§ ((π΄ mod
Ο) β β β§ (π΄ mod Ο) < Ο)) β Β¬ 0 <
(π΄ mod
Ο)) |
152 | 146, 150,
151 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
Β¬ 0 < (π΄ mod
Ο)) |
153 | | modge0 13790 |
. . . . . . . . 9
β’ ((π΄ β β β§ Ο
β β+) β 0 β€ (π΄ mod Ο)) |
154 | 153 | ancoms 460 |
. . . . . . . 8
β’ ((Ο
β β+ β§ π΄ β β) β 0 β€ (π΄ mod Ο)) |
155 | 3, 74, 154 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β β§
(sinβπ΄) = 0) β 0
β€ (π΄ mod
Ο)) |
156 | | leloe 11246 |
. . . . . . . . 9
β’ ((0
β β β§ (π΄ mod
Ο) β β) β (0 β€ (π΄ mod Ο) β (0 < (π΄ mod Ο) β¨ 0 = (π΄ mod Ο)))) |
157 | 156 | biimp3a 1470 |
. . . . . . . 8
β’ ((0
β β β§ (π΄ mod
Ο) β β β§ 0 β€ (π΄ mod Ο)) β (0 < (π΄ mod Ο) β¨ 0 = (π΄ mod Ο))) |
158 | 157 | idiALT 42847 |
. . . . . . 7
β’ ((0
β β β§ (π΄ mod
Ο) β β β§ 0 β€ (π΄ mod Ο)) β (0 < (π΄ mod Ο) β¨ 0 = (π΄ mod Ο))) |
159 | 80, 76, 155, 158 | mp3an2i 1467 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(0 < (π΄ mod Ο) β¨ 0
= (π΄ mod
Ο))) |
160 | | pm2.53 850 |
. . . . . . . 8
β’ ((0 <
(π΄ mod Ο) β¨ 0 =
(π΄ mod Ο)) β (Β¬
0 < (π΄ mod Ο) β
0 = (π΄ mod
Ο))) |
161 | 160 | imp 408 |
. . . . . . 7
β’ (((0 <
(π΄ mod Ο) β¨ 0 =
(π΄ mod Ο)) β§ Β¬ 0
< (π΄ mod Ο)) β 0
= (π΄ mod
Ο)) |
162 | 161 | ancoms 460 |
. . . . . 6
β’ ((Β¬ 0
< (π΄ mod Ο) β§ (0
< (π΄ mod Ο) β¨ 0 =
(π΄ mod Ο))) β 0 =
(π΄ mod
Ο)) |
163 | 152, 159,
162 | syl2anc 585 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) = 0) β 0
= (π΄ mod
Ο)) |
164 | 163 | eqcomd 2739 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ mod Ο) =
0) |
165 | | mod0 13787 |
. . . . . 6
β’ ((π΄ β β β§ Ο
β β+) β ((π΄ mod Ο) = 0 β (π΄ / Ο) β β€)) |
166 | 165 | biimp3a 1470 |
. . . . 5
β’ ((π΄ β β β§ Ο
β β+ β§ (π΄ mod Ο) = 0) β (π΄ / Ο) β β€) |
167 | 166 | 3com12 1124 |
. . . 4
β’ ((Ο
β β+ β§ π΄ β β β§ (π΄ mod Ο) = 0) β (π΄ / Ο) β β€) |
168 | 3, 74, 164, 167 | mp3an2i 1467 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) = 0) β
(π΄ / Ο) β
β€) |
169 | 168 | ex 414 |
. 2
β’ (π΄ β β β
((sinβπ΄) = 0 β
(π΄ / Ο) β
β€)) |
170 | 97 | a1i 11 |
. . . . . 6
β’ (π΄ β β β Ο
β β) |
171 | 85 | a1i 11 |
. . . . . 6
β’ (π΄ β β β Ο β
0) |
172 | 11, 170, 171 | divcan1d 11937 |
. . . . 5
β’ (π΄ β β β ((π΄ / Ο) Β· Ο) = π΄) |
173 | 172 | fveq2d 6847 |
. . . 4
β’ (π΄ β β β
(sinβ((π΄ / Ο)
Β· Ο)) = (sinβπ΄)) |
174 | | id 22 |
. . . . 5
β’ ((π΄ / Ο) β β€ β
(π΄ / Ο) β
β€) |
175 | | sinkpi 25894 |
. . . . 5
β’ ((π΄ / Ο) β β€ β
(sinβ((π΄ / Ο)
Β· Ο)) = 0) |
176 | 174, 175 | syl 17 |
. . . 4
β’ ((π΄ / Ο) β β€ β
(sinβ((π΄ / Ο)
Β· Ο)) = 0) |
177 | 173, 176 | sylan9req 2794 |
. . 3
β’ ((π΄ β β β§ (π΄ / Ο) β β€) β
(sinβπ΄) =
0) |
178 | 177 | ex 414 |
. 2
β’ (π΄ β β β ((π΄ / Ο) β β€ β
(sinβπ΄) =
0)) |
179 | 169, 178 | impbid 211 |
1
β’ (π΄ β β β
((sinβπ΄) = 0 β
(π΄ / Ο) β
β€)) |