Step | Hyp | Ref
| Expression |
1 | | itgsin0pilem1.1 |
. . . . . . . . . . 11
β’ πΆ = (π‘ β (0[,]Ο) β¦ -(cosβπ‘)) |
2 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π‘ = π₯ β (cosβπ‘) = (cosβπ₯)) |
3 | 2 | negeqd 11454 |
. . . . . . . . . . . 12
β’ (π‘ = π₯ β -(cosβπ‘) = -(cosβπ₯)) |
4 | 3 | cbvmptv 5262 |
. . . . . . . . . . 11
β’ (π‘ β (0[,]Ο) β¦
-(cosβπ‘)) = (π₯ β (0[,]Ο) β¦
-(cosβπ₯)) |
5 | 1, 4 | eqtri 2761 |
. . . . . . . . . 10
β’ πΆ = (π₯ β (0[,]Ο) β¦ -(cosβπ₯)) |
6 | 5 | oveq2i 7420 |
. . . . . . . . 9
β’ (β
D πΆ) = (β D (π₯ β (0[,]Ο) β¦
-(cosβπ₯))) |
7 | | ax-resscn 11167 |
. . . . . . . . . . . 12
β’ β
β β |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β β β β) |
9 | | 0re 11216 |
. . . . . . . . . . . . 13
β’ 0 β
β |
10 | | pire 25968 |
. . . . . . . . . . . . 13
β’ Ο
β β |
11 | | iccssre 13406 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ Ο β β) β (0[,]Ο) β
β) |
12 | 9, 10, 11 | mp2an 691 |
. . . . . . . . . . . 12
β’
(0[,]Ο) β β |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (0[,]Ο) β β) |
14 | 12, 7 | sstri 3992 |
. . . . . . . . . . . . . . 15
β’
(0[,]Ο) β β |
15 | 14 | sseli 3979 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0[,]Ο) β π₯ β
β) |
16 | 15 | coscld 16074 |
. . . . . . . . . . . . 13
β’ (π₯ β (0[,]Ο) β
(cosβπ₯) β
β) |
17 | 16 | adantl 483 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (0[,]Ο)) β (cosβπ₯) β β) |
18 | 17 | negcld 11558 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (0[,]Ο)) β -(cosβπ₯) β β) |
19 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(TopOpenββfld) =
(TopOpenββfld) |
20 | 19 | tgioo2 24319 |
. . . . . . . . . . 11
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
21 | | iccntr 24337 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ Ο β β) β ((intβ(topGenβran
(,)))β(0[,]Ο)) = (0(,)Ο)) |
22 | 9, 10, 21 | mp2an 691 |
. . . . . . . . . . . 12
β’
((intβ(topGenβran (,)))β(0[,]Ο)) =
(0(,)Ο) |
23 | 22 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β ((intβ(topGenβran (,)))β(0[,]Ο)) =
(0(,)Ο)) |
24 | 8, 13, 18, 20, 19, 23 | dvmptntr 25488 |
. . . . . . . . . 10
β’ (β€
β (β D (π₯ β
(0[,]Ο) β¦ -(cosβπ₯))) = (β D (π₯ β (0(,)Ο) β¦ -(cosβπ₯)))) |
25 | 24 | mptru 1549 |
. . . . . . . . 9
β’ (β
D (π₯ β (0[,]Ο)
β¦ -(cosβπ₯))) =
(β D (π₯ β
(0(,)Ο) β¦ -(cosβπ₯))) |
26 | | reelprrecn 11202 |
. . . . . . . . . . . 12
β’ β
β {β, β} |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β β β {β, β}) |
28 | | recn 11200 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β π₯ β
β) |
29 | 28 | coscld 16074 |
. . . . . . . . . . . . 13
β’ (π₯ β β β
(cosβπ₯) β
β) |
30 | 29 | adantl 483 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β β) β (cosβπ₯) β β) |
31 | 30 | negcld 11558 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β β) β -(cosβπ₯) β β) |
32 | 28 | sincld 16073 |
. . . . . . . . . . . 12
β’ (π₯ β β β
(sinβπ₯) β
β) |
33 | 32 | adantl 483 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β β) β (sinβπ₯) β β) |
34 | 32 | negcld 11558 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β
-(sinβπ₯) β
β) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β β) β -(sinβπ₯) β β) |
36 | | dvcosre 44628 |
. . . . . . . . . . . . . 14
β’ (β
D (π₯ β β β¦
(cosβπ₯))) = (π₯ β β β¦
-(sinβπ₯)) |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β (β D (π₯ β
β β¦ (cosβπ₯))) = (π₯ β β β¦ -(sinβπ₯))) |
38 | 27, 30, 35, 37 | dvmptneg 25483 |
. . . . . . . . . . . 12
β’ (β€
β (β D (π₯ β
β β¦ -(cosβπ₯))) = (π₯ β β β¦ --(sinβπ₯))) |
39 | 32 | negnegd 11562 |
. . . . . . . . . . . . 13
β’ (π₯ β β β
--(sinβπ₯) =
(sinβπ₯)) |
40 | 39 | mpteq2ia 5252 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦
--(sinβπ₯)) = (π₯ β β β¦
(sinβπ₯)) |
41 | 38, 40 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (β€
β (β D (π₯ β
β β¦ -(cosβπ₯))) = (π₯ β β β¦ (sinβπ₯))) |
42 | | ioossre 13385 |
. . . . . . . . . . . 12
β’
(0(,)Ο) β β |
43 | 42 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (0(,)Ο) β β) |
44 | | iooretop 24282 |
. . . . . . . . . . . 12
β’
(0(,)Ο) β (topGenβran (,)) |
45 | 44 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (0(,)Ο) β (topGenβran (,))) |
46 | 27, 31, 33, 41, 43, 20, 19, 45 | dvmptres 25480 |
. . . . . . . . . 10
β’ (β€
β (β D (π₯ β
(0(,)Ο) β¦ -(cosβπ₯))) = (π₯ β (0(,)Ο) β¦ (sinβπ₯))) |
47 | 46 | mptru 1549 |
. . . . . . . . 9
β’ (β
D (π₯ β (0(,)Ο)
β¦ -(cosβπ₯))) =
(π₯ β (0(,)Ο)
β¦ (sinβπ₯)) |
48 | 6, 25, 47 | 3eqtri 2765 |
. . . . . . . 8
β’ (β
D πΆ) = (π₯ β (0(,)Ο) β¦ (sinβπ₯)) |
49 | 48 | fveq1i 6893 |
. . . . . . 7
β’ ((β
D πΆ)βπ₯) = ((π₯ β (0(,)Ο) β¦ (sinβπ₯))βπ₯) |
50 | 42, 7 | sstri 3992 |
. . . . . . . . . 10
β’
(0(,)Ο) β β |
51 | 50 | sseli 3979 |
. . . . . . . . 9
β’ (π₯ β (0(,)Ο) β π₯ β
β) |
52 | 51 | sincld 16073 |
. . . . . . . 8
β’ (π₯ β (0(,)Ο) β
(sinβπ₯) β
β) |
53 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β (0(,)Ο) β¦
(sinβπ₯)) = (π₯ β (0(,)Ο) β¦
(sinβπ₯)) |
54 | 53 | fvmpt2 7010 |
. . . . . . . 8
β’ ((π₯ β (0(,)Ο) β§
(sinβπ₯) β
β) β ((π₯ β
(0(,)Ο) β¦ (sinβπ₯))βπ₯) = (sinβπ₯)) |
55 | 52, 54 | mpdan 686 |
. . . . . . 7
β’ (π₯ β (0(,)Ο) β
((π₯ β (0(,)Ο)
β¦ (sinβπ₯))βπ₯) = (sinβπ₯)) |
56 | 49, 55 | eqtrid 2785 |
. . . . . 6
β’ (π₯ β (0(,)Ο) β
((β D πΆ)βπ₯) = (sinβπ₯)) |
57 | 56 | adantl 483 |
. . . . 5
β’
((β€ β§ π₯
β (0(,)Ο)) β ((β D πΆ)βπ₯) = (sinβπ₯)) |
58 | 57 | itgeq2dv 25299 |
. . . 4
β’ (β€
β β«(0(,)Ο)((β D πΆ)βπ₯) dπ₯ = β«(0(,)Ο)(sinβπ₯) dπ₯) |
59 | 58 | mptru 1549 |
. . 3
β’
β«(0(,)Ο)((β D πΆ)βπ₯) dπ₯ = β«(0(,)Ο)(sinβπ₯) dπ₯ |
60 | 9 | a1i 11 |
. . . . 5
β’ (β€
β 0 β β) |
61 | 10 | a1i 11 |
. . . . 5
β’ (β€
β Ο β β) |
62 | | pipos 25970 |
. . . . . . 7
β’ 0 <
Ο |
63 | 9, 10, 62 | ltleii 11337 |
. . . . . 6
β’ 0 β€
Ο |
64 | 63 | a1i 11 |
. . . . 5
β’ (β€
β 0 β€ Ο) |
65 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯sin |
66 | | sincn 25956 |
. . . . . . . 8
β’ sin
β (ββcnββ) |
67 | 66 | a1i 11 |
. . . . . . 7
β’ (β€
β sin β (ββcnββ)) |
68 | 50 | a1i 11 |
. . . . . . 7
β’ (β€
β (0(,)Ο) β β) |
69 | 65, 67, 68 | cncfmptss 44303 |
. . . . . 6
β’ (β€
β (π₯ β (0(,)Ο)
β¦ (sinβπ₯))
β ((0(,)Ο)βcnββ)) |
70 | 48, 69 | eqeltrid 2838 |
. . . . 5
β’ (β€
β (β D πΆ) β
((0(,)Ο)βcnββ)) |
71 | | ioossicc 13410 |
. . . . . . . 8
β’
(0(,)Ο) β (0[,]Ο) |
72 | 71 | a1i 11 |
. . . . . . 7
β’ (β€
β (0(,)Ο) β (0[,]Ο)) |
73 | | ioombl 25082 |
. . . . . . . 8
β’
(0(,)Ο) β dom vol |
74 | 73 | a1i 11 |
. . . . . . 7
β’ (β€
β (0(,)Ο) β dom vol) |
75 | 15 | sincld 16073 |
. . . . . . . 8
β’ (π₯ β (0[,]Ο) β
(sinβπ₯) β
β) |
76 | 75 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π₯
β (0[,]Ο)) β (sinβπ₯) β β) |
77 | 14 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (0[,]Ο) β β) |
78 | 65, 67, 77 | cncfmptss 44303 |
. . . . . . . . . 10
β’ (β€
β (π₯ β (0[,]Ο)
β¦ (sinβπ₯))
β ((0[,]Ο)βcnββ)) |
79 | 78 | mptru 1549 |
. . . . . . . . 9
β’ (π₯ β (0[,]Ο) β¦
(sinβπ₯)) β
((0[,]Ο)βcnββ) |
80 | | cniccibl 25358 |
. . . . . . . . 9
β’ ((0
β β β§ Ο β β β§ (π₯ β (0[,]Ο) β¦ (sinβπ₯)) β
((0[,]Ο)βcnββ)) β
(π₯ β (0[,]Ο)
β¦ (sinβπ₯))
β πΏ1) |
81 | 9, 10, 79, 80 | mp3an 1462 |
. . . . . . . 8
β’ (π₯ β (0[,]Ο) β¦
(sinβπ₯)) β
πΏ1 |
82 | 81 | a1i 11 |
. . . . . . 7
β’ (β€
β (π₯ β (0[,]Ο)
β¦ (sinβπ₯))
β πΏ1) |
83 | 72, 74, 76, 82 | iblss 25322 |
. . . . . 6
β’ (β€
β (π₯ β (0(,)Ο)
β¦ (sinβπ₯))
β πΏ1) |
84 | 48, 83 | eqeltrid 2838 |
. . . . 5
β’ (β€
β (β D πΆ) β
πΏ1) |
85 | 16 | negcld 11558 |
. . . . . . . . . . 11
β’ (π₯ β (0[,]Ο) β
-(cosβπ₯) β
β) |
86 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦
-(cosβπ₯)) = (π₯ β β β¦
-(cosβπ₯)) |
87 | 86 | fvmpt2 7010 |
. . . . . . . . . . 11
β’ ((π₯ β β β§
-(cosβπ₯) β
β) β ((π₯ β
β β¦ -(cosβπ₯))βπ₯) = -(cosβπ₯)) |
88 | 15, 85, 87 | syl2anc 585 |
. . . . . . . . . 10
β’ (π₯ β (0[,]Ο) β
((π₯ β β β¦
-(cosβπ₯))βπ₯) = -(cosβπ₯)) |
89 | 88 | eqcomd 2739 |
. . . . . . . . 9
β’ (π₯ β (0[,]Ο) β
-(cosβπ₯) = ((π₯ β β β¦
-(cosβπ₯))βπ₯)) |
90 | 89 | mpteq2ia 5252 |
. . . . . . . 8
β’ (π₯ β (0[,]Ο) β¦
-(cosβπ₯)) = (π₯ β (0[,]Ο) β¦
((π₯ β β β¦
-(cosβπ₯))βπ₯)) |
91 | | nfmpt1 5257 |
. . . . . . . . . 10
β’
β²π₯(π₯ β β β¦ -(cosβπ₯)) |
92 | | coscn 25957 |
. . . . . . . . . . . 12
β’ cos
β (ββcnββ) |
93 | 86 | negfcncf 24439 |
. . . . . . . . . . . 12
β’ (cos
β (ββcnββ)
β (π₯ β β
β¦ -(cosβπ₯))
β (ββcnββ)) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π₯ β β β¦
-(cosβπ₯)) β
(ββcnββ) |
95 | 94 | a1i 11 |
. . . . . . . . . 10
β’ (β€
β (π₯ β β
β¦ -(cosβπ₯))
β (ββcnββ)) |
96 | 91, 95, 77 | cncfmptss 44303 |
. . . . . . . . 9
β’ (β€
β (π₯ β (0[,]Ο)
β¦ ((π₯ β β
β¦ -(cosβπ₯))βπ₯)) β ((0[,]Ο)βcnββ)) |
97 | 96 | mptru 1549 |
. . . . . . . 8
β’ (π₯ β (0[,]Ο) β¦
((π₯ β β β¦
-(cosβπ₯))βπ₯)) β
((0[,]Ο)βcnββ) |
98 | 90, 97 | eqeltri 2830 |
. . . . . . 7
β’ (π₯ β (0[,]Ο) β¦
-(cosβπ₯)) β
((0[,]Ο)βcnββ) |
99 | 5, 98 | eqeltri 2830 |
. . . . . 6
β’ πΆ β ((0[,]Ο)βcnββ) |
100 | 99 | a1i 11 |
. . . . 5
β’ (β€
β πΆ β
((0[,]Ο)βcnββ)) |
101 | 60, 61, 64, 70, 84, 100 | ftc2 25561 |
. . . 4
β’ (β€
β β«(0(,)Ο)((β D πΆ)βπ₯) dπ₯ = ((πΆβΟ) β (πΆβ0))) |
102 | 101 | mptru 1549 |
. . 3
β’
β«(0(,)Ο)((β D πΆ)βπ₯) dπ₯ = ((πΆβΟ) β (πΆβ0)) |
103 | 59, 102 | eqtr3i 2763 |
. 2
β’
β«(0(,)Ο)(sinβπ₯) dπ₯ = ((πΆβΟ) β (πΆβ0)) |
104 | | 0xr 11261 |
. . . . 5
β’ 0 β
β* |
105 | 10 | rexri 11272 |
. . . . 5
β’ Ο
β β* |
106 | | ubicc2 13442 |
. . . . 5
β’ ((0
β β* β§ Ο β β* β§ 0 β€
Ο) β Ο β (0[,]Ο)) |
107 | 104, 105,
63, 106 | mp3an 1462 |
. . . 4
β’ Ο
β (0[,]Ο) |
108 | | fveq2 6892 |
. . . . . . . 8
β’ (π‘ = Ο β (cosβπ‘) =
(cosβΟ)) |
109 | | cospi 25982 |
. . . . . . . 8
β’
(cosβΟ) = -1 |
110 | 108, 109 | eqtrdi 2789 |
. . . . . . 7
β’ (π‘ = Ο β (cosβπ‘) = -1) |
111 | 110 | negeqd 11454 |
. . . . . 6
β’ (π‘ = Ο β -(cosβπ‘) = --1) |
112 | | ax-1cn 11168 |
. . . . . . . 8
β’ 1 β
β |
113 | 112 | a1i 11 |
. . . . . . 7
β’ (π‘ = Ο β 1 β
β) |
114 | 113 | negnegd 11562 |
. . . . . 6
β’ (π‘ = Ο β --1 =
1) |
115 | 111, 114 | eqtrd 2773 |
. . . . 5
β’ (π‘ = Ο β -(cosβπ‘) = 1) |
116 | | 1ex 11210 |
. . . . 5
β’ 1 β
V |
117 | 115, 1, 116 | fvmpt 6999 |
. . . 4
β’ (Ο
β (0[,]Ο) β (πΆβΟ) = 1) |
118 | 107, 117 | ax-mp 5 |
. . 3
β’ (πΆβΟ) =
1 |
119 | | lbicc2 13441 |
. . . . . 6
β’ ((0
β β* β§ Ο β β* β§ 0 β€
Ο) β 0 β (0[,]Ο)) |
120 | 104, 105,
63, 119 | mp3an 1462 |
. . . . 5
β’ 0 β
(0[,]Ο) |
121 | | fveq2 6892 |
. . . . . . 7
β’ (π‘ = 0 β (cosβπ‘) =
(cosβ0)) |
122 | 121 | negeqd 11454 |
. . . . . 6
β’ (π‘ = 0 β -(cosβπ‘) =
-(cosβ0)) |
123 | | negex 11458 |
. . . . . 6
β’
-(cosβ0) β V |
124 | 122, 1, 123 | fvmpt 6999 |
. . . . 5
β’ (0 β
(0[,]Ο) β (πΆβ0) = -(cosβ0)) |
125 | 120, 124 | ax-mp 5 |
. . . 4
β’ (πΆβ0) =
-(cosβ0) |
126 | | cos0 16093 |
. . . . 5
β’
(cosβ0) = 1 |
127 | 126 | negeqi 11453 |
. . . 4
β’
-(cosβ0) = -1 |
128 | 125, 127 | eqtri 2761 |
. . 3
β’ (πΆβ0) = -1 |
129 | 118, 128 | oveq12i 7421 |
. 2
β’ ((πΆβΟ) β (πΆβ0)) = (1 β
-1) |
130 | 112, 112 | subnegi 11539 |
. . 3
β’ (1
β -1) = (1 + 1) |
131 | | 1p1e2 12337 |
. . 3
β’ (1 + 1) =
2 |
132 | 130, 131 | eqtri 2761 |
. 2
β’ (1
β -1) = 2 |
133 | 103, 129,
132 | 3eqtri 2765 |
1
β’
β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 |