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 | | elioore 13301 |
. . . . . . . 8
β’ (π₯ β (-Ο(,)Ο) β
π₯ β
β) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)Ο)) β π₯ β
β) |
15 | | 1re 11162 |
. . . . . . . 8
β’ 1 β
β |
16 | 15 | renegcli 11469 |
. . . . . . . 8
β’ -1 β
β |
17 | 15, 16 | ifcli 4538 |
. . . . . . 7
β’ if((π₯ mod π) < Ο, 1, -1) β
β |
18 | | sqwvfourb.f |
. . . . . . . 8
β’ πΉ = (π₯ β β β¦ if((π₯ mod π) < Ο, 1, -1)) |
19 | 18 | fvmpt2 6964 |
. . . . . . 7
β’ ((π₯ β β β§ if((π₯ mod π) < Ο, 1, -1) β β) β
(πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
20 | 14, 17, 19 | sylancl 587 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)Ο)) β (πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
21 | 17 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)Ο)) β if((π₯ mod π) < Ο, 1, -1) β
β) |
22 | 21 | recnd 11190 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)Ο)) β if((π₯ mod π) < Ο, 1, -1) β
β) |
23 | 20, 22 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ π₯ β (-Ο(,)Ο)) β (πΉβπ₯) β β) |
24 | | sqwvfourb.n |
. . . . . . . . 9
β’ (π β π β β) |
25 | 24 | nncnd 12176 |
. . . . . . . 8
β’ (π β π β β) |
26 | 25 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)Ο)) β π β
β) |
27 | 14 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)Ο)) β π₯ β
β) |
28 | 26, 27 | mulcld 11182 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)Ο)) β (π Β· π₯) β β) |
29 | 28 | sincld 16019 |
. . . . 5
β’ ((π β§ π₯ β (-Ο(,)Ο)) β
(sinβ(π Β·
π₯)) β
β) |
30 | 23, 29 | mulcld 11182 |
. . . 4
β’ ((π β§ π₯ β (-Ο(,)Ο)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) β β) |
31 | | elioore 13301 |
. . . . . . . . . 10
β’ (π₯ β (-Ο(,)0) β π₯ β
β) |
32 | 31, 17, 19 | sylancl 587 |
. . . . . . . . 9
β’ (π₯ β (-Ο(,)0) β
(πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
33 | 1 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β Ο
β β) |
34 | | sqwvfourb.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 | 31, 40 | modcld 13787 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β
(π₯ mod π) β β) |
42 | | picn 25832 |
. . . . . . . . . . . . . . . . . 18
β’ Ο
β β |
43 | 42 | 2timesi 12298 |
. . . . . . . . . . . . . . . . 17
β’ (2
Β· Ο) = (Ο + Ο) |
44 | 34, 43 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
β’ π = (Ο +
Ο) |
45 | 44 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
β’ (-Ο +
π) = (-Ο + (Ο +
Ο)) |
46 | 2 | recni 11176 |
. . . . . . . . . . . . . . . 16
β’ -Ο
β β |
47 | 46, 42, 42 | addassi 11172 |
. . . . . . . . . . . . . . 15
β’ ((-Ο +
Ο) + Ο) = (-Ο + (Ο + Ο)) |
48 | 42 | negidi 11477 |
. . . . . . . . . . . . . . . . . 18
β’ (Ο +
-Ο) = 0 |
49 | 42, 46, 48 | addcomli 11354 |
. . . . . . . . . . . . . . . . 17
β’ (-Ο +
Ο) = 0 |
50 | 49 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’ ((-Ο +
Ο) + Ο) = (0 + Ο) |
51 | 42 | addid2i 11350 |
. . . . . . . . . . . . . . . 16
β’ (0 +
Ο) = Ο |
52 | 50, 51 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ ((-Ο +
Ο) + Ο) = Ο |
53 | 45, 47, 52 | 3eqtr2ri 2772 |
. . . . . . . . . . . . . 14
β’ Ο =
(-Ο + π) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β (-Ο(,)0) β Ο
= (-Ο + π)) |
55 | 2 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β -Ο
β β) |
56 | | 2re 12234 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
57 | 56, 1 | remulcli 11178 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· Ο) β β |
58 | 34, 57 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
β’ π β β |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β π β
β) |
60 | 2 | rexri 11220 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β* |
61 | | 0xr 11209 |
. . . . . . . . . . . . . . 15
β’ 0 β
β* |
62 | | ioogtlb 43807 |
. . . . . . . . . . . . . . 15
β’ ((-Ο
β β* β§ 0 β β* β§ π₯ β (-Ο(,)0)) β
-Ο < π₯) |
63 | 60, 61, 62 | mp3an12 1452 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β -Ο
< π₯) |
64 | 55, 31, 59, 63 | ltadd1dd 11773 |
. . . . . . . . . . . . 13
β’ (π₯ β (-Ο(,)0) β
(-Ο + π) < (π₯ + π)) |
65 | 54, 64 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (π₯ β (-Ο(,)0) β Ο
< (π₯ + π)) |
66 | 58 | recni 11176 |
. . . . . . . . . . . . . . . . 17
β’ π β β |
67 | 66 | mulid2i 11167 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· π) = π |
68 | 67 | eqcomi 2746 |
. . . . . . . . . . . . . . 15
β’ π = (1 Β· π) |
69 | 68 | oveq2i 7373 |
. . . . . . . . . . . . . 14
β’ (π₯ + π) = (π₯ + (1 Β· π)) |
70 | 69 | oveq1i 7372 |
. . . . . . . . . . . . 13
β’ ((π₯ + π) mod π) = ((π₯ + (1 Β· π)) mod π) |
71 | 31, 59 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) β β) |
72 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β 0
β β) |
73 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (-Ο(,)0) β 0
< Ο) |
74 | 72, 33, 71, 73, 65 | lttrd 11323 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β 0
< (π₯ + π)) |
75 | 72, 71, 74 | ltled 11310 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β 0
β€ (π₯ + π)) |
76 | | iooltub 43822 |
. . . . . . . . . . . . . . . . 17
β’ ((-Ο
β β* β§ 0 β β* β§ π₯ β (-Ο(,)0)) β
π₯ < 0) |
77 | 60, 61, 76 | mp3an12 1452 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (-Ο(,)0) β π₯ < 0) |
78 | 31, 72, 59, 77 | ltadd1dd 11773 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) < (0 + π)) |
79 | 59 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (-Ο(,)0) β π β
β) |
80 | 79 | addid2d 11363 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (-Ο(,)0) β (0 +
π) = π) |
81 | 78, 80 | breqtrd 5136 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) < π) |
82 | | modid 13808 |
. . . . . . . . . . . . . 14
β’ ((((π₯ + π) β β β§ π β β+) β§ (0 β€
(π₯ + π) β§ (π₯ + π) < π)) β ((π₯ + π) mod π) = (π₯ + π)) |
83 | 71, 40, 75, 81, 82 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ (π₯ β (-Ο(,)0) β
((π₯ + π) mod π) = (π₯ + π)) |
84 | | 1zzd 12541 |
. . . . . . . . . . . . . 14
β’ (π₯ β (-Ο(,)0) β 1
β β€) |
85 | | modcyc 13818 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π β β+
β§ 1 β β€) β ((π₯ + (1 Β· π)) mod π) = (π₯ mod π)) |
86 | 31, 40, 84, 85 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π₯ β (-Ο(,)0) β
((π₯ + (1 Β· π)) mod π) = (π₯ mod π)) |
87 | 70, 83, 86 | 3eqtr3a 2801 |
. . . . . . . . . . . 12
β’ (π₯ β (-Ο(,)0) β
(π₯ + π) = (π₯ mod π)) |
88 | 65, 87 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β Ο
< (π₯ mod π)) |
89 | 33, 41, 88 | ltnsymd 11311 |
. . . . . . . . . 10
β’ (π₯ β (-Ο(,)0) β Β¬
(π₯ mod π) < Ο) |
90 | 89 | iffalsed 4502 |
. . . . . . . . 9
β’ (π₯ β (-Ο(,)0) β
if((π₯ mod π) < Ο, 1, -1) = -1) |
91 | 32, 90 | eqtrd 2777 |
. . . . . . . 8
β’ (π₯ β (-Ο(,)0) β
(πΉβπ₯) = -1) |
92 | 91 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)0)) β (πΉβπ₯) = -1) |
93 | 92 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)0)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (-1 Β· (sinβ(π Β· π₯)))) |
94 | 93 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β (-Ο(,)0) β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) = (π₯ β (-Ο(,)0) β¦ (-1 Β·
(sinβ(π Β·
π₯))))) |
95 | | neg1cn 12274 |
. . . . . . 7
β’ -1 β
β |
96 | 95 | a1i 11 |
. . . . . 6
β’ (π β -1 β
β) |
97 | 24 | nnred 12175 |
. . . . . . . . 9
β’ (π β π β β) |
98 | 97 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο(,)0)) β π β β) |
99 | 31 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο(,)0)) β π₯ β
β) |
100 | 98, 99 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)0)) β (π Β· π₯) β β) |
101 | 100 | resincld 16032 |
. . . . . 6
β’ ((π β§ π₯ β (-Ο(,)0)) β (sinβ(π Β· π₯)) β β) |
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 | 97 | 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 | resincld 16032 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο[,]0)) β (sinβ(π Β· π₯)) β β) |
113 | | 0red 11165 |
. . . . . . . 8
β’ (π β 0 β
β) |
114 | | sincn 25819 |
. . . . . . . . . 10
β’ sin
β (ββcnββ) |
115 | 114 | a1i 11 |
. . . . . . . . 9
β’ (π β sin β
(ββcnββ)) |
116 | | ax-resscn 11115 |
. . . . . . . . . . . . 13
β’ β
β β |
117 | 108, 116 | sstri 3958 |
. . . . . . . . . . . 12
β’
(-Ο[,]0) β β |
118 | 117 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (-Ο[,]0) β
β) |
119 | | ssid 3971 |
. . . . . . . . . . . 12
β’ β
β β |
120 | 119 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β
β) |
121 | 118, 25, 120 | constcncfg 44187 |
. . . . . . . . . 10
β’ (π β (π₯ β (-Ο[,]0) β¦ π) β ((-Ο[,]0)βcnββ)) |
122 | 118, 120 | idcncfg 44188 |
. . . . . . . . . 10
β’ (π β (π₯ β (-Ο[,]0) β¦ π₯) β
((-Ο[,]0)βcnββ)) |
123 | 121, 122 | mulcncf 24826 |
. . . . . . . . 9
β’ (π β (π₯ β (-Ο[,]0) β¦ (π Β· π₯)) β ((-Ο[,]0)βcnββ)) |
124 | 115, 123 | cncfmpt1f 24293 |
. . . . . . . 8
β’ (π β (π₯ β (-Ο[,]0) β¦ (sinβ(π Β· π₯))) β ((-Ο[,]0)βcnββ)) |
125 | | cniccibl 25221 |
. . . . . . . 8
β’ ((-Ο
β β β§ 0 β β β§ (π₯ β (-Ο[,]0) β¦ (sinβ(π Β· π₯))) β ((-Ο[,]0)βcnββ)) β (π₯ β (-Ο[,]0) β¦ (sinβ(π Β· π₯))) β
πΏ1) |
126 | 3, 113, 124, 125 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β (-Ο[,]0) β¦ (sinβ(π Β· π₯))) β
πΏ1) |
127 | 103, 105,
112, 126 | iblss 25185 |
. . . . . 6
β’ (π β (π₯ β (-Ο(,)0) β¦ (sinβ(π Β· π₯))) β
πΏ1) |
128 | 96, 101, 127 | iblmulc2 25211 |
. . . . 5
β’ (π β (π₯ β (-Ο(,)0) β¦ (-1 Β·
(sinβ(π Β·
π₯)))) β
πΏ1) |
129 | 94, 128 | eqeltrd 2838 |
. . . 4
β’ (π β (π₯ β (-Ο(,)0) β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1) |
130 | 60 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β -Ο
β β*) |
131 | 1 | rexri 11220 |
. . . . . . . . . . . 12
β’ Ο
β β* |
132 | 131 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β Ο
β β*) |
133 | | elioore 13301 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β π₯ β
β) |
134 | 2 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β -Ο
β β) |
135 | | 0red 11165 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β 0
β β) |
136 | 6 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β -Ο
< 0) |
137 | | ioogtlb 43807 |
. . . . . . . . . . . . 13
β’ ((0
β β* β§ Ο β β* β§ π₯ β (0(,)Ο)) β 0
< π₯) |
138 | 61, 131, 137 | mp3an12 1452 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β 0 <
π₯) |
139 | 134, 135,
133, 136, 138 | lttrd 11323 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β -Ο
< π₯) |
140 | | iooltub 43822 |
. . . . . . . . . . . 12
β’ ((0
β β* β§ Ο β β* β§ π₯ β (0(,)Ο)) β π₯ < Ο) |
141 | 61, 131, 140 | mp3an12 1452 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β π₯ < Ο) |
142 | 130, 132,
133, 139, 141 | eliood 43810 |
. . . . . . . . . 10
β’ (π₯ β (0(,)Ο) β π₯ β
(-Ο(,)Ο)) |
143 | 142, 20 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π₯ β (0(,)Ο)) β (πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
144 | 39 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β π β
β+) |
145 | 135, 133,
138 | ltled 11310 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β 0 β€
π₯) |
146 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0(,)Ο) β Ο
β β) |
147 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0(,)Ο) β π β
β) |
148 | | 2timesgt 43596 |
. . . . . . . . . . . . . . . . 17
β’ (Ο
β β+ β Ο < (2 Β· Ο)) |
149 | 36, 148 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ Ο <
(2 Β· Ο) |
150 | 149, 34 | breqtrri 5137 |
. . . . . . . . . . . . . . 15
β’ Ο <
π |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0(,)Ο) β Ο
< π) |
152 | 133, 146,
147, 141, 151 | lttrd 11323 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)Ο) β π₯ < π) |
153 | | modid 13808 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§ π β β+)
β§ (0 β€ π₯ β§ π₯ < π)) β (π₯ mod π) = π₯) |
154 | 133, 144,
145, 152, 153 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)Ο) β (π₯ mod π) = π₯) |
155 | 154, 141 | eqbrtrd 5132 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β (π₯ mod π) < Ο) |
156 | 155 | iftrued 4499 |
. . . . . . . . . 10
β’ (π₯ β (0(,)Ο) β
if((π₯ mod π) < Ο, 1, -1) = 1) |
157 | 156 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (0(,)Ο)) β if((π₯ mod π) < Ο, 1, -1) = 1) |
158 | 143, 157 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π₯ β (0(,)Ο)) β (πΉβπ₯) = 1) |
159 | 158 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ π₯ β (0(,)Ο)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (1 Β· (sinβ(π Β· π₯)))) |
160 | 142, 29 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π₯ β (0(,)Ο)) β (sinβ(π Β· π₯)) β β) |
161 | 160 | mulid2d 11180 |
. . . . . . 7
β’ ((π β§ π₯ β (0(,)Ο)) β (1 Β·
(sinβ(π Β·
π₯))) = (sinβ(π Β· π₯))) |
162 | 159, 161 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π₯ β (0(,)Ο)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (sinβ(π Β· π₯))) |
163 | 162 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β (0(,)Ο) β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) = (π₯ β (0(,)Ο) β¦ (sinβ(π Β· π₯)))) |
164 | | ioossicc 13357 |
. . . . . . 7
β’
(0(,)Ο) β (0[,]Ο) |
165 | 164 | a1i 11 |
. . . . . 6
β’ (π β (0(,)Ο) β
(0[,]Ο)) |
166 | | ioombl 24945 |
. . . . . . 7
β’
(0(,)Ο) β dom vol |
167 | 166 | a1i 11 |
. . . . . 6
β’ (π β (0(,)Ο) β dom
vol) |
168 | 97 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (0[,]Ο)) β π β β) |
169 | | iccssre 13353 |
. . . . . . . . . . 11
β’ ((0
β β β§ Ο β β) β (0[,]Ο) β
β) |
170 | 5, 1, 169 | mp2an 691 |
. . . . . . . . . 10
β’
(0[,]Ο) β β |
171 | 170 | sseli 3945 |
. . . . . . . . 9
β’ (π₯ β (0[,]Ο) β π₯ β
β) |
172 | 171 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (0[,]Ο)) β π₯ β β) |
173 | 168, 172 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π₯ β (0[,]Ο)) β (π Β· π₯) β β) |
174 | 173 | resincld 16032 |
. . . . . 6
β’ ((π β§ π₯ β (0[,]Ο)) β (sinβ(π Β· π₯)) β β) |
175 | 170, 116 | sstri 3958 |
. . . . . . . . . . 11
β’
(0[,]Ο) β β |
176 | 175 | a1i 11 |
. . . . . . . . . 10
β’ (π β (0[,]Ο) β
β) |
177 | 176, 25, 120 | constcncfg 44187 |
. . . . . . . . 9
β’ (π β (π₯ β (0[,]Ο) β¦ π) β ((0[,]Ο)βcnββ)) |
178 | 176, 120 | idcncfg 44188 |
. . . . . . . . 9
β’ (π β (π₯ β (0[,]Ο) β¦ π₯) β ((0[,]Ο)βcnββ)) |
179 | 177, 178 | mulcncf 24826 |
. . . . . . . 8
β’ (π β (π₯ β (0[,]Ο) β¦ (π Β· π₯)) β ((0[,]Ο)βcnββ)) |
180 | 115, 179 | cncfmpt1f 24293 |
. . . . . . 7
β’ (π β (π₯ β (0[,]Ο) β¦ (sinβ(π Β· π₯))) β ((0[,]Ο)βcnββ)) |
181 | | cniccibl 25221 |
. . . . . . 7
β’ ((0
β β β§ Ο β β β§ (π₯ β (0[,]Ο) β¦ (sinβ(π Β· π₯))) β ((0[,]Ο)βcnββ)) β (π₯ β (0[,]Ο) β¦ (sinβ(π Β· π₯))) β
πΏ1) |
182 | 113, 4, 180, 181 | syl3anc 1372 |
. . . . . 6
β’ (π β (π₯ β (0[,]Ο) β¦ (sinβ(π Β· π₯))) β
πΏ1) |
183 | 165, 167,
174, 182 | iblss 25185 |
. . . . 5
β’ (π β (π₯ β (0(,)Ο) β¦ (sinβ(π Β· π₯))) β
πΏ1) |
184 | 163, 183 | eqeltrd 2838 |
. . . 4
β’ (π β (π₯ β (0(,)Ο) β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1) |
185 | 3, 4, 12, 30, 129, 184 | itgsplitioo 25218 |
. . 3
β’ (π β β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = (β«(-Ο(,)0)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯)) |
186 | 185 | oveq1d 7377 |
. 2
β’ (π β
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο) = ((β«(-Ο(,)0)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) / Ο)) |
187 | 91 | oveq1d 7377 |
. . . . . . . . 9
β’ (π₯ β (-Ο(,)0) β
((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (-1 Β· (sinβ(π Β· π₯)))) |
188 | 187 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο(,)0)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (-1 Β· (sinβ(π Β· π₯)))) |
189 | 60 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β -Ο
β β*) |
190 | 131 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β Ο
β β*) |
191 | 31, 72, 33, 77, 73 | lttrd 11323 |
. . . . . . . . . . 11
β’ (π₯ β (-Ο(,)0) β π₯ < Ο) |
192 | 189, 190,
31, 63, 191 | eliood 43810 |
. . . . . . . . . 10
β’ (π₯ β (-Ο(,)0) β π₯ β
(-Ο(,)Ο)) |
193 | 192, 29 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π₯ β (-Ο(,)0)) β (sinβ(π Β· π₯)) β β) |
194 | 193 | mulm1d 11614 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο(,)0)) β (-1 Β·
(sinβ(π Β·
π₯))) = -(sinβ(π Β· π₯))) |
195 | 188, 194 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π₯ β (-Ο(,)0)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = -(sinβ(π Β· π₯))) |
196 | 195 | itgeq2dv 25162 |
. . . . . 6
β’ (π β β«(-Ο(,)0)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = β«(-Ο(,)0)-(sinβ(π Β· π₯)) dπ₯) |
197 | 101, 127 | itgneg 25184 |
. . . . . 6
β’ (π β
-β«(-Ο(,)0)(sinβ(π Β· π₯)) dπ₯ = β«(-Ο(,)0)-(sinβ(π Β· π₯)) dπ₯) |
198 | 24 | nnne0d 12210 |
. . . . . . . . . 10
β’ (π β π β 0) |
199 | 7 | a1i 11 |
. . . . . . . . . 10
β’ (π β -Ο β€
0) |
200 | 25, 198, 3, 113, 199 | itgsincmulx 44289 |
. . . . . . . . 9
β’ (π β
β«(-Ο(,)0)(sinβ(π Β· π₯)) dπ₯ = (((cosβ(π Β· -Ο)) β (cosβ(π Β· 0))) / π)) |
201 | 24 | nnzd 12533 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
202 | | cosknegpi 44184 |
. . . . . . . . . . . . 13
β’ (π β β€ β
(cosβ(π Β·
-Ο)) = if(2 β₯ π,
1, -1)) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (cosβ(π Β· -Ο)) = if(2 β₯
π, 1, -1)) |
204 | 25 | mul01d 11361 |
. . . . . . . . . . . . . 14
β’ (π β (π Β· 0) = 0) |
205 | 204 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π β (cosβ(π Β· 0)) =
(cosβ0)) |
206 | | cos0 16039 |
. . . . . . . . . . . . 13
β’
(cosβ0) = 1 |
207 | 205, 206 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (π β (cosβ(π Β· 0)) =
1) |
208 | 203, 207 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π β ((cosβ(π Β· -Ο)) β
(cosβ(π Β· 0)))
= (if(2 β₯ π, 1, -1)
β 1)) |
209 | | 1m1e0 12232 |
. . . . . . . . . . . . 13
β’ (1
β 1) = 0 |
210 | | iftrue 4497 |
. . . . . . . . . . . . . 14
β’ (2
β₯ π β if(2
β₯ π, 1, -1) =
1) |
211 | 210 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (2
β₯ π β (if(2
β₯ π, 1, -1) β
1) = (1 β 1)) |
212 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (2
β₯ π β if(2
β₯ π, 0, -2) =
0) |
213 | 209, 211,
212 | 3eqtr4a 2803 |
. . . . . . . . . . . 12
β’ (2
β₯ π β (if(2
β₯ π, 1, -1) β
1) = if(2 β₯ π, 0,
-2)) |
214 | | iffalse 4500 |
. . . . . . . . . . . . . 14
β’ (Β¬ 2
β₯ π β if(2
β₯ π, 1, -1) =
-1) |
215 | 214 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (Β¬ 2
β₯ π β (if(2
β₯ π, 1, -1) β
1) = (-1 β 1)) |
216 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
217 | | negdi2 11466 |
. . . . . . . . . . . . . . . 16
β’ ((1
β β β§ 1 β β) β -(1 + 1) = (-1 β
1)) |
218 | 216, 216,
217 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ -(1 + 1)
= (-1 β 1) |
219 | 218 | eqcomi 2746 |
. . . . . . . . . . . . . 14
β’ (-1
β 1) = -(1 + 1) |
220 | 219 | a1i 11 |
. . . . . . . . . . . . 13
β’ (Β¬ 2
β₯ π β (-1
β 1) = -(1 + 1)) |
221 | | 1p1e2 12285 |
. . . . . . . . . . . . . . 15
β’ (1 + 1) =
2 |
222 | 221 | negeqi 11401 |
. . . . . . . . . . . . . 14
β’ -(1 + 1)
= -2 |
223 | | iffalse 4500 |
. . . . . . . . . . . . . 14
β’ (Β¬ 2
β₯ π β if(2
β₯ π, 0, -2) =
-2) |
224 | 222, 223 | eqtr4id 2796 |
. . . . . . . . . . . . 13
β’ (Β¬ 2
β₯ π β -(1 + 1) =
if(2 β₯ π, 0,
-2)) |
225 | 215, 220,
224 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ (Β¬ 2
β₯ π β (if(2
β₯ π, 1, -1) β
1) = if(2 β₯ π, 0,
-2)) |
226 | 213, 225 | pm2.61i 182 |
. . . . . . . . . . 11
β’ (if(2
β₯ π, 1, -1) β
1) = if(2 β₯ π, 0,
-2) |
227 | 208, 226 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π β ((cosβ(π Β· -Ο)) β
(cosβ(π Β· 0)))
= if(2 β₯ π, 0,
-2)) |
228 | 227 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β (((cosβ(π Β· -Ο)) β
(cosβ(π Β· 0)))
/ π) = (if(2 β₯ π, 0, -2) / π)) |
229 | 200, 228 | eqtrd 2777 |
. . . . . . . 8
β’ (π β
β«(-Ο(,)0)(sinβ(π Β· π₯)) dπ₯ = (if(2 β₯ π, 0, -2) / π)) |
230 | 229 | negeqd 11402 |
. . . . . . 7
β’ (π β
-β«(-Ο(,)0)(sinβ(π Β· π₯)) dπ₯ = -(if(2 β₯ π, 0, -2) / π)) |
231 | | 0cn 11154 |
. . . . . . . . . 10
β’ 0 β
β |
232 | | 2cn 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
233 | 232 | negcli 11476 |
. . . . . . . . . 10
β’ -2 β
β |
234 | 231, 233 | ifcli 4538 |
. . . . . . . . 9
β’ if(2
β₯ π, 0, -2) β
β |
235 | 234 | a1i 11 |
. . . . . . . 8
β’ (π β if(2 β₯ π, 0, -2) β
β) |
236 | 235, 25, 198 | divnegd 11951 |
. . . . . . 7
β’ (π β -(if(2 β₯ π, 0, -2) / π) = (-if(2 β₯ π, 0, -2) / π)) |
237 | | neg0 11454 |
. . . . . . . . . . 11
β’ -0 =
0 |
238 | 212 | negeqd 11402 |
. . . . . . . . . . 11
β’ (2
β₯ π β -if(2
β₯ π, 0, -2) =
-0) |
239 | | iftrue 4497 |
. . . . . . . . . . 11
β’ (2
β₯ π β if(2
β₯ π, 0, 2) =
0) |
240 | 237, 238,
239 | 3eqtr4a 2803 |
. . . . . . . . . 10
β’ (2
β₯ π β -if(2
β₯ π, 0, -2) = if(2
β₯ π, 0,
2)) |
241 | 232 | negnegi 11478 |
. . . . . . . . . . 11
β’ --2 =
2 |
242 | 223 | negeqd 11402 |
. . . . . . . . . . 11
β’ (Β¬ 2
β₯ π β -if(2
β₯ π, 0, -2) =
--2) |
243 | | iffalse 4500 |
. . . . . . . . . . 11
β’ (Β¬ 2
β₯ π β if(2
β₯ π, 0, 2) =
2) |
244 | 241, 242,
243 | 3eqtr4a 2803 |
. . . . . . . . . 10
β’ (Β¬ 2
β₯ π β -if(2
β₯ π, 0, -2) = if(2
β₯ π, 0,
2)) |
245 | 240, 244 | pm2.61i 182 |
. . . . . . . . 9
β’ -if(2
β₯ π, 0, -2) = if(2
β₯ π, 0,
2) |
246 | 245 | oveq1i 7372 |
. . . . . . . 8
β’ (-if(2
β₯ π, 0, -2) / π) = (if(2 β₯ π, 0, 2) / π) |
247 | 246 | a1i 11 |
. . . . . . 7
β’ (π β (-if(2 β₯ π, 0, -2) / π) = (if(2 β₯ π, 0, 2) / π)) |
248 | 230, 236,
247 | 3eqtrd 2781 |
. . . . . 6
β’ (π β
-β«(-Ο(,)0)(sinβ(π Β· π₯)) dπ₯ = (if(2 β₯ π, 0, 2) / π)) |
249 | 196, 197,
248 | 3eqtr2d 2783 |
. . . . 5
β’ (π β β«(-Ο(,)0)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = (if(2 β₯ π, 0, 2) / π)) |
250 | 133, 17, 19 | sylancl 587 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)Ο) β (πΉβπ₯) = if((π₯ mod π) < Ο, 1, -1)) |
251 | 250, 156 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π₯ β (0(,)Ο) β (πΉβπ₯) = 1) |
252 | 251 | oveq1d 7377 |
. . . . . . . . 9
β’ (π₯ β (0(,)Ο) β
((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (1 Β· (sinβ(π Β· π₯)))) |
253 | 252 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (0(,)Ο)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (1 Β· (sinβ(π Β· π₯)))) |
254 | 253, 161 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π₯ β (0(,)Ο)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = (sinβ(π Β· π₯))) |
255 | 254 | itgeq2dv 25162 |
. . . . . 6
β’ (π β β«(0(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = β«(0(,)Ο)(sinβ(π Β· π₯)) dπ₯) |
256 | 9 | a1i 11 |
. . . . . . 7
β’ (π β 0 β€
Ο) |
257 | 25, 198, 113, 4, 256 | itgsincmulx 44289 |
. . . . . 6
β’ (π β
β«(0(,)Ο)(sinβ(π Β· π₯)) dπ₯ = (((cosβ(π Β· 0)) β (cosβ(π Β· Ο))) / π)) |
258 | | coskpi2 44181 |
. . . . . . . . . 10
β’ (π β β€ β
(cosβ(π Β·
Ο)) = if(2 β₯ π, 1,
-1)) |
259 | 201, 258 | syl 17 |
. . . . . . . . 9
β’ (π β (cosβ(π Β· Ο)) = if(2 β₯
π, 1, -1)) |
260 | 207, 259 | oveq12d 7380 |
. . . . . . . 8
β’ (π β ((cosβ(π Β· 0)) β
(cosβ(π Β·
Ο))) = (1 β if(2 β₯ π, 1, -1))) |
261 | 210 | oveq2d 7378 |
. . . . . . . . . 10
β’ (2
β₯ π β (1 β
if(2 β₯ π, 1, -1)) =
(1 β 1)) |
262 | 209, 261,
239 | 3eqtr4a 2803 |
. . . . . . . . 9
β’ (2
β₯ π β (1 β
if(2 β₯ π, 1, -1)) =
if(2 β₯ π, 0,
2)) |
263 | 214 | oveq2d 7378 |
. . . . . . . . . 10
β’ (Β¬ 2
β₯ π β (1 β
if(2 β₯ π, 1, -1)) =
(1 β -1)) |
264 | 216, 216 | subnegi 11487 |
. . . . . . . . . . 11
β’ (1
β -1) = (1 + 1) |
265 | 264 | a1i 11 |
. . . . . . . . . 10
β’ (Β¬ 2
β₯ π β (1 β
-1) = (1 + 1)) |
266 | 221, 243 | eqtr4id 2796 |
. . . . . . . . . 10
β’ (Β¬ 2
β₯ π β (1 + 1) =
if(2 β₯ π, 0,
2)) |
267 | 263, 265,
266 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (Β¬ 2
β₯ π β (1 β
if(2 β₯ π, 1, -1)) =
if(2 β₯ π, 0,
2)) |
268 | 262, 267 | pm2.61i 182 |
. . . . . . . 8
β’ (1
β if(2 β₯ π, 1,
-1)) = if(2 β₯ π, 0,
2) |
269 | 260, 268 | eqtrdi 2793 |
. . . . . . 7
β’ (π β ((cosβ(π Β· 0)) β
(cosβ(π Β·
Ο))) = if(2 β₯ π,
0, 2)) |
270 | 269 | oveq1d 7377 |
. . . . . 6
β’ (π β (((cosβ(π Β· 0)) β
(cosβ(π Β·
Ο))) / π) = (if(2
β₯ π, 0, 2) / π)) |
271 | 255, 257,
270 | 3eqtrd 2781 |
. . . . 5
β’ (π β β«(0(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = (if(2 β₯ π, 0, 2) / π)) |
272 | 249, 271 | oveq12d 7380 |
. . . 4
β’ (π β (β«(-Ο(,)0)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) = ((if(2 β₯ π, 0, 2) / π) + (if(2 β₯ π, 0, 2) / π))) |
273 | 231, 232 | ifcli 4538 |
. . . . . 6
β’ if(2
β₯ π, 0, 2) β
β |
274 | 273 | a1i 11 |
. . . . 5
β’ (π β if(2 β₯ π, 0, 2) β
β) |
275 | 274, 274,
25, 198 | divdird 11976 |
. . . 4
β’ (π β ((if(2 β₯ π, 0, 2) + if(2 β₯ π, 0, 2)) / π) = ((if(2 β₯ π, 0, 2) / π) + (if(2 β₯ π, 0, 2) / π))) |
276 | 239, 239 | oveq12d 7380 |
. . . . . . . . 9
β’ (2
β₯ π β (if(2
β₯ π, 0, 2) + if(2
β₯ π, 0, 2)) = (0 +
0)) |
277 | | 00id 11337 |
. . . . . . . . 9
β’ (0 + 0) =
0 |
278 | 276, 277 | eqtrdi 2793 |
. . . . . . . 8
β’ (2
β₯ π β (if(2
β₯ π, 0, 2) + if(2
β₯ π, 0, 2)) =
0) |
279 | 278 | oveq1d 7377 |
. . . . . . 7
β’ (2
β₯ π β ((if(2
β₯ π, 0, 2) + if(2
β₯ π, 0, 2)) / π) = (0 / π)) |
280 | 279 | adantl 483 |
. . . . . 6
β’ ((π β§ 2 β₯ π) β ((if(2 β₯ π, 0, 2) + if(2 β₯ π, 0, 2)) / π) = (0 / π)) |
281 | 25, 198 | div0d 11937 |
. . . . . . 7
β’ (π β (0 / π) = 0) |
282 | 281 | adantr 482 |
. . . . . 6
β’ ((π β§ 2 β₯ π) β (0 / π) = 0) |
283 | | iftrue 4497 |
. . . . . . . 8
β’ (2
β₯ π β if(2
β₯ π, 0, (4 / π)) = 0) |
284 | 283 | eqcomd 2743 |
. . . . . . 7
β’ (2
β₯ π β 0 = if(2
β₯ π, 0, (4 / π))) |
285 | 284 | adantl 483 |
. . . . . 6
β’ ((π β§ 2 β₯ π) β 0 = if(2 β₯ π, 0, (4 / π))) |
286 | 280, 282,
285 | 3eqtrd 2781 |
. . . . 5
β’ ((π β§ 2 β₯ π) β ((if(2 β₯ π, 0, 2) + if(2 β₯ π, 0, 2)) / π) = if(2 β₯ π, 0, (4 / π))) |
287 | 243, 243 | oveq12d 7380 |
. . . . . . . . 9
β’ (Β¬ 2
β₯ π β (if(2
β₯ π, 0, 2) + if(2
β₯ π, 0, 2)) = (2 +
2)) |
288 | | 2p2e4 12295 |
. . . . . . . . 9
β’ (2 + 2) =
4 |
289 | 287, 288 | eqtrdi 2793 |
. . . . . . . 8
β’ (Β¬ 2
β₯ π β (if(2
β₯ π, 0, 2) + if(2
β₯ π, 0, 2)) =
4) |
290 | 289 | oveq1d 7377 |
. . . . . . 7
β’ (Β¬ 2
β₯ π β ((if(2
β₯ π, 0, 2) + if(2
β₯ π, 0, 2)) / π) = (4 / π)) |
291 | | iffalse 4500 |
. . . . . . 7
β’ (Β¬ 2
β₯ π β if(2
β₯ π, 0, (4 / π)) = (4 / π)) |
292 | 290, 291 | eqtr4d 2780 |
. . . . . 6
β’ (Β¬ 2
β₯ π β ((if(2
β₯ π, 0, 2) + if(2
β₯ π, 0, 2)) / π) = if(2 β₯ π, 0, (4 / π))) |
293 | 292 | adantl 483 |
. . . . 5
β’ ((π β§ Β¬ 2 β₯ π) β ((if(2 β₯ π, 0, 2) + if(2 β₯ π, 0, 2)) / π) = if(2 β₯ π, 0, (4 / π))) |
294 | 286, 293 | pm2.61dan 812 |
. . . 4
β’ (π β ((if(2 β₯ π, 0, 2) + if(2 β₯ π, 0, 2)) / π) = if(2 β₯ π, 0, (4 / π))) |
295 | 272, 275,
294 | 3eqtr2d 2783 |
. . 3
β’ (π β (β«(-Ο(,)0)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) = if(2 β₯ π, 0, (4 / π))) |
296 | 295 | oveq1d 7377 |
. 2
β’ (π β ((β«(-Ο(,)0)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ + β«(0(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) / Ο) = (if(2 β₯ π, 0, (4 / π)) / Ο)) |
297 | 283 | oveq1d 7377 |
. . . . 5
β’ (2
β₯ π β (if(2
β₯ π, 0, (4 / π)) / Ο) = (0 /
Ο)) |
298 | 297 | adantl 483 |
. . . 4
β’ ((π β§ 2 β₯ π) β (if(2 β₯ π, 0, (4 / π)) / Ο) = (0 / Ο)) |
299 | 5, 8 | gtneii 11274 |
. . . . . 6
β’ Ο β
0 |
300 | 42, 299 | div0i 11896 |
. . . . 5
β’ (0 /
Ο) = 0 |
301 | 300 | a1i 11 |
. . . 4
β’ ((π β§ 2 β₯ π) β (0 / Ο) = 0) |
302 | | iftrue 4497 |
. . . . . 6
β’ (2
β₯ π β if(2
β₯ π, 0, (4 / (π Β· Ο))) =
0) |
303 | 302 | eqcomd 2743 |
. . . . 5
β’ (2
β₯ π β 0 = if(2
β₯ π, 0, (4 / (π Β·
Ο)))) |
304 | 303 | adantl 483 |
. . . 4
β’ ((π β§ 2 β₯ π) β 0 = if(2 β₯ π, 0, (4 / (π Β· Ο)))) |
305 | 298, 301,
304 | 3eqtrd 2781 |
. . 3
β’ ((π β§ 2 β₯ π) β (if(2 β₯ π, 0, (4 / π)) / Ο) = if(2 β₯ π, 0, (4 / (π Β· Ο)))) |
306 | 291 | oveq1d 7377 |
. . . . 5
β’ (Β¬ 2
β₯ π β (if(2
β₯ π, 0, (4 / π)) / Ο) = ((4 / π) / Ο)) |
307 | 306 | adantl 483 |
. . . 4
β’ ((π β§ Β¬ 2 β₯ π) β (if(2 β₯ π, 0, (4 / π)) / Ο) = ((4 / π) / Ο)) |
308 | | 4cn 12245 |
. . . . . . 7
β’ 4 β
β |
309 | 308 | a1i 11 |
. . . . . 6
β’ (π β 4 β
β) |
310 | 42 | a1i 11 |
. . . . . 6
β’ (π β Ο β
β) |
311 | 299 | a1i 11 |
. . . . . 6
β’ (π β Ο β
0) |
312 | 309, 25, 310, 198, 311 | divdiv1d 11969 |
. . . . 5
β’ (π β ((4 / π) / Ο) = (4 / (π Β· Ο))) |
313 | 312 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ 2 β₯ π) β ((4 / π) / Ο) = (4 / (π Β· Ο))) |
314 | | iffalse 4500 |
. . . . . 6
β’ (Β¬ 2
β₯ π β if(2
β₯ π, 0, (4 / (π Β· Ο))) = (4 / (π Β·
Ο))) |
315 | 314 | eqcomd 2743 |
. . . . 5
β’ (Β¬ 2
β₯ π β (4 /
(π Β· Ο)) = if(2
β₯ π, 0, (4 / (π Β·
Ο)))) |
316 | 315 | adantl 483 |
. . . 4
β’ ((π β§ Β¬ 2 β₯ π) β (4 / (π Β· Ο)) = if(2 β₯ π, 0, (4 / (π Β· Ο)))) |
317 | 307, 313,
316 | 3eqtrd 2781 |
. . 3
β’ ((π β§ Β¬ 2 β₯ π) β (if(2 β₯ π, 0, (4 / π)) / Ο) = if(2 β₯ π, 0, (4 / (π Β· Ο)))) |
318 | 305, 317 | pm2.61dan 812 |
. 2
β’ (π β (if(2 β₯ π, 0, (4 / π)) / Ο) = if(2 β₯ π, 0, (4 / (π Β· Ο)))) |
319 | 186, 296,
318 | 3eqtrd 2781 |
1
β’ (π β
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο) = if(2 β₯ π, 0, (4 / (π Β· Ο)))) |