Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . 7
β’ ((π = π β§ π β β) β π = π) |
2 | 1 | oveq2d 7374 |
. . . . . 6
β’ ((π = π β§ π β β) β (2 Β· π) = (2 Β· π)) |
3 | 2 | oveq1d 7373 |
. . . . 5
β’ ((π = π β§ π β β) β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
4 | 3 | oveq1d 7373 |
. . . 4
β’ ((π = π β§ π β β) β (((2 Β· π) + 1) / (2 Β· Ο)) =
(((2 Β· π) + 1) / (2
Β· Ο))) |
5 | 1 | oveq1d 7373 |
. . . . . 6
β’ ((π = π β§ π β β) β (π + (1 / 2)) = (π + (1 / 2))) |
6 | 5 | fvoveq1d 7380 |
. . . . 5
β’ ((π = π β§ π β β) β (sinβ((π + (1 / 2)) Β· π )) = (sinβ((π + (1 / 2)) Β· π ))) |
7 | 6 | oveq1d 7373 |
. . . 4
β’ ((π = π β§ π β β) β ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
8 | 4, 7 | ifeq12d 4508 |
. . 3
β’ ((π = π β§ π β β) β 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)))))) |
9 | 8 | mpteq2dva 5206 |
. 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))))))) |
10 | | dirkerval.1 |
. . 3
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
11 | | simpl 484 |
. . . . . . . . 9
β’ ((π = π β§ π β β) β π = π) |
12 | 11 | oveq2d 7374 |
. . . . . . . 8
β’ ((π = π β§ π β β) β (2 Β· π) = (2 Β· π)) |
13 | 12 | oveq1d 7373 |
. . . . . . 7
β’ ((π = π β§ π β β) β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
14 | 13 | oveq1d 7373 |
. . . . . 6
β’ ((π = π β§ π β β) β (((2 Β· π) + 1) / (2 Β· Ο)) =
(((2 Β· π) + 1) / (2
Β· Ο))) |
15 | 11 | oveq1d 7373 |
. . . . . . . 8
β’ ((π = π β§ π β β) β (π + (1 / 2)) = (π + (1 / 2))) |
16 | 15 | fvoveq1d 7380 |
. . . . . . 7
β’ ((π = π β§ π β β) β (sinβ((π + (1 / 2)) Β· π )) = (sinβ((π + (1 / 2)) Β· π ))) |
17 | 16 | oveq1d 7373 |
. . . . . 6
β’ ((π = π β§ π β β) β ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
18 | 14, 17 | ifeq12d 4508 |
. . . . 5
β’ ((π = π β§ π β β) β 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)))))) |
19 | 18 | mpteq2dva 5206 |
. . . 4
β’ (π = π β (π β β β¦ 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))))))) |
20 | 19 | cbvmptv 5219 |
. . 3
β’ (π β β β¦ (π β β β¦
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))))))) |
21 | 10, 20 | eqtri 2761 |
. 2
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
22 | | reex 11147 |
. . 3
β’ β
β V |
23 | 22 | mptex 7174 |
. 2
β’ (π β β β¦
if((π mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2)))))) β V |
24 | 9, 21, 23 | fvmpt 6949 |
1
β’ (π β β β (π·βπ) = (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |