Step | Hyp | Ref
| Expression |
1 | | dirkerval2.1 |
. . . . 5
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
2 | 1 | dirkerval 44418 |
. . . 4
β’ (π β β β (π·βπ) = (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
3 | | oveq1 7365 |
. . . . . . 7
β’ (π = π‘ β (π mod (2 Β· Ο)) = (π‘ mod (2 Β· Ο))) |
4 | 3 | eqeq1d 2735 |
. . . . . 6
β’ (π = π‘ β ((π mod (2 Β· Ο)) = 0 β (π‘ mod (2 Β· Ο)) =
0)) |
5 | | oveq2 7366 |
. . . . . . . 8
β’ (π = π‘ β ((π + (1 / 2)) Β· π ) = ((π + (1 / 2)) Β· π‘)) |
6 | 5 | fveq2d 6847 |
. . . . . . 7
β’ (π = π‘ β (sinβ((π + (1 / 2)) Β· π )) = (sinβ((π + (1 / 2)) Β· π‘))) |
7 | | fvoveq1 7381 |
. . . . . . . 8
β’ (π = π‘ β (sinβ(π / 2)) = (sinβ(π‘ / 2))) |
8 | 7 | oveq2d 7374 |
. . . . . . 7
β’ (π = π‘ β ((2 Β· Ο) Β·
(sinβ(π / 2))) = ((2
Β· Ο) Β· (sinβ(π‘ / 2)))) |
9 | 6, 8 | oveq12d 7376 |
. . . . . 6
β’ (π = π‘ β ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2)))) =
((sinβ((π + (1 / 2))
Β· π‘)) / ((2 Β·
Ο) Β· (sinβ(π‘ / 2))))) |
10 | 4, 9 | ifbieq2d 4513 |
. . . . 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)))))) |
11 | 10 | cbvmptv 5219 |
. . . 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)))))) |
12 | 2, 11 | eqtrdi 2789 |
. . 3
β’ (π β β β (π·βπ) = (π‘ β β β¦ if((π‘ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π‘)) / ((2 Β· Ο) Β·
(sinβ(π‘ /
2))))))) |
13 | 12 | adantr 482 |
. 2
β’ ((π β β β§ π β β) β (π·βπ) = (π‘ β β β¦ if((π‘ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π‘)) / ((2 Β· Ο) Β·
(sinβ(π‘ /
2))))))) |
14 | | simpr 486 |
. . . . 5
β’ (((π β β β§ π β β) β§ π‘ = π) β π‘ = π) |
15 | 14 | oveq1d 7373 |
. . . 4
β’ (((π β β β§ π β β) β§ π‘ = π) β (π‘ mod (2 Β· Ο)) = (π mod (2 Β· Ο))) |
16 | 15 | eqeq1d 2735 |
. . 3
β’ (((π β β β§ π β β) β§ π‘ = π) β ((π‘ mod (2 Β· Ο)) = 0 β (π mod (2 Β· Ο)) =
0)) |
17 | 14 | oveq2d 7374 |
. . . . 5
β’ (((π β β β§ π β β) β§ π‘ = π) β ((π + (1 / 2)) Β· π‘) = ((π + (1 / 2)) Β· π)) |
18 | 17 | fveq2d 6847 |
. . . 4
β’ (((π β β β§ π β β) β§ π‘ = π) β (sinβ((π + (1 / 2)) Β· π‘)) = (sinβ((π + (1 / 2)) Β· π))) |
19 | 14 | fvoveq1d 7380 |
. . . . 5
β’ (((π β β β§ π β β) β§ π‘ = π) β (sinβ(π‘ / 2)) = (sinβ(π / 2))) |
20 | 19 | oveq2d 7374 |
. . . 4
β’ (((π β β β§ π β β) β§ π‘ = π) β ((2 Β· Ο) Β·
(sinβ(π‘ / 2))) = ((2
Β· Ο) Β· (sinβ(π / 2)))) |
21 | 18, 20 | oveq12d 7376 |
. . 3
β’ (((π β β β§ π β β) β§ π‘ = π) β ((sinβ((π + (1 / 2)) Β· π‘)) / ((2 Β· Ο) Β·
(sinβ(π‘ / 2)))) =
((sinβ((π + (1 / 2))
Β· π)) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
22 | 16, 21 | ifbieq2d 4513 |
. 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)))))) |
23 | | simpr 486 |
. 2
β’ ((π β β β§ π β β) β π β
β) |
24 | | 2re 12232 |
. . . . . . . 8
β’ 2 β
β |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (π β β β 2 β
β) |
26 | | nnre 12165 |
. . . . . . 7
β’ (π β β β π β
β) |
27 | 25, 26 | remulcld 11190 |
. . . . . 6
β’ (π β β β (2
Β· π) β
β) |
28 | | 1red 11161 |
. . . . . 6
β’ (π β β β 1 β
β) |
29 | 27, 28 | readdcld 11189 |
. . . . 5
β’ (π β β β ((2
Β· π) + 1) β
β) |
30 | | pire 25831 |
. . . . . . 7
β’ Ο
β β |
31 | 30 | a1i 11 |
. . . . . 6
β’ (π β β β Ο
β β) |
32 | 25, 31 | remulcld 11190 |
. . . . 5
β’ (π β β β (2
Β· Ο) β β) |
33 | | 2cnd 12236 |
. . . . . 6
β’ (π β β β 2 β
β) |
34 | 31 | recnd 11188 |
. . . . . 6
β’ (π β β β Ο
β β) |
35 | | 2pos 12261 |
. . . . . . . 8
β’ 0 <
2 |
36 | 35 | a1i 11 |
. . . . . . 7
β’ (π β β β 0 <
2) |
37 | 36 | gt0ne0d 11724 |
. . . . . 6
β’ (π β β β 2 β
0) |
38 | | pipos 25833 |
. . . . . . . 8
β’ 0 <
Ο |
39 | 38 | a1i 11 |
. . . . . . 7
β’ (π β β β 0 <
Ο) |
40 | 39 | gt0ne0d 11724 |
. . . . . 6
β’ (π β β β Ο β
0) |
41 | 33, 34, 37, 40 | mulne0d 11812 |
. . . . 5
β’ (π β β β (2
Β· Ο) β 0) |
42 | 29, 32, 41 | redivcld 11988 |
. . . 4
β’ (π β β β (((2
Β· π) + 1) / (2
Β· Ο)) β β) |
43 | 42 | ad2antrr 725 |
. . 3
β’ (((π β β β§ π β β) β§ (π mod (2 Β· Ο)) = 0)
β (((2 Β· π) +
1) / (2 Β· Ο)) β β) |
44 | | dirker2re 44419 |
. . 3
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((sinβ((π +
(1 / 2)) Β· π)) / ((2
Β· Ο) Β· (sinβ(π / 2)))) β β) |
45 | 43, 44 | ifclda 4522 |
. 2
β’ ((π β β β§ π β β) β
if((π mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π)) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) β β) |
46 | 13, 22, 23, 45 | fvmptd 6956 |
1
β’ ((π β β β§ π β β) β ((π·βπ)βπ) = if((π mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π)) / ((2
Β· Ο) Β· (sinβ(π / 2)))))) |