Step | Hyp | Ref
| Expression |
1 | | dirkerper.2 |
. . . . . . . . . . . . 13
β’ π = (2 Β·
Ο) |
2 | 1 | eqcomi 2742 |
. . . . . . . . . . . 12
β’ (2
Β· Ο) = π |
3 | 2 | oveq2i 7369 |
. . . . . . . . . . 11
β’ (1
Β· (2 Β· Ο)) = (1 Β· π) |
4 | | 2re 12232 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
5 | | pire 25831 |
. . . . . . . . . . . . . . 15
β’ Ο
β β |
6 | 4, 5 | remulcli 11176 |
. . . . . . . . . . . . . 14
β’ (2
Β· Ο) β β |
7 | 1, 6 | eqeltri 2830 |
. . . . . . . . . . . . 13
β’ π β β |
8 | 7 | recni 11174 |
. . . . . . . . . . . 12
β’ π β β |
9 | 8 | mulid2i 11165 |
. . . . . . . . . . 11
β’ (1
Β· π) = π |
10 | 3, 9 | eqtri 2761 |
. . . . . . . . . 10
β’ (1
Β· (2 Β· Ο)) = π |
11 | 10 | oveq2i 7369 |
. . . . . . . . 9
β’ (π₯ + (1 Β· (2 Β·
Ο))) = (π₯ + π) |
12 | 11 | eqcomi 2742 |
. . . . . . . 8
β’ (π₯ + π) = (π₯ + (1 Β· (2 Β·
Ο))) |
13 | 12 | oveq1i 7368 |
. . . . . . 7
β’ ((π₯ + π) mod (2 Β· Ο)) = ((π₯ + (1 Β· (2 Β·
Ο))) mod (2 Β· Ο)) |
14 | 13 | a1i 11 |
. . . . . 6
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β ((π₯ + π) mod (2 Β· Ο)) =
((π₯ + (1 Β· (2
Β· Ο))) mod (2 Β· Ο))) |
15 | | id 22 |
. . . . . . . 8
β’ (π₯ β β β π₯ β
β) |
16 | 15 | ad2antlr 726 |
. . . . . . 7
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β π₯ β
β) |
17 | | 2rp 12925 |
. . . . . . . . 9
β’ 2 β
β+ |
18 | | pirp 25834 |
. . . . . . . . 9
β’ Ο
β β+ |
19 | | rpmulcl 12943 |
. . . . . . . . 9
β’ ((2
β β+ β§ Ο β β+) β (2
Β· Ο) β β+) |
20 | 17, 18, 19 | mp2an 691 |
. . . . . . . 8
β’ (2
Β· Ο) β β+ |
21 | 20 | a1i 11 |
. . . . . . 7
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β (2 Β· Ο) β β+) |
22 | | 1z 12538 |
. . . . . . . 8
β’ 1 β
β€ |
23 | 22 | a1i 11 |
. . . . . . 7
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β 1 β β€) |
24 | | modcyc 13817 |
. . . . . . 7
β’ ((π₯ β β β§ (2
Β· Ο) β β+ β§ 1 β β€) β
((π₯ + (1 Β· (2
Β· Ο))) mod (2 Β· Ο)) = (π₯ mod (2 Β· Ο))) |
25 | 16, 21, 23, 24 | syl3anc 1372 |
. . . . . 6
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β ((π₯ + (1 Β· (2
Β· Ο))) mod (2 Β· Ο)) = (π₯ mod (2 Β· Ο))) |
26 | | simpr 486 |
. . . . . 6
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β (π₯ mod (2 Β·
Ο)) = 0) |
27 | 14, 25, 26 | 3eqtrd 2777 |
. . . . 5
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β ((π₯ + π) mod (2 Β· Ο)) =
0) |
28 | 27 | iftrued 4495 |
. . . 4
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β if(((π₯ + π) mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· (π₯ + π))) / ((2 Β· Ο) Β·
(sinβ((π₯ + π) / 2))))) = (((2 Β· π) + 1) / (2 Β·
Ο))) |
29 | | iftrue 4493 |
. . . . 5
β’ ((π₯ mod (2 Β· Ο)) = 0
β if((π₯ mod (2
Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π₯)) / ((2 Β·
Ο) Β· (sinβ(π₯ / 2))))) = (((2 Β· π) + 1) / (2 Β·
Ο))) |
30 | 29 | adantl 483 |
. . . 4
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β if((π₯ mod (2
Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π₯)) / ((2 Β·
Ο) Β· (sinβ(π₯ / 2))))) = (((2 Β· π) + 1) / (2 Β·
Ο))) |
31 | 28, 30 | eqtr4d 2776 |
. . 3
β’ (((π β β β§ π₯ β β) β§ (π₯ mod (2 Β· Ο)) = 0)
β if(((π₯ + π) mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· (π₯ + π))) / ((2 Β· Ο) Β·
(sinβ((π₯ + π) / 2))))) = if((π₯ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ /
2)))))) |
32 | | iffalse 4496 |
. . . . 5
β’ (Β¬
(π₯ mod (2 Β· Ο)) =
0 β if((π₯ mod (2
Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π₯)) / ((2 Β·
Ο) Β· (sinβ(π₯ / 2))))) = ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ /
2))))) |
33 | 32 | adantl 483 |
. . . 4
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β if((π₯ mod (2
Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π₯)) / ((2 Β·
Ο) Β· (sinβ(π₯ / 2))))) = ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ /
2))))) |
34 | | nncn 12166 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
35 | | halfcn 12373 |
. . . . . . . . . . 11
β’ (1 / 2)
β β |
36 | 35 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β (1 / 2)
β β) |
37 | 34, 36 | addcld 11179 |
. . . . . . . . 9
β’ (π β β β (π + (1 / 2)) β
β) |
38 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β (π + (1 / 2)) β
β) |
39 | | recn 11146 |
. . . . . . . . 9
β’ (π₯ β β β π₯ β
β) |
40 | 39 | adantl 483 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β π₯ β
β) |
41 | 38, 40 | mulcld 11180 |
. . . . . . 7
β’ ((π β β β§ π₯ β β) β ((π + (1 / 2)) Β· π₯) β
β) |
42 | 41 | sincld 16017 |
. . . . . 6
β’ ((π β β β§ π₯ β β) β
(sinβ((π + (1 / 2))
Β· π₯)) β
β) |
43 | 42 | adantr 482 |
. . . . 5
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β (sinβ((π +
(1 / 2)) Β· π₯))
β β) |
44 | 6 | recni 11174 |
. . . . . . . 8
β’ (2
Β· Ο) β β |
45 | 44 | a1i 11 |
. . . . . . 7
β’ ((π β β β§ π₯ β β) β (2
Β· Ο) β β) |
46 | 40 | halfcld 12403 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β (π₯ / 2) β
β) |
47 | 46 | sincld 16017 |
. . . . . . 7
β’ ((π β β β§ π₯ β β) β
(sinβ(π₯ / 2)) β
β) |
48 | 45, 47 | mulcld 11180 |
. . . . . 6
β’ ((π β β β§ π₯ β β) β ((2
Β· Ο) Β· (sinβ(π₯ / 2))) β β) |
49 | 48 | adantr 482 |
. . . . 5
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β ((2 Β· Ο) Β· (sinβ(π₯ / 2))) β β) |
50 | | dirkerdenne0 44420 |
. . . . . 6
β’ ((π₯ β β β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β ((2 Β· Ο) Β· (sinβ(π₯ / 2))) β 0) |
51 | 50 | adantll 713 |
. . . . 5
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β ((2 Β· Ο) Β· (sinβ(π₯ / 2))) β 0) |
52 | 43, 49, 51 | div2negd 11951 |
. . . 4
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β (-(sinβ((π
+ (1 / 2)) Β· π₯)) /
-((2 Β· Ο) Β· (sinβ(π₯ / 2)))) = ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ /
2))))) |
53 | 13 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β β β ((π₯ + π) mod (2 Β· Ο)) = ((π₯ + (1 Β· (2 Β·
Ο))) mod (2 Β· Ο))) |
54 | 20, 22, 24 | mp3an23 1454 |
. . . . . . . . . . 11
β’ (π₯ β β β ((π₯ + (1 Β· (2 Β·
Ο))) mod (2 Β· Ο)) = (π₯ mod (2 Β· Ο))) |
55 | 53, 54 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π₯ β β β ((π₯ + π) mod (2 Β· Ο)) = (π₯ mod (2 Β·
Ο))) |
56 | 55 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β β β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β ((π₯ + π) mod (2 Β· Ο)) =
(π₯ mod (2 Β·
Ο))) |
57 | | simpr 486 |
. . . . . . . . . 10
β’ ((π₯ β β β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β Β¬ (π₯ mod (2
Β· Ο)) = 0) |
58 | 57 | neqned 2947 |
. . . . . . . . 9
β’ ((π₯ β β β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β (π₯ mod (2
Β· Ο)) β 0) |
59 | 56, 58 | eqnetrd 3008 |
. . . . . . . 8
β’ ((π₯ β β β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β ((π₯ + π) mod (2 Β· Ο)) β
0) |
60 | 59 | neneqd 2945 |
. . . . . . 7
β’ ((π₯ β β β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β Β¬ ((π₯ + π) mod (2 Β· Ο)) =
0) |
61 | | iffalse 4496 |
. . . . . . . 8
β’ (Β¬
((π₯ + π) mod (2 Β· Ο)) = 0 β
if(((π₯ + π) mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· (π₯ +
π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) / 2))))) =
((sinβ((π + (1 / 2))
Β· (π₯ + π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) /
2))))) |
62 | 1 | oveq2i 7369 |
. . . . . . . . . . 11
β’ (π₯ + π) = (π₯ + (2 Β· Ο)) |
63 | 62 | oveq2i 7369 |
. . . . . . . . . 10
β’ ((π + (1 / 2)) Β· (π₯ + π)) = ((π + (1 / 2)) Β· (π₯ + (2 Β· Ο))) |
64 | 63 | fveq2i 6846 |
. . . . . . . . 9
β’
(sinβ((π + (1
/ 2)) Β· (π₯ + π))) = (sinβ((π + (1 / 2)) Β· (π₯ + (2 Β·
Ο)))) |
65 | 62 | oveq1i 7368 |
. . . . . . . . . . 11
β’ ((π₯ + π) / 2) = ((π₯ + (2 Β· Ο)) / 2) |
66 | 65 | fveq2i 6846 |
. . . . . . . . . 10
β’
(sinβ((π₯ +
π) / 2)) =
(sinβ((π₯ + (2
Β· Ο)) / 2)) |
67 | 66 | oveq2i 7369 |
. . . . . . . . 9
β’ ((2
Β· Ο) Β· (sinβ((π₯ + π) / 2))) = ((2 Β· Ο) Β·
(sinβ((π₯ + (2
Β· Ο)) / 2))) |
68 | 64, 67 | oveq12i 7370 |
. . . . . . . 8
β’
((sinβ((π + (1
/ 2)) Β· (π₯ + π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) / 2)))) =
((sinβ((π + (1 / 2))
Β· (π₯ + (2 Β·
Ο)))) / ((2 Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) /
2)))) |
69 | 61, 68 | eqtrdi 2789 |
. . . . . . 7
β’ (Β¬
((π₯ + π) mod (2 Β· Ο)) = 0 β
if(((π₯ + π) mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· (π₯ +
π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) / 2))))) =
((sinβ((π + (1 / 2))
Β· (π₯ + (2 Β·
Ο)))) / ((2 Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) /
2))))) |
70 | 60, 69 | syl 17 |
. . . . . 6
β’ ((π₯ β β β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β if(((π₯ + π) mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· (π₯ + π))) / ((2 Β· Ο) Β·
(sinβ((π₯ + π) / 2))))) = ((sinβ((π + (1 / 2)) Β· (π₯ + (2 Β· Ο)))) / ((2
Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) /
2))))) |
71 | 70 | adantll 713 |
. . . . 5
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β if(((π₯ + π) mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· (π₯ + π))) / ((2 Β· Ο) Β·
(sinβ((π₯ + π) / 2))))) = ((sinβ((π + (1 / 2)) Β· (π₯ + (2 Β· Ο)))) / ((2
Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) /
2))))) |
72 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β (2
Β· Ο) β β) |
73 | 34, 36, 72 | adddird 11185 |
. . . . . . . . . . . . 13
β’ (π β β β ((π + (1 / 2)) Β· (2 Β·
Ο)) = ((π Β· (2
Β· Ο)) + ((1 / 2) Β· (2 Β· Ο)))) |
74 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
75 | | 2cnne0 12368 |
. . . . . . . . . . . . . . . 16
β’ (2 β
β β§ 2 β 0) |
76 | | 2cn 12233 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
77 | | picn 25832 |
. . . . . . . . . . . . . . . . 17
β’ Ο
β β |
78 | 76, 77 | mulcli 11167 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· Ο) β β |
79 | | div32 11838 |
. . . . . . . . . . . . . . . 16
β’ ((1
β β β§ (2 β β β§ 2 β 0) β§ (2 Β· Ο)
β β) β ((1 / 2) Β· (2 Β· Ο)) = (1 Β· ((2
Β· Ο) / 2))) |
80 | 74, 75, 78, 79 | mp3an 1462 |
. . . . . . . . . . . . . . 15
β’ ((1 / 2)
Β· (2 Β· Ο)) = (1 Β· ((2 Β· Ο) /
2)) |
81 | | 2ne0 12262 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
0 |
82 | 78, 76, 81 | divcli 11902 |
. . . . . . . . . . . . . . . . 17
β’ ((2
Β· Ο) / 2) β β |
83 | 82 | mulid2i 11165 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· ((2 Β· Ο) / 2)) = ((2 Β· Ο) / 2) |
84 | 77, 76, 81 | divcan3i 11906 |
. . . . . . . . . . . . . . . 16
β’ ((2
Β· Ο) / 2) = Ο |
85 | 83, 84 | eqtri 2761 |
. . . . . . . . . . . . . . 15
β’ (1
Β· ((2 Β· Ο) / 2)) = Ο |
86 | 80, 85 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’ ((1 / 2)
Β· (2 Β· Ο)) = Ο |
87 | 86 | oveq2i 7369 |
. . . . . . . . . . . . 13
β’ ((π Β· (2 Β· Ο)) +
((1 / 2) Β· (2 Β· Ο))) = ((π Β· (2 Β· Ο)) +
Ο) |
88 | 73, 87 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π β β β ((π + (1 / 2)) Β· (2 Β·
Ο)) = ((π Β· (2
Β· Ο)) + Ο)) |
89 | 88 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π β β β (((π + (1 / 2)) Β· π₯) + ((π + (1 / 2)) Β· (2 Β· Ο))) =
(((π + (1 / 2)) Β·
π₯) + ((π Β· (2 Β· Ο)) +
Ο))) |
90 | 89 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β β§ π₯ β β) β (((π + (1 / 2)) Β· π₯) + ((π + (1 / 2)) Β· (2 Β· Ο))) =
(((π + (1 / 2)) Β·
π₯) + ((π Β· (2 Β· Ο)) +
Ο))) |
91 | 38, 40, 45 | adddid 11184 |
. . . . . . . . . 10
β’ ((π β β β§ π₯ β β) β ((π + (1 / 2)) Β· (π₯ + (2 Β· Ο))) =
(((π + (1 / 2)) Β·
π₯) + ((π + (1 / 2)) Β· (2 Β·
Ο)))) |
92 | 34, 72 | mulcld 11180 |
. . . . . . . . . . . 12
β’ (π β β β (π Β· (2 Β· Ο))
β β) |
93 | 92 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β β§ π₯ β β) β (π Β· (2 Β· Ο))
β β) |
94 | 77 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β β β§ π₯ β β) β Ο
β β) |
95 | 41, 93, 94 | addassd 11182 |
. . . . . . . . . 10
β’ ((π β β β§ π₯ β β) β
((((π + (1 / 2)) Β·
π₯) + (π Β· (2 Β· Ο))) + Ο) =
(((π + (1 / 2)) Β·
π₯) + ((π Β· (2 Β· Ο)) +
Ο))) |
96 | 90, 91, 95 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β β) β ((π + (1 / 2)) Β· (π₯ + (2 Β· Ο))) =
((((π + (1 / 2)) Β·
π₯) + (π Β· (2 Β· Ο))) +
Ο)) |
97 | 96 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β
(sinβ((π + (1 / 2))
Β· (π₯ + (2 Β·
Ο)))) = (sinβ((((π
+ (1 / 2)) Β· π₯) +
(π Β· (2 Β·
Ο))) + Ο))) |
98 | 41, 93 | addcld 11179 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β β) β (((π + (1 / 2)) Β· π₯) + (π Β· (2 Β· Ο))) β
β) |
99 | | sinppi 25862 |
. . . . . . . . 9
β’ ((((π + (1 / 2)) Β· π₯) + (π Β· (2 Β· Ο))) β β
β (sinβ((((π +
(1 / 2)) Β· π₯) +
(π Β· (2 Β·
Ο))) + Ο)) = -(sinβ(((π + (1 / 2)) Β· π₯) + (π Β· (2 Β·
Ο))))) |
100 | 98, 99 | syl 17 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β
(sinβ((((π + (1 / 2))
Β· π₯) + (π Β· (2 Β· Ο))) +
Ο)) = -(sinβ(((π +
(1 / 2)) Β· π₯) +
(π Β· (2 Β·
Ο))))) |
101 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π β β β§ π₯ β β) β π β
β) |
102 | 101 | nnzd 12531 |
. . . . . . . . . 10
β’ ((π β β β§ π₯ β β) β π β
β€) |
103 | | sinper 25854 |
. . . . . . . . . 10
β’ ((((π + (1 / 2)) Β· π₯) β β β§ π β β€) β
(sinβ(((π + (1 / 2))
Β· π₯) + (π Β· (2 Β· Ο)))) =
(sinβ((π + (1 / 2))
Β· π₯))) |
104 | 41, 102, 103 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β β) β
(sinβ(((π + (1 / 2))
Β· π₯) + (π Β· (2 Β· Ο)))) =
(sinβ((π + (1 / 2))
Β· π₯))) |
105 | 104 | negeqd 11400 |
. . . . . . . 8
β’ ((π β β β§ π₯ β β) β
-(sinβ(((π + (1 / 2))
Β· π₯) + (π Β· (2 Β· Ο)))) =
-(sinβ((π + (1 / 2))
Β· π₯))) |
106 | 97, 100, 105 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π β β β§ π₯ β β) β
(sinβ((π + (1 / 2))
Β· (π₯ + (2 Β·
Ο)))) = -(sinβ((π
+ (1 / 2)) Β· π₯))) |
107 | 44 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (2
Β· Ο) β β) |
108 | 76 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β 2 β
β) |
109 | 81 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β 2 β
0) |
110 | 39, 107, 108, 109 | divdird 11974 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((π₯ + (2 Β· Ο)) / 2) =
((π₯ / 2) + ((2 Β·
Ο) / 2))) |
111 | 84 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((2
Β· Ο) / 2) = Ο) |
112 | 111 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((π₯ / 2) + ((2 Β· Ο) / 2))
= ((π₯ / 2) +
Ο)) |
113 | 110, 112 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π₯ β β β ((π₯ + (2 Β· Ο)) / 2) =
((π₯ / 2) +
Ο)) |
114 | 113 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π₯ β β β
(sinβ((π₯ + (2
Β· Ο)) / 2)) = (sinβ((π₯ / 2) + Ο))) |
115 | 39 | halfcld 12403 |
. . . . . . . . . . 11
β’ (π₯ β β β (π₯ / 2) β
β) |
116 | | sinppi 25862 |
. . . . . . . . . . 11
β’ ((π₯ / 2) β β β
(sinβ((π₯ / 2) +
Ο)) = -(sinβ(π₯ /
2))) |
117 | 115, 116 | syl 17 |
. . . . . . . . . 10
β’ (π₯ β β β
(sinβ((π₯ / 2) +
Ο)) = -(sinβ(π₯ /
2))) |
118 | 114, 117 | eqtrd 2773 |
. . . . . . . . 9
β’ (π₯ β β β
(sinβ((π₯ + (2
Β· Ο)) / 2)) = -(sinβ(π₯ / 2))) |
119 | 118 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ β β β ((2
Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) / 2))) = ((2 Β·
Ο) Β· -(sinβ(π₯ / 2)))) |
120 | 119 | adantl 483 |
. . . . . . 7
β’ ((π β β β§ π₯ β β) β ((2
Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) / 2))) = ((2 Β·
Ο) Β· -(sinβ(π₯ / 2)))) |
121 | 106, 120 | oveq12d 7376 |
. . . . . 6
β’ ((π β β β§ π₯ β β) β
((sinβ((π + (1 / 2))
Β· (π₯ + (2 Β·
Ο)))) / ((2 Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) / 2)))) =
(-(sinβ((π + (1 / 2))
Β· π₯)) / ((2 Β·
Ο) Β· -(sinβ(π₯ / 2))))) |
122 | 121 | adantr 482 |
. . . . 5
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β ((sinβ((π +
(1 / 2)) Β· (π₯ + (2
Β· Ο)))) / ((2 Β· Ο) Β· (sinβ((π₯ + (2 Β· Ο)) / 2)))) =
(-(sinβ((π + (1 / 2))
Β· π₯)) / ((2 Β·
Ο) Β· -(sinβ(π₯ / 2))))) |
123 | 115 | sincld 16017 |
. . . . . . . 8
β’ (π₯ β β β
(sinβ(π₯ / 2)) β
β) |
124 | 107, 123 | mulneg2d 11614 |
. . . . . . 7
β’ (π₯ β β β ((2
Β· Ο) Β· -(sinβ(π₯ / 2))) = -((2 Β· Ο) Β·
(sinβ(π₯ /
2)))) |
125 | 124 | oveq2d 7374 |
. . . . . 6
β’ (π₯ β β β
(-(sinβ((π + (1 / 2))
Β· π₯)) / ((2 Β·
Ο) Β· -(sinβ(π₯ / 2)))) = (-(sinβ((π + (1 / 2)) Β· π₯)) / -((2 Β· Ο) Β·
(sinβ(π₯ /
2))))) |
126 | 125 | ad2antlr 726 |
. . . . 5
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β (-(sinβ((π
+ (1 / 2)) Β· π₯)) /
((2 Β· Ο) Β· -(sinβ(π₯ / 2)))) = (-(sinβ((π + (1 / 2)) Β· π₯)) / -((2 Β· Ο) Β·
(sinβ(π₯ /
2))))) |
127 | 71, 122, 126 | 3eqtrrd 2778 |
. . . 4
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β (-(sinβ((π
+ (1 / 2)) Β· π₯)) /
-((2 Β· Ο) Β· (sinβ(π₯ / 2)))) = if(((π₯ + π) mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· (π₯ +
π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) /
2)))))) |
128 | 33, 52, 127 | 3eqtr2rd 2780 |
. . 3
β’ (((π β β β§ π₯ β β) β§ Β¬
(π₯ mod (2 Β· Ο)) =
0) β if(((π₯ + π) mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· (π₯ + π))) / ((2 Β· Ο) Β·
(sinβ((π₯ + π) / 2))))) = if((π₯ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ /
2)))))) |
129 | 31, 128 | pm2.61dan 812 |
. 2
β’ ((π β β β§ π₯ β β) β
if(((π₯ + π) mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· (π₯ +
π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) / 2))))) = if((π₯ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ /
2)))))) |
130 | 7 | a1i 11 |
. . . 4
β’ (π₯ β β β π β
β) |
131 | 15, 130 | readdcld 11189 |
. . 3
β’ (π₯ β β β (π₯ + π) β β) |
132 | | dirkerper.1 |
. . . 4
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
133 | 132 | dirkerval2 44421 |
. . 3
β’ ((π β β β§ (π₯ + π) β β) β ((π·βπ)β(π₯ + π)) = if(((π₯ + π) mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· (π₯ +
π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) /
2)))))) |
134 | 131, 133 | sylan2 594 |
. 2
β’ ((π β β β§ π₯ β β) β ((π·βπ)β(π₯ + π)) = if(((π₯ + π) mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· (π₯ +
π))) / ((2 Β· Ο)
Β· (sinβ((π₯ +
π) /
2)))))) |
135 | 132 | dirkerval2 44421 |
. 2
β’ ((π β β β§ π₯ β β) β ((π·βπ)βπ₯) = if((π₯ mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π₯)) / ((2
Β· Ο) Β· (sinβ(π₯ / 2)))))) |
136 | 129, 134,
135 | 3eqtr4d 2783 |
1
β’ ((π β β β§ π₯ β β) β ((π·βπ)β(π₯ + π)) = ((π·βπ)βπ₯)) |