Step | Hyp | Ref
| Expression |
1 | | pire 25831 |
. . . . . 6
β’ Ο
β β |
2 | 1 | renegcli 11469 |
. . . . 5
β’ -Ο
β β |
3 | 2 | a1i 11 |
. . . 4
β’ (π β -Ο β
β) |
4 | 1 | a1i 11 |
. . . 4
β’ (π β Ο β
β) |
5 | | 0re 11164 |
. . . . . 6
β’ 0 β
β |
6 | | negpilt0 43588 |
. . . . . . 7
β’ -Ο
< 0 |
7 | 2, 5, 6 | ltleii 11285 |
. . . . . 6
β’ -Ο
β€ 0 |
8 | | pipos 25833 |
. . . . . . 7
β’ 0 <
Ο |
9 | 5, 1, 8 | ltleii 11285 |
. . . . . 6
β’ 0 β€
Ο |
10 | 2, 1 | elicc2i 13337 |
. . . . . 6
β’ (0 β
(-Ο[,]Ο) β (0 β β β§ -Ο β€ 0 β§ 0 β€
Ο)) |
11 | 5, 7, 9, 10 | mpbir3an 1342 |
. . . . 5
β’ 0 β
(-Ο[,]Ο) |
12 | 11 | a1i 11 |
. . . 4
β’ (π β 0 β
(-Ο[,]Ο)) |
13 | | 1red 11163 |
. . . . . . . . . . 11
β’ (π₯ β β β 1 β
β) |
14 | 13 | renegcld 11589 |
. . . . . . . . . . 11
β’ (π₯ β β β -1 β
β) |
15 | 13, 14 | ifcld 4537 |
. . . . . . . . . 10
β’ (π₯ β β β if((π₯ mod π) < Ο, 1, -1) β
β) |
16 | 15 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β if((π₯ mod π) < Ο, 1, -1) β
β) |
17 | | sqwvfoura.f |
. . . . . . . . 9
β’ πΉ = (π₯ β β β¦ if((π₯ mod π) < Ο, 1, -1)) |
18 | 16, 17 | fmptd 7067 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
19 | 18 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)Ο)) β πΉ:ββΆβ) |
20 | | elioore 13301 |
. . . . . . . 8
β’ (π₯ β (-Ο(,)Ο) β
π₯ β
β) |
21 | 20 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)Ο)) β π₯ β
β) |
22 | 19, 21 | ffvelcdmd 7041 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)Ο)) β (πΉβπ₯) β β) |
23 | | sqwvfoura.n |
. . . . . . . . . 10
β’ (π β π β
β0) |
24 | 23 | nn0red 12481 |
. . . . . . . . 9
β’ (π β π β β) |
25 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο(,)Ο)) β π β
β) |
26 | 25, 21 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)Ο)) β (π Β· π₯) β β) |
27 | 26 | recoscld 16033 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)Ο)) β
(cosβ(π Β·
π₯)) β
β) |
28 | 22, 27 | remulcld 11192 |
. . . . 5
β’ ((π β§ π₯ β (-Ο(,)Ο)) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) β β) |
29 | 28 | recnd 11190 |
. . . 4
β’ ((π β§ π₯ β (-Ο(,)Ο)) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) β β) |
30 | | elioore 13301 |
. . . . . . . . . 10
β’ (π₯ β (-Ο(,)0) β π₯ β
β) |
31 | 17 | fvmpt2 6964 |
. . . . . . . . . 10
β’ ((π₯ β β β§ if((π₯ mod π) < Ο, 1, -1) β β) β
(πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
32 | 30, 15, 31 | syl2anc2 586 |
. . . . . . . . 9
β’ (π₯ β (-Ο(,)0) β
(πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
33 | 1 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β Ο
β β) |
34 | | sqwvfoura.t |
. . . . . . . . . . . . . 14
β’ π = (2 Β·
Ο) |
35 | | 2rp 12927 |
. . . . . . . . . . . . . . 15
β’ 2 β
β+ |
36 | | pirp 25834 |
. . . . . . . . . . . . . . 15
β’ Ο
β β+ |
37 | | rpmulcl 12945 |
. . . . . . . . . . . . . . 15
β’ ((2
β β+ β§ Ο β β+) β (2
Β· Ο) β β+) |
38 | 35, 36, 37 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (2
Β· Ο) β β+ |
39 | 34, 38 | eqeltri 2834 |
. . . . . . . . . . . . 13
β’ π β
β+ |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ β (-Ο(,)0) β π β
β+) |
41 | 30, 40 | modcld 13787 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β
(π₯ mod π) β β) |
42 | | picn 25832 |
. . . . . . . . . . . . . . . . 17
β’ Ο
β β |
43 | 42 | 2timesi 12298 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· Ο) = (Ο + Ο) |
44 | 34, 43 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ π = (Ο +
Ο) |
45 | 44 | oveq2i 7373 |
. . . . . . . . . . . . . 14
β’ (-Ο +
π) = (-Ο + (Ο +
Ο)) |
46 | 2 | recni 11176 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β |
47 | 46, 42, 42 | addassi 11172 |
. . . . . . . . . . . . . 14
β’ ((-Ο +
Ο) + Ο) = (-Ο + (Ο + Ο)) |
48 | 42 | negidi 11477 |
. . . . . . . . . . . . . . . . 17
β’ (Ο +
-Ο) = 0 |
49 | 42, 46, 48 | addcomli 11354 |
. . . . . . . . . . . . . . . 16
β’ (-Ο +
Ο) = 0 |
50 | 49 | oveq1i 7372 |
. . . . . . . . . . . . . . 15
β’ ((-Ο +
Ο) + Ο) = (0 + Ο) |
51 | 42 | addid2i 11350 |
. . . . . . . . . . . . . . 15
β’ (0 +
Ο) = Ο |
52 | 50, 51 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ ((-Ο +
Ο) + Ο) = Ο |
53 | 45, 47, 52 | 3eqtr2ri 2772 |
. . . . . . . . . . . . 13
β’ Ο =
(-Ο + π) |
54 | 2 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β -Ο
β β) |
55 | | 2re 12234 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
56 | 55, 1 | remulcli 11178 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· Ο) β β |
57 | 34, 56 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
β’ π β β |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β π β
β) |
59 | 2 | rexri 11220 |
. . . . . . . . . . . . . . . 16
β’ -Ο
β β* |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β -Ο
β β*) |
61 | | 0red 11165 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (-Ο(,)0) β 0
β β) |
62 | 61 | rexrd 11212 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β 0
β β*) |
63 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β π₯ β
(-Ο(,)0)) |
64 | | ioogtlb 43807 |
. . . . . . . . . . . . . . 15
β’ ((-Ο
β β* β§ 0 β β* β§ π₯ β (-Ο(,)0)) β
-Ο < π₯) |
65 | 60, 62, 63, 64 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β -Ο
< π₯) |
66 | 54, 30, 58, 65 | ltadd1dd 11773 |
. . . . . . . . . . . . 13
β’ (π₯ β (-Ο(,)0) β
(-Ο + π) < (π₯ + π)) |
67 | 53, 66 | eqbrtrid 5145 |
. . . . . . . . . . . 12
β’ (π₯ β (-Ο(,)0) β Ο
< (π₯ + π)) |
68 | 57 | recni 11176 |
. . . . . . . . . . . . . . . . 17
β’ π β β |
69 | 68 | mulid2i 11167 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· π) = π |
70 | 69 | eqcomi 2746 |
. . . . . . . . . . . . . . 15
β’ π = (1 Β· π) |
71 | 70 | oveq2i 7373 |
. . . . . . . . . . . . . 14
β’ (π₯ + π) = (π₯ + (1 Β· π)) |
72 | 71 | oveq1i 7372 |
. . . . . . . . . . . . 13
β’ ((π₯ + π) mod π) = ((π₯ + (1 Β· π)) mod π) |
73 | 30, 58 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) β β) |
74 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (-Ο(,)0) β 0
< Ο) |
75 | 61, 33, 73, 74, 67 | lttrd 11323 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β 0
< (π₯ + π)) |
76 | 61, 73, 75 | ltled 11310 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β 0
β€ (π₯ + π)) |
77 | | iooltub 43822 |
. . . . . . . . . . . . . . . . 17
β’ ((-Ο
β β* β§ 0 β β* β§ π₯ β (-Ο(,)0)) β
π₯ < 0) |
78 | 60, 62, 63, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (-Ο(,)0) β π₯ < 0) |
79 | 30, 61, 58, 78 | ltadd1dd 11773 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) < (0 + π)) |
80 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (-Ο(,)0) β π β
β) |
81 | 80 | addid2d 11363 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β (0 +
π) = π) |
82 | 79, 81 | breqtrd 5136 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) < π) |
83 | | modid 13808 |
. . . . . . . . . . . . . 14
β’ ((((π₯ + π) β β β§ π β β+) β§ (0 β€
(π₯ + π) β§ (π₯ + π) < π)) β ((π₯ + π) mod π) = (π₯ + π)) |
84 | 73, 40, 76, 82, 83 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ (π₯ β (-Ο(,)0) β
((π₯ + π) mod π) = (π₯ + π)) |
85 | | 1zzd 12541 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β 1
β β€) |
86 | | modcyc 13818 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π β β+
β§ 1 β β€) β ((π₯ + (1 Β· π)) mod π) = (π₯ mod π)) |
87 | 30, 40, 85, 86 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π₯ β (-Ο(,)0) β
((π₯ + (1 Β· π)) mod π) = (π₯ mod π)) |
88 | 72, 84, 87 | 3eqtr3a 2801 |
. . . . . . . . . . . 12
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) = (π₯ mod π)) |
89 | 67, 88 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β Ο
< (π₯ mod π)) |
90 | 33, 41, 89 | ltnsymd 11311 |
. . . . . . . . . 10
β’ (π₯ β (-Ο(,)0) β Β¬
(π₯ mod π) < Ο) |
91 | 90 | iffalsed 4502 |
. . . . . . . . 9
β’ (π₯ β (-Ο(,)0) β
if((π₯ mod π) < Ο, 1, -1) = -1) |
92 | 32, 91 | eqtrd 2777 |
. . . . . . . 8
β’ (π₯ β (-Ο(,)0) β
(πΉβπ₯) = -1) |
93 | 92 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ β (-Ο(,)0) β
((πΉβπ₯) Β· (cosβ(π Β· π₯))) = (-1 Β· (cosβ(π Β· π₯)))) |
94 | 93 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)0)) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) = (-1 Β· (cosβ(π Β· π₯)))) |
95 | 94 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β (-Ο(,)0) β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) = (π₯ β (-Ο(,)0) β¦ (-1 Β·
(cosβ(π Β·
π₯))))) |
96 | | 1cnd 11157 |
. . . . . . 7
β’ (π β 1 β
β) |
97 | 96 | negcld 11506 |
. . . . . 6
β’ (π β -1 β
β) |
98 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο(,)0)) β π β β) |
99 | 30 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο(,)0)) β π₯ β
β) |
100 | 98, 99 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)0)) β (π Β· π₯) β β) |
101 | 100 | recoscld 16033 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)0)) β (cosβ(π Β· π₯)) β β) |
102 | | ioossicc 13357 |
. . . . . . . 8
β’
(-Ο(,)0) β (-Ο[,]0) |
103 | 102 | a1i 11 |
. . . . . . 7
β’ (π β (-Ο(,)0) β
(-Ο[,]0)) |
104 | | ioombl 24945 |
. . . . . . . 8
β’
(-Ο(,)0) β dom vol |
105 | 104 | a1i 11 |
. . . . . . 7
β’ (π β (-Ο(,)0) β dom
vol) |
106 | 24 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (-Ο[,]0)) β π β β) |
107 | | iccssre 13353 |
. . . . . . . . . . . 12
β’ ((-Ο
β β β§ 0 β β) β (-Ο[,]0) β
β) |
108 | 2, 5, 107 | mp2an 691 |
. . . . . . . . . . 11
β’
(-Ο[,]0) β β |
109 | 108 | sseli 3945 |
. . . . . . . . . 10
β’ (π₯ β (-Ο[,]0) β π₯ β
β) |
110 | 109 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (-Ο[,]0)) β π₯ β
β) |
111 | 106, 110 | remulcld 11192 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο[,]0)) β (π Β· π₯) β β) |
112 | 111 | recoscld 16033 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο[,]0)) β (cosβ(π Β· π₯)) β β) |
113 | | 0red 11165 |
. . . . . . . 8
β’ (π β 0 β
β) |
114 | | coscn 25820 |
. . . . . . . . . 10
β’ cos
β (ββcnββ) |
115 | 114 | a1i 11 |
. . . . . . . . 9
β’ (π β cos β
(ββcnββ)) |
116 | | ax-resscn 11115 |
. . . . . . . . . . . . 13
β’ β
β β |
117 | 108, 116 | sstri 3958 |
. . . . . . . . . . . 12
β’
(-Ο[,]0) β β |
118 | 117 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (-Ο[,]0) β
β) |
119 | 24 | recnd 11190 |
. . . . . . . . . . 11
β’ (π β π β β) |
120 | | ssid 3971 |
. . . . . . . . . . . 12
β’ β
β β |
121 | 120 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β
β) |
122 | 118, 119,
121 | constcncfg 44187 |
. . . . . . . . . 10
β’ (π β (π₯ β (-Ο[,]0) β¦ π) β ((-Ο[,]0)βcnββ)) |
123 | 118, 121 | idcncfg 44188 |
. . . . . . . . . 10
β’ (π β (π₯ β (-Ο[,]0) β¦ π₯) β
((-Ο[,]0)βcnββ)) |
124 | 122, 123 | mulcncf 24826 |
. . . . . . . . 9
β’ (π β (π₯ β (-Ο[,]0) β¦ (π Β· π₯)) β ((-Ο[,]0)βcnββ)) |
125 | 115, 124 | cncfmpt1f 24293 |
. . . . . . . 8
β’ (π β (π₯ β (-Ο[,]0) β¦ (cosβ(π Β· π₯))) β ((-Ο[,]0)βcnββ)) |
126 | | cniccibl 25221 |
. . . . . . . 8
β’ ((-Ο
β β β§ 0 β β β§ (π₯ β (-Ο[,]0) β¦ (cosβ(π Β· π₯))) β ((-Ο[,]0)βcnββ)) β (π₯ β (-Ο[,]0) β¦ (cosβ(π Β· π₯))) β
πΏ1) |
127 | 3, 113, 125, 126 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β (-Ο[,]0) β¦ (cosβ(π Β· π₯))) β
πΏ1) |
128 | 103, 105,
112, 127 | iblss 25185 |
. . . . . 6
β’ (π β (π₯ β (-Ο(,)0) β¦ (cosβ(π Β· π₯))) β
πΏ1) |
129 | 97, 101, 128 | iblmulc2 25211 |
. . . . 5
β’ (π β (π₯ β (-Ο(,)0) β¦ (-1 Β·
(cosβ(π Β·
π₯)))) β
πΏ1) |
130 | 95, 129 | eqeltrd 2838 |
. . . 4
β’ (π β (π₯ β (-Ο(,)0) β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) β
πΏ1) |
131 | | elioore 13301 |
. . . . . . . . . 10
β’ (π₯ β (0(,)Ο) β π₯ β
β) |
132 | 131, 15, 31 | syl2anc2 586 |
. . . . . . . . 9
β’ (π₯ β (0(,)Ο) β (πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
133 | 39 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β π β
β+) |
134 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β 0
β β) |
135 | 134 | rexrd 11212 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0(,)Ο) β 0
β β*) |
136 | 1 | rexri 11220 |
. . . . . . . . . . . . . . 15
β’ Ο
β β* |
137 | 136 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0(,)Ο) β Ο
β β*) |
138 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0(,)Ο) β π₯ β
(0(,)Ο)) |
139 | | ioogtlb 43807 |
. . . . . . . . . . . . . 14
β’ ((0
β β* β§ Ο β β* β§ π₯ β (0(,)Ο)) β 0
< π₯) |
140 | 135, 137,
138, 139 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β 0 <
π₯) |
141 | 134, 131,
140 | ltled 11310 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β 0 β€
π₯) |
142 | 1 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β Ο
β β) |
143 | 57 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β π β
β) |
144 | | iooltub 43822 |
. . . . . . . . . . . . . 14
β’ ((0
β β* β§ Ο β β* β§ π₯ β (0(,)Ο)) β π₯ < Ο) |
145 | 135, 137,
138, 144 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β π₯ < Ο) |
146 | | 2timesgt 43596 |
. . . . . . . . . . . . . . . 16
β’ (Ο
β β+ β Ο < (2 Β· Ο)) |
147 | 36, 146 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ Ο <
(2 Β· Ο) |
148 | 147, 34 | breqtrri 5137 |
. . . . . . . . . . . . . 14
β’ Ο <
π |
149 | 148 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β Ο
< π) |
150 | 131, 142,
143, 145, 149 | lttrd 11323 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β π₯ < π) |
151 | | modid 13808 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π β β+)
β§ (0 β€ π₯ β§ π₯ < π)) β (π₯ mod π) = π₯) |
152 | 131, 133,
141, 150, 151 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β (π₯ mod π) = π₯) |
153 | 152, 145 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ (π₯ β (0(,)Ο) β (π₯ mod π) < Ο) |
154 | 153 | iftrued 4499 |
. . . . . . . . 9
β’ (π₯ β (0(,)Ο) β
if((π₯ mod π) < Ο, 1, -1) = 1) |
155 | 132, 154 | eqtrd 2777 |
. . . . . . . 8
β’ (π₯ β (0(,)Ο) β (πΉβπ₯) = 1) |
156 | 155 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ β (0(,)Ο) β
((πΉβπ₯) Β· (cosβ(π Β· π₯))) = (1 Β· (cosβ(π Β· π₯)))) |
157 | 156 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β (0(,)Ο)) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) = (1 Β· (cosβ(π Β· π₯)))) |
158 | 157 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β (0(,)Ο) β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) = (π₯ β (0(,)Ο) β¦ (1 Β·
(cosβ(π Β·
π₯))))) |
159 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (0(,)Ο)) β π β β) |
160 | 131 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (0(,)Ο)) β π₯ β β) |
161 | 159, 160 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π₯ β (0(,)Ο)) β (π Β· π₯) β β) |
162 | 161 | recoscld 16033 |
. . . . . 6
β’ ((π β§ π₯ β (0(,)Ο)) β (cosβ(π Β· π₯)) β β) |
163 | | ioossicc 13357 |
. . . . . . . 8
β’
(0(,)Ο) β (0[,]Ο) |
164 | 163 | a1i 11 |
. . . . . . 7
β’ (π β (0(,)Ο) β
(0[,]Ο)) |
165 | | ioombl 24945 |
. . . . . . . 8
β’
(0(,)Ο) β dom vol |
166 | 165 | a1i 11 |
. . . . . . 7
β’ (π β (0(,)Ο) β dom
vol) |
167 | 24 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (0[,]Ο)) β π β β) |
168 | | iccssre 13353 |
. . . . . . . . . . . 12
β’ ((0
β β β§ Ο β β) β (0[,]Ο) β
β) |
169 | 5, 1, 168 | mp2an 691 |
. . . . . . . . . . 11
β’
(0[,]Ο) β β |
170 | 169 | sseli 3945 |
. . . . . . . . . 10
β’ (π₯ β (0[,]Ο) β π₯ β
β) |
171 | 170 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (0[,]Ο)) β π₯ β β) |
172 | 167, 171 | remulcld 11192 |
. . . . . . . 8
β’ ((π β§ π₯ β (0[,]Ο)) β (π Β· π₯) β β) |
173 | 172 | recoscld 16033 |
. . . . . . 7
β’ ((π β§ π₯ β (0[,]Ο)) β (cosβ(π Β· π₯)) β β) |
174 | 169, 116 | sstri 3958 |
. . . . . . . . . . . 12
β’
(0[,]Ο) β β |
175 | 174 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (0[,]Ο) β
β) |
176 | 175, 119,
121 | constcncfg 44187 |
. . . . . . . . . 10
β’ (π β (π₯ β (0[,]Ο) β¦ π) β ((0[,]Ο)βcnββ)) |
177 | 175, 121 | idcncfg 44188 |
. . . . . . . . . 10
β’ (π β (π₯ β (0[,]Ο) β¦ π₯) β ((0[,]Ο)βcnββ)) |
178 | 176, 177 | mulcncf 24826 |
. . . . . . . . 9
β’ (π β (π₯ β (0[,]Ο) β¦ (π Β· π₯)) β ((0[,]Ο)βcnββ)) |
179 | 115, 178 | cncfmpt1f 24293 |
. . . . . . . 8
β’ (π β (π₯ β (0[,]Ο) β¦ (cosβ(π Β· π₯))) β ((0[,]Ο)βcnββ)) |
180 | | cniccibl 25221 |
. . . . . . . 8
β’ ((0
β β β§ Ο β β β§ (π₯ β (0[,]Ο) β¦ (cosβ(π Β· π₯))) β ((0[,]Ο)βcnββ)) β (π₯ β (0[,]Ο) β¦ (cosβ(π Β· π₯))) β
πΏ1) |
181 | 113, 4, 179, 180 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β (0[,]Ο) β¦ (cosβ(π Β· π₯))) β
πΏ1) |
182 | 164, 166,
173, 181 | iblss 25185 |
. . . . . 6
β’ (π β (π₯ β (0(,)Ο) β¦ (cosβ(π Β· π₯))) β
πΏ1) |
183 | 96, 162, 182 | iblmulc2 25211 |
. . . . 5
β’ (π β (π₯ β (0(,)Ο) β¦ (1 Β·
(cosβ(π Β·
π₯)))) β
πΏ1) |
184 | 158, 183 | eqeltrd 2838 |
. . . 4
β’ (π β (π₯ β (0(,)Ο) β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) β
πΏ1) |
185 | 3, 4, 12, 29, 130, 184 | itgsplitioo 25218 |
. . 3
β’ (π β β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ = (β«(-Ο(,)0)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯)) |
186 | 185 | oveq1d 7377 |
. 2
β’ (π β
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο) = ((β«(-Ο(,)0)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯) / Ο)) |
187 | 94 | itgeq2dv 25162 |
. . . . 5
β’ (π β β«(-Ο(,)0)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ = β«(-Ο(,)0)(-1 Β·
(cosβ(π Β·
π₯))) dπ₯) |
188 | 97, 101, 128 | itgmulc2 25214 |
. . . . 5
β’ (π β (-1 Β·
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯) = β«(-Ο(,)0)(-1 Β·
(cosβ(π Β·
π₯))) dπ₯) |
189 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (π Β· π₯) = (0 Β· π₯)) |
190 | | ioosscn 13333 |
. . . . . . . . . . . . . . . 16
β’
(-Ο(,)0) β β |
191 | 190 | sseli 3945 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β π₯ β
β) |
192 | 191 | mul02d 11360 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β (0
Β· π₯) =
0) |
193 | 189, 192 | sylan9eq 2797 |
. . . . . . . . . . . . 13
β’ ((π = 0 β§ π₯ β (-Ο(,)0)) β (π Β· π₯) = 0) |
194 | 193 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π = 0 β§ π₯ β (-Ο(,)0)) β (cosβ(π Β· π₯)) = (cosβ0)) |
195 | | cos0 16039 |
. . . . . . . . . . . 12
β’
(cosβ0) = 1 |
196 | 194, 195 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((π = 0 β§ π₯ β (-Ο(,)0)) β (cosβ(π Β· π₯)) = 1) |
197 | 196 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π = 0) β§ π₯ β (-Ο(,)0)) β (cosβ(π Β· π₯)) = 1) |
198 | 197 | itgeq2dv 25162 |
. . . . . . . . 9
β’ ((π β§ π = 0) β
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯ = β«(-Ο(,)0)1 dπ₯) |
199 | | ioovolcl 24950 |
. . . . . . . . . . . . 13
β’ ((-Ο
β β β§ 0 β β) β (volβ(-Ο(,)0)) β
β) |
200 | 2, 5, 199 | mp2an 691 |
. . . . . . . . . . . 12
β’
(volβ(-Ο(,)0)) β β |
201 | 200 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (volβ(-Ο(,)0))
β β) |
202 | | itgconst 25199 |
. . . . . . . . . . 11
β’
(((-Ο(,)0) β dom vol β§ (volβ(-Ο(,)0)) β
β β§ 1 β β) β β«(-Ο(,)0)1 dπ₯ = (1 Β·
(volβ(-Ο(,)0)))) |
203 | 105, 201,
96, 202 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β β«(-Ο(,)0)1 dπ₯ = (1 Β·
(volβ(-Ο(,)0)))) |
204 | 203 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π = 0) β β«(-Ο(,)0)1 dπ₯ = (1 Β·
(volβ(-Ο(,)0)))) |
205 | | volioo 24949 |
. . . . . . . . . . . . . . 15
β’ ((-Ο
β β β§ 0 β β β§ -Ο β€ 0) β
(volβ(-Ο(,)0)) = (0 β -Ο)) |
206 | 2, 5, 7, 205 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’
(volβ(-Ο(,)0)) = (0 β -Ο) |
207 | | 0cn 11154 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
208 | 207, 42 | subnegi 11487 |
. . . . . . . . . . . . . 14
β’ (0
β -Ο) = (0 + Ο) |
209 | 206, 208,
51 | 3eqtri 2769 |
. . . . . . . . . . . . 13
β’
(volβ(-Ο(,)0)) = Ο |
210 | 209 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (volβ(-Ο(,)0)) =
Ο) |
211 | 210 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π β (1 Β·
(volβ(-Ο(,)0))) = (1 Β· Ο)) |
212 | 42 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β Ο β
β) |
213 | 212 | mulid2d 11180 |
. . . . . . . . . . 11
β’ (π β (1 Β· Ο) =
Ο) |
214 | 211, 213 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π β (1 Β·
(volβ(-Ο(,)0))) = Ο) |
215 | 214 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π = 0) β (1 Β·
(volβ(-Ο(,)0))) = Ο) |
216 | 198, 204,
215 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π β§ π = 0) β
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯ = Ο) |
217 | 216 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ π = 0) β (-1 Β·
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯) = (-1 Β· Ο)) |
218 | 42 | mulm1i 11607 |
. . . . . . . 8
β’ (-1
Β· Ο) = -Ο |
219 | 218 | a1i 11 |
. . . . . . 7
β’ ((π β§ π = 0) β (-1 Β· Ο) =
-Ο) |
220 | | iftrue 4497 |
. . . . . . . . 9
β’ (π = 0 β if(π = 0, -Ο, 0) = -Ο) |
221 | 220 | eqcomd 2743 |
. . . . . . . 8
β’ (π = 0 β -Ο = if(π = 0, -Ο,
0)) |
222 | 221 | adantl 483 |
. . . . . . 7
β’ ((π β§ π = 0) β -Ο = if(π = 0, -Ο, 0)) |
223 | 217, 219,
222 | 3eqtrd 2781 |
. . . . . 6
β’ ((π β§ π = 0) β (-1 Β·
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯) = if(π = 0, -Ο, 0)) |
224 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ Β¬ π = 0) β π β β) |
225 | 23 | nn0ge0d 12483 |
. . . . . . . . 9
β’ (π β 0 β€ π) |
226 | 225 | adantr 482 |
. . . . . . . 8
β’ ((π β§ Β¬ π = 0) β 0 β€ π) |
227 | | neqne 2952 |
. . . . . . . . 9
β’ (Β¬
π = 0 β π β 0) |
228 | 227 | adantl 483 |
. . . . . . . 8
β’ ((π β§ Β¬ π = 0) β π β 0) |
229 | 224, 226,
228 | ne0gt0d 11299 |
. . . . . . 7
β’ ((π β§ Β¬ π = 0) β 0 < π) |
230 | | 1cnd 11157 |
. . . . . . . . . 10
β’ ((π β§ 0 < π) β 1 β β) |
231 | 230 | negcld 11506 |
. . . . . . . . 9
β’ ((π β§ 0 < π) β -1 β β) |
232 | 231 | mul01d 11361 |
. . . . . . . 8
β’ ((π β§ 0 < π) β (-1 Β· 0) =
0) |
233 | 119 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β π β β) |
234 | 2 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β -Ο β
β) |
235 | | 0red 11165 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β 0 β β) |
236 | 7 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β -Ο β€ 0) |
237 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ 0 < π) β 0 < π) |
238 | 237 | gt0ne0d 11726 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β π β 0) |
239 | 233, 234,
235, 236, 238 | itgcoscmulx 44284 |
. . . . . . . . . 10
β’ ((π β§ 0 < π) β β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯ = (((sinβ(π Β· 0)) β (sinβ(π Β· -Ο))) / π)) |
240 | 119 | mul01d 11361 |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· 0) = 0) |
241 | 240 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π β (sinβ(π Β· 0)) =
(sinβ0)) |
242 | | sin0 16038 |
. . . . . . . . . . . . . . 15
β’
(sinβ0) = 0 |
243 | 241, 242 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π β (sinβ(π Β· 0)) =
0) |
244 | 119, 212 | mulneg2d 11616 |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· -Ο) = -(π Β· Ο)) |
245 | 244 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π β (sinβ(π Β· -Ο)) =
(sinβ-(π Β·
Ο))) |
246 | 119, 212 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· Ο) β
β) |
247 | | sinneg 16035 |
. . . . . . . . . . . . . . . 16
β’ ((π Β· Ο) β β
β (sinβ-(π
Β· Ο)) = -(sinβ(π Β· Ο))) |
248 | 246, 247 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (sinβ-(π Β· Ο)) =
-(sinβ(π Β·
Ο))) |
249 | 245, 248 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (π β (sinβ(π Β· -Ο)) =
-(sinβ(π Β·
Ο))) |
250 | 243, 249 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π β ((sinβ(π Β· 0)) β
(sinβ(π Β·
-Ο))) = (0 β -(sinβ(π Β· Ο)))) |
251 | | 0cnd 11155 |
. . . . . . . . . . . . . 14
β’ (π β 0 β
β) |
252 | 246 | sincld 16019 |
. . . . . . . . . . . . . 14
β’ (π β (sinβ(π Β· Ο)) β
β) |
253 | 251, 252 | subnegd 11526 |
. . . . . . . . . . . . 13
β’ (π β (0 β
-(sinβ(π Β·
Ο))) = (0 + (sinβ(π Β· Ο)))) |
254 | 252 | addid2d 11363 |
. . . . . . . . . . . . 13
β’ (π β (0 + (sinβ(π Β· Ο))) =
(sinβ(π Β·
Ο))) |
255 | 250, 253,
254 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ (π β ((sinβ(π Β· 0)) β
(sinβ(π Β·
-Ο))) = (sinβ(π
Β· Ο))) |
256 | 255 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β ((sinβ(π Β· 0)) β (sinβ(π Β· -Ο))) =
(sinβ(π Β·
Ο))) |
257 | 256 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ 0 < π) β (((sinβ(π Β· 0)) β (sinβ(π Β· -Ο))) / π) = ((sinβ(π Β· Ο)) / π)) |
258 | 23 | nn0zd 12532 |
. . . . . . . . . . . . . 14
β’ (π β π β β€) |
259 | | sinkpi 25894 |
. . . . . . . . . . . . . 14
β’ (π β β€ β
(sinβ(π Β·
Ο)) = 0) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (sinβ(π Β· Ο)) =
0) |
261 | 260 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π β ((sinβ(π Β· Ο)) / π) = (0 / π)) |
262 | 261 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β ((sinβ(π Β· Ο)) / π) = (0 / π)) |
263 | 233, 238 | div0d 11937 |
. . . . . . . . . . 11
β’ ((π β§ 0 < π) β (0 / π) = 0) |
264 | 262, 263 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ 0 < π) β ((sinβ(π Β· Ο)) / π) = 0) |
265 | 239, 257,
264 | 3eqtrd 2781 |
. . . . . . . . 9
β’ ((π β§ 0 < π) β β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯ = 0) |
266 | 265 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β§ 0 < π) β (-1 Β·
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯) = (-1 Β· 0)) |
267 | 238 | neneqd 2949 |
. . . . . . . . 9
β’ ((π β§ 0 < π) β Β¬ π = 0) |
268 | 267 | iffalsed 4502 |
. . . . . . . 8
β’ ((π β§ 0 < π) β if(π = 0, -Ο, 0) = 0) |
269 | 232, 266,
268 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((π β§ 0 < π) β (-1 Β·
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯) = if(π = 0, -Ο, 0)) |
270 | 229, 269 | syldan 592 |
. . . . . 6
β’ ((π β§ Β¬ π = 0) β (-1 Β·
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯) = if(π = 0, -Ο, 0)) |
271 | 223, 270 | pm2.61dan 812 |
. . . . 5
β’ (π β (-1 Β·
β«(-Ο(,)0)(cosβ(π Β· π₯)) dπ₯) = if(π = 0, -Ο, 0)) |
272 | 187, 188,
271 | 3eqtr2d 2783 |
. . . 4
β’ (π β β«(-Ο(,)0)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ = if(π = 0, -Ο, 0)) |
273 | 157 | itgeq2dv 25162 |
. . . . 5
β’ (π β β«(0(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ = β«(0(,)Ο)(1 Β·
(cosβ(π Β·
π₯))) dπ₯) |
274 | 96, 162, 182 | itgmulc2 25214 |
. . . . 5
β’ (π β (1 Β·
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯) = β«(0(,)Ο)(1 Β·
(cosβ(π Β·
π₯))) dπ₯) |
275 | 162, 182 | itgcl 25164 |
. . . . . . 7
β’ (π β
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯ β β) |
276 | 275 | mulid2d 11180 |
. . . . . 6
β’ (π β (1 Β·
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯) = β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯) |
277 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π = 0 β§ π₯ β (0(,)Ο)) β π = 0) |
278 | 277 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π = 0 β§ π₯ β (0(,)Ο)) β (π Β· π₯) = (0 Β· π₯)) |
279 | 131 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (0(,)Ο) β π₯ β
β) |
280 | 279 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π = 0 β§ π₯ β (0(,)Ο)) β π₯ β β) |
281 | 280 | mul02d 11360 |
. . . . . . . . . . . . 13
β’ ((π = 0 β§ π₯ β (0(,)Ο)) β (0 Β· π₯) = 0) |
282 | 278, 281 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π = 0 β§ π₯ β (0(,)Ο)) β (π Β· π₯) = 0) |
283 | 282 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π = 0 β§ π₯ β (0(,)Ο)) β (cosβ(π Β· π₯)) = (cosβ0)) |
284 | 283, 195 | eqtrdi 2793 |
. . . . . . . . . 10
β’ ((π = 0 β§ π₯ β (0(,)Ο)) β (cosβ(π Β· π₯)) = 1) |
285 | 284 | adantll 713 |
. . . . . . . . 9
β’ (((π β§ π = 0) β§ π₯ β (0(,)Ο)) β (cosβ(π Β· π₯)) = 1) |
286 | 285 | itgeq2dv 25162 |
. . . . . . . 8
β’ ((π β§ π = 0) β
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯ = β«(0(,)Ο)1 dπ₯) |
287 | | ioovolcl 24950 |
. . . . . . . . . . 11
β’ ((0
β β β§ Ο β β) β (volβ(0(,)Ο)) β
β) |
288 | 5, 1, 287 | mp2an 691 |
. . . . . . . . . 10
β’
(volβ(0(,)Ο)) β β |
289 | | ax-1cn 11116 |
. . . . . . . . . 10
β’ 1 β
β |
290 | | itgconst 25199 |
. . . . . . . . . 10
β’
(((0(,)Ο) β dom vol β§ (volβ(0(,)Ο)) β β
β§ 1 β β) β β«(0(,)Ο)1 dπ₯ = (1 Β·
(volβ(0(,)Ο)))) |
291 | 165, 288,
289, 290 | mp3an 1462 |
. . . . . . . . 9
β’
β«(0(,)Ο)1 dπ₯
= (1 Β· (volβ(0(,)Ο))) |
292 | 291 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π = 0) β β«(0(,)Ο)1 dπ₯ = (1 Β·
(volβ(0(,)Ο)))) |
293 | 42 | mulid2i 11167 |
. . . . . . . . . 10
β’ (1
Β· Ο) = Ο |
294 | | volioo 24949 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ Ο β β β§ 0 β€ Ο) β
(volβ(0(,)Ο)) = (Ο β 0)) |
295 | 5, 1, 9, 294 | mp3an 1462 |
. . . . . . . . . . . . 13
β’
(volβ(0(,)Ο)) = (Ο β 0) |
296 | 42 | subid1i 11480 |
. . . . . . . . . . . . 13
β’ (Ο
β 0) = Ο |
297 | 295, 296 | eqtri 2765 |
. . . . . . . . . . . 12
β’
(volβ(0(,)Ο)) = Ο |
298 | 297 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (1
Β· (volβ(0(,)Ο))) = (1 Β· Ο) |
299 | 298 | a1i 11 |
. . . . . . . . . 10
β’ (π = 0 β (1 Β·
(volβ(0(,)Ο))) = (1 Β· Ο)) |
300 | | iftrue 4497 |
. . . . . . . . . 10
β’ (π = 0 β if(π = 0, Ο, 0) = Ο) |
301 | 293, 299,
300 | 3eqtr4a 2803 |
. . . . . . . . 9
β’ (π = 0 β (1 Β·
(volβ(0(,)Ο))) = if(π = 0, Ο, 0)) |
302 | 301 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π = 0) β (1 Β·
(volβ(0(,)Ο))) = if(π = 0, Ο, 0)) |
303 | 286, 292,
302 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ π = 0) β
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯ = if(π = 0, Ο, 0)) |
304 | 260, 243 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π β ((sinβ(π Β· Ο)) β
(sinβ(π Β· 0)))
= (0 β 0)) |
305 | 251 | subidd 11507 |
. . . . . . . . . . . . 13
β’ (π β (0 β 0) =
0) |
306 | 304, 305 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β ((sinβ(π Β· Ο)) β
(sinβ(π Β· 0)))
= 0) |
307 | 306 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π β (((sinβ(π Β· Ο)) β
(sinβ(π Β· 0)))
/ π) = (0 / π)) |
308 | 307 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ 0 < π) β (((sinβ(π Β· Ο)) β (sinβ(π Β· 0))) / π) = (0 / π)) |
309 | 308, 263 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ 0 < π) β (((sinβ(π Β· Ο)) β (sinβ(π Β· 0))) / π) = 0) |
310 | 1 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ 0 < π) β Ο β
β) |
311 | 9 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ 0 < π) β 0 β€ Ο) |
312 | 233, 235,
310, 311, 238 | itgcoscmulx 44284 |
. . . . . . . . 9
β’ ((π β§ 0 < π) β β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯ = (((sinβ(π Β· Ο)) β (sinβ(π Β· 0))) / π)) |
313 | 267 | iffalsed 4502 |
. . . . . . . . 9
β’ ((π β§ 0 < π) β if(π = 0, Ο, 0) = 0) |
314 | 309, 312,
313 | 3eqtr4d 2787 |
. . . . . . . 8
β’ ((π β§ 0 < π) β β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯ = if(π = 0, Ο, 0)) |
315 | 229, 314 | syldan 592 |
. . . . . . 7
β’ ((π β§ Β¬ π = 0) β
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯ = if(π = 0, Ο, 0)) |
316 | 303, 315 | pm2.61dan 812 |
. . . . . 6
β’ (π β
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯ = if(π = 0, Ο, 0)) |
317 | 276, 316 | eqtrd 2777 |
. . . . 5
β’ (π β (1 Β·
β«(0(,)Ο)(cosβ(π Β· π₯)) dπ₯) = if(π = 0, Ο, 0)) |
318 | 273, 274,
317 | 3eqtr2d 2783 |
. . . 4
β’ (π β β«(0(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ = if(π = 0, Ο, 0)) |
319 | 272, 318 | oveq12d 7380 |
. . 3
β’ (π β (β«(-Ο(,)0)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯) = (if(π = 0, -Ο, 0) + if(π = 0, Ο, 0))) |
320 | 319 | oveq1d 7377 |
. 2
β’ (π β ((β«(-Ο(,)0)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯) / Ο) = ((if(π = 0, -Ο, 0) + if(π = 0, Ο, 0)) / Ο)) |
321 | 220, 300 | oveq12d 7380 |
. . . . . . 7
β’ (π = 0 β (if(π = 0, -Ο, 0) + if(π = 0, Ο, 0)) = (-Ο +
Ο)) |
322 | 321, 49 | eqtrdi 2793 |
. . . . . 6
β’ (π = 0 β (if(π = 0, -Ο, 0) + if(π = 0, Ο, 0)) =
0) |
323 | | iffalse 4500 |
. . . . . . . 8
β’ (Β¬
π = 0 β if(π = 0, -Ο, 0) =
0) |
324 | | iffalse 4500 |
. . . . . . . 8
β’ (Β¬
π = 0 β if(π = 0, Ο, 0) =
0) |
325 | 323, 324 | oveq12d 7380 |
. . . . . . 7
β’ (Β¬
π = 0 β (if(π = 0, -Ο, 0) + if(π = 0, Ο, 0)) = (0 +
0)) |
326 | | 00id 11337 |
. . . . . . 7
β’ (0 + 0) =
0 |
327 | 325, 326 | eqtrdi 2793 |
. . . . . 6
β’ (Β¬
π = 0 β (if(π = 0, -Ο, 0) + if(π = 0, Ο, 0)) =
0) |
328 | 322, 327 | pm2.61i 182 |
. . . . 5
β’ (if(π = 0, -Ο, 0) + if(π = 0, Ο, 0)) =
0 |
329 | 328 | oveq1i 7372 |
. . . 4
β’
((if(π = 0, -Ο,
0) + if(π = 0, Ο, 0)) /
Ο) = (0 / Ο) |
330 | 5, 8 | gtneii 11274 |
. . . . 5
β’ Ο β
0 |
331 | 42, 330 | div0i 11896 |
. . . 4
β’ (0 /
Ο) = 0 |
332 | 329, 331 | eqtri 2765 |
. . 3
β’
((if(π = 0, -Ο,
0) + if(π = 0, Ο, 0)) /
Ο) = 0 |
333 | 332 | a1i 11 |
. 2
β’ (π β ((if(π = 0, -Ο, 0) + if(π = 0, Ο, 0)) / Ο) =
0) |
334 | 186, 320,
333 | 3eqtrd 2781 |
1
β’ (π β
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο) = 0) |