Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . 4
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ )) |
2 | 1 | cbvitgv 25157 |
. . 3
β’
β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = β«(π΄(,)π΅)(πΉβπ ) dπ |
3 | 2 | a1i 11 |
. 2
β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = β«(π΄(,)π΅)(πΉβπ ) dπ ) |
4 | | elioore 13301 |
. . . . . 6
β’ (π β (π΄(,)π΅) β π β β) |
5 | 4 | adantl 483 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
6 | | halfre 12374 |
. . . . . . . . 9
β’ (1 / 2)
β β |
7 | 6 | a1i 11 |
. . . . . . . 8
β’ (π β β β (1 / 2)
β β) |
8 | | fzfid 13885 |
. . . . . . . . 9
β’ (π β β β
(1...π) β
Fin) |
9 | | elfzelz 13448 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β π β β€) |
10 | 9 | zred 12614 |
. . . . . . . . . . . 12
β’ (π β (1...π) β π β β) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β β β§ π β (1...π)) β π β β) |
12 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π β β β§ π β (1...π)) β π β β) |
13 | 11, 12 | remulcld 11192 |
. . . . . . . . . 10
β’ ((π β β β§ π β (1...π)) β (π Β· π ) β β) |
14 | 13 | recoscld 16033 |
. . . . . . . . 9
β’ ((π β β β§ π β (1...π)) β (cosβ(π Β· π )) β β) |
15 | 8, 14 | fsumrecl 15626 |
. . . . . . . 8
β’ (π β β β
Ξ£π β (1...π)(cosβ(π Β· π )) β β) |
16 | 7, 15 | readdcld 11191 |
. . . . . . 7
β’ (π β β β ((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) β β) |
17 | | pire 25831 |
. . . . . . . 8
β’ Ο
β β |
18 | 17 | a1i 11 |
. . . . . . 7
β’ (π β β β Ο
β β) |
19 | | pipos 25833 |
. . . . . . . . 9
β’ 0 <
Ο |
20 | 17, 19 | gt0ne0ii 11698 |
. . . . . . . 8
β’ Ο β
0 |
21 | 20 | a1i 11 |
. . . . . . 7
β’ (π β β β Ο β
0) |
22 | 16, 18, 21 | redivcld 11990 |
. . . . . 6
β’ (π β β β (((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) / Ο) β β) |
23 | 5, 22 | syl 17 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο) β β) |
24 | | eqid 2737 |
. . . . . 6
β’ (π β β β¦ (((1 /
2) + Ξ£π β
(1...π)(cosβ(π Β· π ))) / Ο)) = (π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
25 | 24 | fvmpt2 6964 |
. . . . 5
β’ ((π β β β§ (((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) / Ο) β β) β ((π β β β¦ (((1 /
2) + Ξ£π β
(1...π)(cosβ(π Β· π ))) / Ο))βπ ) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
26 | 5, 23, 25 | syl2anc 585 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β ((π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο))βπ ) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
27 | | dirkeritg.d |
. . . . . . . 8
β’ π· = (π β β β¦ (π₯ β β β¦ if((π₯ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ /
2))))))) |
28 | | oveq1 7369 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ mod (2 Β· Ο)) = (π mod (2 Β· Ο))) |
29 | 28 | eqeq1d 2739 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π₯ mod (2 Β· Ο)) = 0 β (π mod (2 Β· Ο)) =
0)) |
30 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((π + (1 / 2)) Β· π₯) = ((π + (1 / 2)) Β· π )) |
31 | 30 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π₯ = π β (sinβ((π + (1 / 2)) Β· π₯)) = (sinβ((π + (1 / 2)) Β· π ))) |
32 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯ / 2) = (π / 2)) |
33 | 32 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (sinβ(π₯ / 2)) = (sinβ(π / 2))) |
34 | 33 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((2 Β· Ο) Β·
(sinβ(π₯ / 2))) = ((2
Β· Ο) Β· (sinβ(π / 2)))) |
35 | 31, 34 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π₯ = π β ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β·
(sinβ(π₯ / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
36 | 29, 35 | ifbieq2d 4517 |
. . . . . . . . . 10
β’ (π₯ = π β 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)))))) |
37 | 36 | cbvmptv 5223 |
. . . . . . . . 9
β’ (π₯ β β β¦
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)))))) |
38 | 37 | mpteq2i 5215 |
. . . . . . . 8
β’ (π β β β¦ (π₯ β β β¦
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))))))) |
39 | 27, 38 | eqtri 2765 |
. . . . . . 7
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
40 | | dirkeritg.n |
. . . . . . 7
β’ (π β π β β) |
41 | | dirkeritg.f |
. . . . . . 7
β’ πΉ = (π·βπ) |
42 | 39, 40, 41, 24 | dirkertrigeq 44416 |
. . . . . 6
β’ (π β πΉ = (π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο))) |
43 | 42 | fveq1d 6849 |
. . . . 5
β’ (π β (πΉβπ ) = ((π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο))βπ )) |
44 | 43 | adantr 482 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβπ ) = ((π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο))βπ )) |
45 | | dirkeritg.g |
. . . . . . . 8
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ (((π₯ / 2) + Ξ£π β (1...π)((sinβ(π Β· π₯)) / π)) / Ο)) |
46 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π Β· π₯) = (π Β· π )) |
47 | 46 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (sinβ(π Β· π₯)) = (sinβ(π Β· π ))) |
48 | 47 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((sinβ(π Β· π₯)) / π) = ((sinβ(π Β· π )) / π)) |
49 | 48 | sumeq2sdv 15596 |
. . . . . . . . . . 11
β’ (π₯ = π β Ξ£π β (1...π)((sinβ(π Β· π₯)) / π) = Ξ£π β (1...π)((sinβ(π Β· π )) / π)) |
50 | 32, 49 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π₯ = π β ((π₯ / 2) + Ξ£π β (1...π)((sinβ(π Β· π₯)) / π)) = ((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π))) |
51 | 50 | oveq1d 7377 |
. . . . . . . . 9
β’ (π₯ = π β (((π₯ / 2) + Ξ£π β (1...π)((sinβ(π Β· π₯)) / π)) / Ο) = (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο)) |
52 | 51 | cbvmptv 5223 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β¦ (((π₯ / 2) + Ξ£π β (1...π)((sinβ(π Β· π₯)) / π)) / Ο)) = (π β (π΄[,]π΅) β¦ (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο)) |
53 | 45, 52 | eqtri 2765 |
. . . . . . 7
β’ πΊ = (π β (π΄[,]π΅) β¦ (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο)) |
54 | 53 | oveq2i 7373 |
. . . . . 6
β’ (β
D πΊ) = (β D (π β (π΄[,]π΅) β¦ (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο))) |
55 | | reelprrecn 11150 |
. . . . . . . 8
β’ β
β {β, β} |
56 | 55 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
57 | | recn 11148 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
58 | 57 | halfcld 12405 |
. . . . . . . . . 10
β’ (π β β β (π / 2) β
β) |
59 | 9 | zcnd 12615 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β π β β) |
60 | 59 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (1...π)) β π β β) |
61 | 57 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (1...π)) β π β β) |
62 | 60, 61 | mulcld 11182 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (1...π)) β (π Β· π ) β β) |
63 | 62 | sincld 16019 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (1...π)) β (sinβ(π Β· π )) β β) |
64 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β 0 β β) |
65 | | 1red 11163 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β 1 β β) |
66 | | 0lt1 11684 |
. . . . . . . . . . . . . . . 16
β’ 0 <
1 |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β 0 < 1) |
68 | | elfzle1 13451 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β 1 β€ π) |
69 | 64, 65, 10, 67, 68 | ltletrd 11322 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β 0 < π) |
70 | 69 | gt0ne0d 11726 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β π β 0) |
71 | 70 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (1...π)) β π β 0) |
72 | 63, 60, 71 | divcld 11938 |
. . . . . . . . . . 11
β’ ((π β β β§ π β (1...π)) β ((sinβ(π Β· π )) / π) β β) |
73 | 8, 72 | fsumcl 15625 |
. . . . . . . . . 10
β’ (π β β β
Ξ£π β (1...π)((sinβ(π Β· π )) / π) β β) |
74 | 58, 73 | addcld 11181 |
. . . . . . . . 9
β’ (π β β β ((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) β β) |
75 | | picn 25832 |
. . . . . . . . . 10
β’ Ο
β β |
76 | 75 | a1i 11 |
. . . . . . . . 9
β’ (π β β β Ο
β β) |
77 | 74, 76, 21 | divcld 11938 |
. . . . . . . 8
β’ (π β β β (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο) β β) |
78 | 77 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β) β (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο) β β) |
79 | 22 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β) β (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο) β β) |
80 | 74 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) β β) |
81 | 16 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β ((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) β β) |
82 | 58 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π / 2) β β) |
83 | 6 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1 / 2) β
β) |
84 | 57 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
85 | | 1red 11163 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 1 β
β) |
86 | 56 | dvmptid 25337 |
. . . . . . . . . 10
β’ (π β (β D (π β β β¦ π )) = (π β β β¦ 1)) |
87 | | 2cnd 12238 |
. . . . . . . . . 10
β’ (π β 2 β
β) |
88 | | 2ne0 12264 |
. . . . . . . . . . 11
β’ 2 β
0 |
89 | 88 | a1i 11 |
. . . . . . . . . 10
β’ (π β 2 β 0) |
90 | 56, 84, 85, 86, 87, 89 | dvmptdivc 25345 |
. . . . . . . . 9
β’ (π β (β D (π β β β¦ (π / 2))) = (π β β β¦ (1 /
2))) |
91 | 73 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β (1...π)((sinβ(π Β· π )) / π) β β) |
92 | 15 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β (1...π)(cosβ(π Β· π )) β β) |
93 | | eqid 2737 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
94 | 93 | tgioo2 24182 |
. . . . . . . . . 10
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
95 | | reopn 43597 |
. . . . . . . . . . 11
β’ β
β (topGenβran (,)) |
96 | 95 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
(topGenβran (,))) |
97 | | fzfid 13885 |
. . . . . . . . . 10
β’ (π β (1...π) β Fin) |
98 | 72 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π β (1...π) β§ π β β) β ((sinβ(π Β· π )) / π) β β) |
99 | 98 | 3adant1 1131 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π) β§ π β β) β ((sinβ(π Β· π )) / π) β β) |
100 | 14 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((π β (1...π) β§ π β β) β (cosβ(π Β· π )) β β) |
101 | 100 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β (1...π) β§ π β β) β (cosβ(π Β· π )) β β) |
102 | 101 | 3adant1 1131 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π) β§ π β β) β (cosβ(π Β· π )) β β) |
103 | 55 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β β β {β,
β}) |
104 | 63 | ancoms 460 |
. . . . . . . . . . . . 13
β’ ((π β (1...π) β§ π β β) β (sinβ(π Β· π )) β β) |
105 | 59 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β (1...π) β§ π β β) β π β β) |
106 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1...π) β§ π β β) β π β β) |
107 | 105, 106 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1...π) β§ π β β) β (π Β· π ) β β) |
108 | 107 | coscld 16020 |
. . . . . . . . . . . . . . 15
β’ ((π β (1...π) β§ π β β) β (cosβ(π Β· π )) β β) |
109 | 105, 108 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ ((π β (1...π) β§ π β β) β (π Β· (cosβ(π Β· π ))) β β) |
110 | 57, 109 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β (1...π) β§ π β β) β (π Β· (cosβ(π Β· π ))) β β) |
111 | | ax-resscn 11115 |
. . . . . . . . . . . . . . . . 17
β’ β
β β |
112 | | resmpt 5996 |
. . . . . . . . . . . . . . . . 17
β’ (β
β β β ((π
β β β¦ (sinβ(π Β· π ))) βΎ β) = (π β β β¦ (sinβ(π Β· π )))) |
113 | 111, 112 | mp1i 13 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β ((π β β β¦ (sinβ(π Β· π ))) βΎ β) = (π β β β¦ (sinβ(π Β· π )))) |
114 | 113 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β (π β β β¦ (sinβ(π Β· π ))) = ((π β β β¦ (sinβ(π Β· π ))) βΎ β)) |
115 | 114 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (β D (π β β β¦ (sinβ(π Β· π )))) = (β D ((π β β β¦ (sinβ(π Β· π ))) βΎ β))) |
116 | 107 | sincld 16019 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1...π) β§ π β β) β (sinβ(π Β· π )) β β) |
117 | 116 | fmpttd 7068 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β (π β β β¦ (sinβ(π Β· π ))):ββΆβ) |
118 | 109 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β βπ β β (π Β· (cosβ(π Β· π ))) β β) |
119 | | dmmptg 6199 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
β (π Β·
(cosβ(π Β·
π ))) β β β
dom (π β β
β¦ (π Β·
(cosβ(π Β·
π )))) =
β) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β dom (π β β β¦ (π Β· (cosβ(π Β· π )))) = β) |
121 | 111, 120 | sseqtrrid 4002 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β β β dom (π β β β¦ (π Β· (cosβ(π Β· π ))))) |
122 | | dvsinax 44228 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (β
D (π β β β¦
(sinβ(π Β·
π )))) = (π β β β¦ (π Β· (cosβ(π Β· π ))))) |
123 | 59, 122 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β (β D (π β β β¦ (sinβ(π Β· π )))) = (π β β β¦ (π Β· (cosβ(π Β· π ))))) |
124 | 123 | dmeqd 5866 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β dom (β D (π β β β¦ (sinβ(π Β· π )))) = dom (π β β β¦ (π Β· (cosβ(π Β· π ))))) |
125 | 121, 124 | sseqtrrd 3990 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β β β dom (β D
(π β β β¦
(sinβ(π Β·
π ))))) |
126 | | dvcnre 44231 |
. . . . . . . . . . . . . . 15
β’ (((π β β β¦
(sinβ(π Β·
π ))):ββΆβ
β§ β β dom (β D (π β β β¦ (sinβ(π Β· π ))))) β (β D ((π β β β¦ (sinβ(π Β· π ))) βΎ β)) = ((β D (π β β β¦
(sinβ(π Β·
π )))) βΎ
β)) |
127 | 117, 125,
126 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (β D ((π β β β¦ (sinβ(π Β· π ))) βΎ β)) = ((β D (π β β β¦
(sinβ(π Β·
π )))) βΎ
β)) |
128 | 123 | reseq1d 5941 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β ((β D (π β β β¦ (sinβ(π Β· π )))) βΎ β) = ((π β β β¦ (π Β· (cosβ(π Β· π )))) βΎ β)) |
129 | | resmpt 5996 |
. . . . . . . . . . . . . . . 16
β’ (β
β β β ((π
β β β¦ (π
Β· (cosβ(π
Β· π )))) βΎ
β) = (π β
β β¦ (π Β·
(cosβ(π Β·
π ))))) |
130 | 111, 129 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((π β β β¦ (π Β· (cosβ(π Β· π )))) βΎ β) = (π β β β¦ (π Β· (cosβ(π Β· π )))) |
131 | 128, 130 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β ((β D (π β β β¦ (sinβ(π Β· π )))) βΎ β) = (π β β β¦ (π Β· (cosβ(π Β· π ))))) |
132 | 115, 127,
131 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β (β D (π β β β¦ (sinβ(π Β· π )))) = (π β β β¦ (π Β· (cosβ(π Β· π ))))) |
133 | 103, 104,
110, 132, 59, 70 | dvmptdivc 25345 |
. . . . . . . . . . . 12
β’ (π β (1...π) β (β D (π β β β¦ ((sinβ(π Β· π )) / π))) = (π β β β¦ ((π Β· (cosβ(π Β· π ))) / π))) |
134 | 59 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β (1...π) β§ π β β) β π β β) |
135 | 70 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β (1...π) β§ π β β) β π β 0) |
136 | 101, 134,
135 | divcan3d 11943 |
. . . . . . . . . . . . 13
β’ ((π β (1...π) β§ π β β) β ((π Β· (cosβ(π Β· π ))) / π) = (cosβ(π Β· π ))) |
137 | 136 | mpteq2dva 5210 |
. . . . . . . . . . . 12
β’ (π β (1...π) β (π β β β¦ ((π Β· (cosβ(π Β· π ))) / π)) = (π β β β¦ (cosβ(π Β· π )))) |
138 | 133, 137 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β (1...π) β (β D (π β β β¦ ((sinβ(π Β· π )) / π))) = (π β β β¦ (cosβ(π Β· π )))) |
139 | 138 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (β D (π β β β¦ ((sinβ(π Β· π )) / π))) = (π β β β¦ (cosβ(π Β· π )))) |
140 | 94, 93, 56, 96, 97, 99, 102, 139 | dvmptfsum 25355 |
. . . . . . . . 9
β’ (π β (β D (π β β β¦
Ξ£π β (1...π)((sinβ(π Β· π )) / π))) = (π β β β¦ Ξ£π β (1...π)(cosβ(π Β· π )))) |
141 | 56, 82, 83, 90, 91, 92, 140 | dvmptadd 25340 |
. . . . . . . 8
β’ (π β (β D (π β β β¦ ((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)))) = (π β β β¦ ((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))))) |
142 | 75 | a1i 11 |
. . . . . . . 8
β’ (π β Ο β
β) |
143 | 20 | a1i 11 |
. . . . . . . 8
β’ (π β Ο β
0) |
144 | 56, 80, 81, 141, 142, 143 | dvmptdivc 25345 |
. . . . . . 7
β’ (π β (β D (π β β β¦ (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο))) = (π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο))) |
145 | | dirkeritg.a |
. . . . . . . 8
β’ (π β π΄ β β) |
146 | | dirkeritg.b |
. . . . . . . 8
β’ (π β π΅ β β) |
147 | 145, 146 | iccssred 13358 |
. . . . . . 7
β’ (π β (π΄[,]π΅) β β) |
148 | | iccntr 24200 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
149 | 145, 146,
148 | syl2anc 585 |
. . . . . . 7
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
150 | 56, 78, 79, 144, 147, 94, 93, 149 | dvmptres2 25342 |
. . . . . 6
β’ (π β (β D (π β (π΄[,]π΅) β¦ (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο))) = (π β (π΄(,)π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο))) |
151 | 54, 150 | eqtrid 2789 |
. . . . 5
β’ (π β (β D πΊ) = (π β (π΄(,)π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο))) |
152 | 151, 23 | fvmpt2d 6966 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β ((β D πΊ)βπ ) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
153 | 26, 44, 152 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβπ ) = ((β D πΊ)βπ )) |
154 | 153 | itgeq2dv 25162 |
. 2
β’ (π β β«(π΄(,)π΅)(πΉβπ ) dπ = β«(π΄(,)π΅)((β D πΊ)βπ ) dπ ) |
155 | | dirkeritg.aleb |
. . 3
β’ (π β π΄ β€ π΅) |
156 | | ioosscn 13333 |
. . . . . . . 8
β’ (π΄(,)π΅) β β |
157 | 156 | a1i 11 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β β) |
158 | | halfcn 12375 |
. . . . . . . 8
β’ (1 / 2)
β β |
159 | 158 | a1i 11 |
. . . . . . 7
β’ (π β (1 / 2) β
β) |
160 | | ssid 3971 |
. . . . . . . 8
β’ β
β β |
161 | 160 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
162 | 157, 159,
161 | constcncfg 44187 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ (1 / 2)) β ((π΄(,)π΅)βcnββ)) |
163 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦
(cosβ(π Β·
π ))) = (π β β β¦ (cosβ(π Β· π ))) |
164 | | coscn 25820 |
. . . . . . . . . . 11
β’ cos
β (ββcnββ) |
165 | 164 | a1i 11 |
. . . . . . . . . 10
β’ (π β (1...π) β cos β (ββcnββ)) |
166 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦ (π Β· π )) = (π β β β¦ (π Β· π )) |
167 | 166 | mulc1cncf 24284 |
. . . . . . . . . . 11
β’ (π β β β (π β β β¦ (π Β· π )) β (ββcnββ)) |
168 | 59, 167 | syl 17 |
. . . . . . . . . 10
β’ (π β (1...π) β (π β β β¦ (π Β· π )) β (ββcnββ)) |
169 | 165, 168 | cncfmpt1f 24293 |
. . . . . . . . 9
β’ (π β (1...π) β (π β β β¦ (cosβ(π Β· π ))) β (ββcnββ)) |
170 | 156 | a1i 11 |
. . . . . . . . 9
β’ (π β (1...π) β (π΄(,)π΅) β β) |
171 | 160 | a1i 11 |
. . . . . . . . 9
β’ (π β (1...π) β β β
β) |
172 | 4, 101 | sylan2 594 |
. . . . . . . . 9
β’ ((π β (1...π) β§ π β (π΄(,)π΅)) β (cosβ(π Β· π )) β β) |
173 | 163, 169,
170, 171, 172 | cncfmptssg 44186 |
. . . . . . . 8
β’ (π β (1...π) β (π β (π΄(,)π΅) β¦ (cosβ(π Β· π ))) β ((π΄(,)π΅)βcnββ)) |
174 | 173 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (π β (π΄(,)π΅) β¦ (cosβ(π Β· π ))) β ((π΄(,)π΅)βcnββ)) |
175 | 157, 97, 174 | fsumcncf 44193 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ Ξ£π β (1...π)(cosβ(π Β· π ))) β ((π΄(,)π΅)βcnββ)) |
176 | 162, 175 | addcncf 24824 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β¦ ((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π )))) β ((π΄(,)π΅)βcnββ)) |
177 | | eqid 2737 |
. . . . . 6
β’ (π β β β¦ Ο) =
(π β β β¦
Ο) |
178 | | cncfmptc 24291 |
. . . . . . . 8
β’ ((Ο
β β β§ β β β β§ β β β)
β (π β β
β¦ Ο) β (ββcnββ)) |
179 | 75, 160, 160, 178 | mp3an 1462 |
. . . . . . 7
β’ (π β β β¦ Ο)
β (ββcnββ) |
180 | 179 | a1i 11 |
. . . . . 6
β’ (π β (π β β β¦ Ο) β
(ββcnββ)) |
181 | | difssd 4097 |
. . . . . 6
β’ (π β (β β {0})
β β) |
182 | | eldifsn 4752 |
. . . . . . . 8
β’ (Ο
β (β β {0}) β (Ο β β β§ Ο β
0)) |
183 | 75, 20, 182 | mpbir2an 710 |
. . . . . . 7
β’ Ο
β (β β {0}) |
184 | 183 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β Ο β (β β
{0})) |
185 | 177, 180,
157, 181, 184 | cncfmptssg 44186 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β¦ Ο) β ((π΄(,)π΅)βcnβ(β β {0}))) |
186 | 176, 185 | divcncf 24827 |
. . . 4
β’ (π β (π β (π΄(,)π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β ((π΄(,)π΅)βcnββ)) |
187 | 151, 186 | eqeltrd 2838 |
. . 3
β’ (π β (β D πΊ) β ((π΄(,)π΅)βcnββ)) |
188 | | ioossicc 13357 |
. . . . . 6
β’ (π΄(,)π΅) β (π΄[,]π΅) |
189 | 188 | a1i 11 |
. . . . 5
β’ (π β (π΄(,)π΅) β (π΄[,]π΅)) |
190 | | ioombl 24945 |
. . . . . 6
β’ (π΄(,)π΅) β dom vol |
191 | 190 | a1i 11 |
. . . . 5
β’ (π β (π΄(,)π΅) β dom vol) |
192 | 6 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π΄[,]π΅)) β (1 / 2) β
β) |
193 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ π β (π΄[,]π΅)) β (1...π) β Fin) |
194 | 10 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄[,]π΅)) β§ π β (1...π)) β π β β) |
195 | 147 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄[,]π΅)) β π β β) |
196 | 195 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄[,]π΅)) β§ π β (1...π)) β π β β) |
197 | 194, 196 | remulcld 11192 |
. . . . . . . . 9
β’ (((π β§ π β (π΄[,]π΅)) β§ π β (1...π)) β (π Β· π ) β β) |
198 | 197 | recoscld 16033 |
. . . . . . . 8
β’ (((π β§ π β (π΄[,]π΅)) β§ π β (1...π)) β (cosβ(π Β· π )) β β) |
199 | 193, 198 | fsumrecl 15626 |
. . . . . . 7
β’ ((π β§ π β (π΄[,]π΅)) β Ξ£π β (1...π)(cosβ(π Β· π )) β β) |
200 | 192, 199 | readdcld 11191 |
. . . . . 6
β’ ((π β§ π β (π΄[,]π΅)) β ((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) β β) |
201 | 17 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (π΄[,]π΅)) β Ο β
β) |
202 | 20 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (π΄[,]π΅)) β Ο β 0) |
203 | 200, 201,
202 | redivcld 11990 |
. . . . 5
β’ ((π β§ π β (π΄[,]π΅)) β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο) β β) |
204 | 147, 111 | sstrdi 3961 |
. . . . . . . . 9
β’ (π β (π΄[,]π΅) β β) |
205 | 204, 159,
161 | constcncfg 44187 |
. . . . . . . 8
β’ (π β (π β (π΄[,]π΅) β¦ (1 / 2)) β ((π΄[,]π΅)βcnββ)) |
206 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦
Ξ£π β (1...π)(cosβ(π Β· π ))) = (π β β β¦ Ξ£π β (1...π)(cosβ(π Β· π ))) |
207 | 169 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (π β β β¦ (cosβ(π Β· π ))) β (ββcnββ)) |
208 | 161, 97, 207 | fsumcncf 44193 |
. . . . . . . . 9
β’ (π β (π β β β¦ Ξ£π β (1...π)(cosβ(π Β· π ))) β (ββcnββ)) |
209 | 199 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π β (π΄[,]π΅)) β Ξ£π β (1...π)(cosβ(π Β· π )) β β) |
210 | 206, 208,
204, 161, 209 | cncfmptssg 44186 |
. . . . . . . 8
β’ (π β (π β (π΄[,]π΅) β¦ Ξ£π β (1...π)(cosβ(π Β· π ))) β ((π΄[,]π΅)βcnββ)) |
211 | 205, 210 | addcncf 24824 |
. . . . . . 7
β’ (π β (π β (π΄[,]π΅) β¦ ((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π )))) β ((π΄[,]π΅)βcnββ)) |
212 | 183 | a1i 11 |
. . . . . . . 8
β’ (π β Ο β (β
β {0})) |
213 | 204, 212,
181 | constcncfg 44187 |
. . . . . . 7
β’ (π β (π β (π΄[,]π΅) β¦ Ο) β ((π΄[,]π΅)βcnβ(β β {0}))) |
214 | 211, 213 | divcncf 24827 |
. . . . . 6
β’ (π β (π β (π΄[,]π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β ((π΄[,]π΅)βcnββ)) |
215 | | cniccibl 25221 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β β§ (π β (π΄[,]π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β ((π΄[,]π΅)βcnββ)) β (π β (π΄[,]π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β
πΏ1) |
216 | 145, 146,
214, 215 | syl3anc 1372 |
. . . . 5
β’ (π β (π β (π΄[,]π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β
πΏ1) |
217 | 189, 191,
203, 216 | iblss 25185 |
. . . 4
β’ (π β (π β (π΄(,)π΅) β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β
πΏ1) |
218 | 151, 217 | eqeltrd 2838 |
. . 3
β’ (π β (β D πΊ) β
πΏ1) |
219 | 204, 161 | idcncfg 44188 |
. . . . . . 7
β’ (π β (π β (π΄[,]π΅) β¦ π ) β ((π΄[,]π΅)βcnββ)) |
220 | | 2cn 12235 |
. . . . . . . . . 10
β’ 2 β
β |
221 | | eldifsn 4752 |
. . . . . . . . . 10
β’ (2 β
(β β {0}) β (2 β β β§ 2 β
0)) |
222 | 220, 88, 221 | mpbir2an 710 |
. . . . . . . . 9
β’ 2 β
(β β {0}) |
223 | 222 | a1i 11 |
. . . . . . . 8
β’ (π β 2 β (β β
{0})) |
224 | 204, 223,
181 | constcncfg 44187 |
. . . . . . 7
β’ (π β (π β (π΄[,]π΅) β¦ 2) β ((π΄[,]π΅)βcnβ(β β {0}))) |
225 | 219, 224 | divcncf 24827 |
. . . . . 6
β’ (π β (π β (π΄[,]π΅) β¦ (π / 2)) β ((π΄[,]π΅)βcnββ)) |
226 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦
(sinβ(π Β·
π ))) = (π β β β¦ (sinβ(π Β· π ))) |
227 | | sincn 25819 |
. . . . . . . . . . . 12
β’ sin
β (ββcnββ) |
228 | 227 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (1...π) β sin β (ββcnββ)) |
229 | 228, 168 | cncfmpt1f 24293 |
. . . . . . . . . 10
β’ (π β (1...π) β (π β β β¦ (sinβ(π Β· π ))) β (ββcnββ)) |
230 | 229 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (π β β β¦ (sinβ(π Β· π ))) β (ββcnββ)) |
231 | 204 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (π΄[,]π΅) β β) |
232 | 160 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β β β
β) |
233 | 59 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β (π΄[,]π΅)) β π β β) |
234 | 195 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄[,]π΅)) β π β β) |
235 | 234 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β (π΄[,]π΅)) β π β β) |
236 | 233, 235 | mulcld 11182 |
. . . . . . . . . 10
β’ (((π β§ π β (1...π)) β§ π β (π΄[,]π΅)) β (π Β· π ) β β) |
237 | 236 | sincld 16019 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π β (π΄[,]π΅)) β (sinβ(π Β· π )) β β) |
238 | 226, 230,
231, 232, 237 | cncfmptssg 44186 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (π β (π΄[,]π΅) β¦ (sinβ(π Β· π ))) β ((π΄[,]π΅)βcnββ)) |
239 | | eldifsn 4752 |
. . . . . . . . . . 11
β’ (π β (β β {0})
β (π β β
β§ π β
0)) |
240 | 59, 70, 239 | sylanbrc 584 |
. . . . . . . . . 10
β’ (π β (1...π) β π β (β β
{0})) |
241 | 240 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β π β (β β
{0})) |
242 | | difssd 4097 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (β β {0}) β
β) |
243 | 231, 241,
242 | constcncfg 44187 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (π β (π΄[,]π΅) β¦ π) β ((π΄[,]π΅)βcnβ(β β {0}))) |
244 | 238, 243 | divcncf 24827 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (π β (π΄[,]π΅) β¦ ((sinβ(π Β· π )) / π)) β ((π΄[,]π΅)βcnββ)) |
245 | 204, 97, 244 | fsumcncf 44193 |
. . . . . 6
β’ (π β (π β (π΄[,]π΅) β¦ Ξ£π β (1...π)((sinβ(π Β· π )) / π)) β ((π΄[,]π΅)βcnββ)) |
246 | 225, 245 | addcncf 24824 |
. . . . 5
β’ (π β (π β (π΄[,]π΅) β¦ ((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π))) β ((π΄[,]π΅)βcnββ)) |
247 | 246, 213 | divcncf 24827 |
. . . 4
β’ (π β (π β (π΄[,]π΅) β¦ (((π / 2) + Ξ£π β (1...π)((sinβ(π Β· π )) / π)) / Ο)) β ((π΄[,]π΅)βcnββ)) |
248 | 53, 247 | eqeltrid 2842 |
. . 3
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |
249 | 145, 146,
155, 187, 218, 248 | ftc2 25424 |
. 2
β’ (π β β«(π΄(,)π΅)((β D πΊ)βπ ) dπ = ((πΊβπ΅) β (πΊβπ΄))) |
250 | 3, 154, 249 | 3eqtrd 2781 |
1
β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = ((πΊβπ΅) β (πΊβπ΄))) |