Step | Hyp | Ref
| Expression |
1 | | fourierdlem78.g |
. . . . 5
β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ )))) |
3 | 2 | reseq1d 5940 |
. . 3
β’ (π β (πΊ βΎ (π΄(,)π΅)) = ((π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) βΎ (π΄(,)π΅))) |
4 | | pire 25838 |
. . . . . . . . 9
β’ Ο
β β |
5 | 4 | renegcli 11470 |
. . . . . . . 8
β’ -Ο
β β |
6 | 5 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β -Ο β
β) |
7 | 4 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β Ο β
β) |
8 | | elioore 13303 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β π β β) |
9 | 8 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
10 | 5 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β -Ο β
β) |
11 | 4 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β Ο β
β) |
12 | 10, 11 | iccssred 13360 |
. . . . . . . . . . 11
β’ (π β (-Ο[,]Ο) β
β) |
13 | | fourierdlem78.a |
. . . . . . . . . . 11
β’ (π β π΄ β (-Ο[,]Ο)) |
14 | 12, 13 | sseldd 3949 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
15 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β β) |
16 | 5, 4 | elicc2i 13339 |
. . . . . . . . . . . 12
β’ (π΄ β (-Ο[,]Ο) β
(π΄ β β β§
-Ο β€ π΄ β§ π΄ β€ Ο)) |
17 | 16 | simp2bi 1147 |
. . . . . . . . . . 11
β’ (π΄ β (-Ο[,]Ο) β
-Ο β€ π΄) |
18 | 13, 17 | syl 17 |
. . . . . . . . . 10
β’ (π β -Ο β€ π΄) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β -Ο β€ π΄) |
20 | 15 | rexrd 11213 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β
β*) |
21 | | fourierdlem78.b |
. . . . . . . . . . . . 13
β’ (π β π΅ β (-Ο[,]Ο)) |
22 | 12, 21 | sseldd 3949 |
. . . . . . . . . . . 12
β’ (π β π΅ β β) |
23 | 22 | rexrd 11213 |
. . . . . . . . . . 11
β’ (π β π΅ β
β*) |
24 | 23 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β
β*) |
25 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π β (π΄(,)π΅)) |
26 | | ioogtlb 43823 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π΄ < π ) |
27 | 20, 24, 25, 26 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΄ < π ) |
28 | 6, 15, 9, 19, 27 | lelttrd 11321 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β -Ο < π ) |
29 | 6, 9, 28 | ltled 11311 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β -Ο β€ π ) |
30 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β β) |
31 | | iooltub 43838 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π < π΅) |
32 | 20, 24, 25, 31 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π < π΅) |
33 | 5, 4 | elicc2i 13339 |
. . . . . . . . . . . 12
β’ (π΅ β (-Ο[,]Ο) β
(π΅ β β β§
-Ο β€ π΅ β§ π΅ β€ Ο)) |
34 | 33 | simp3bi 1148 |
. . . . . . . . . . 11
β’ (π΅ β (-Ο[,]Ο) β
π΅ β€
Ο) |
35 | 21, 34 | syl 17 |
. . . . . . . . . 10
β’ (π β π΅ β€ Ο) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β€ Ο) |
37 | 9, 30, 7, 32, 36 | ltletrd 11323 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β π < Ο) |
38 | 9, 7, 37 | ltled 11311 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β π β€ Ο) |
39 | 6, 7, 9, 29, 38 | eliccd 43832 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π β (-Ο[,]Ο)) |
40 | 39 | ex 414 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β π β (-Ο[,]Ο))) |
41 | 40 | ssrdv 3954 |
. . . 4
β’ (π β (π΄(,)π΅) β (-Ο[,]Ο)) |
42 | 41 | resmptd 5998 |
. . 3
β’ (π β ((π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) βΎ (π΄(,)π΅)) = (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ )))) |
43 | 3, 42 | eqtrd 2773 |
. 2
β’ (π β (πΊ βΎ (π΄(,)π΅)) = (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ )))) |
44 | | 0red 11166 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β 0 β β) |
45 | | fourierdlem78.f |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆβ) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(,)π΅)) β πΉ:ββΆβ) |
47 | | fourierdlem78.x |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
49 | 48, 9 | readdcld 11192 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β β) |
50 | 46, 49 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) β β) |
51 | | fourierdlem78.y |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
52 | | fourierdlem78.w |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
53 | 51, 52 | ifcld 4536 |
. . . . . . . . . . . . . 14
β’ (π β if(0 < π , π, π) β β) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β if(0 < π , π, π) β β) |
55 | 50, 54 | resubcld 11591 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
56 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (π β (π΄(,)π΅) β 0 β (π΄(,)π΅))) |
57 | 56 | biimpac 480 |
. . . . . . . . . . . . . . 15
β’ ((π β (π΄(,)π΅) β§ π = 0) β 0 β (π΄(,)π΅)) |
58 | 57 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄(,)π΅)) β§ π = 0) β 0 β (π΄(,)π΅)) |
59 | | fourierdlem78.nxelab |
. . . . . . . . . . . . . . 15
β’ (π β Β¬ 0 β (π΄(,)π΅)) |
60 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄(,)π΅)) β§ π = 0) β Β¬ 0 β (π΄(,)π΅)) |
61 | 58, 60 | pm2.65da 816 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β Β¬ π = 0) |
62 | 61 | neqned 2947 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β π β 0) |
63 | 55, 9, 62 | redivcld 11991 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (((πΉβ(π + π )) β if(0 < π , π, π)) / π ) β β) |
64 | 44, 63 | ifcld 4536 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) β β) |
65 | | fourierdlem78.h |
. . . . . . . . . . 11
β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
66 | 65 | fvmpt2 6963 |
. . . . . . . . . 10
β’ ((π β (-Ο[,]Ο) β§
if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) β β) β (π»βπ ) = if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
67 | 39, 64, 66 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (π»βπ ) = if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
68 | 67, 64 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β (π»βπ ) β β) |
69 | | 1red 11164 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β 1 β β) |
70 | | 2re 12235 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
71 | 70 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β 2 β β) |
72 | 9 | rehalfcld 12408 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(,)π΅)) β (π / 2) β β) |
73 | 72 | resincld 16033 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β (sinβ(π / 2)) β β) |
74 | 71, 73 | remulcld 11193 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β (2 Β· (sinβ(π / 2))) β
β) |
75 | 71 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β 2 β β) |
76 | 73 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β (sinβ(π / 2)) β β) |
77 | | 2ne0 12265 |
. . . . . . . . . . . . . 14
β’ 2 β
0 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β 2 β 0) |
79 | | fourierdlem44 44482 |
. . . . . . . . . . . . . 14
β’ ((π β (-Ο[,]Ο) β§
π β 0) β
(sinβ(π / 2)) β
0) |
80 | 39, 62, 79 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β (sinβ(π / 2)) β 0) |
81 | 75, 76, 78, 80 | mulne0d 11815 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β (2 Β· (sinβ(π / 2))) β 0) |
82 | 9, 74, 81 | redivcld 11991 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (π / (2 Β· (sinβ(π / 2)))) β β) |
83 | 69, 82 | ifcld 4536 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))) β β) |
84 | | fourierdlem78.k |
. . . . . . . . . . 11
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
85 | 84 | fvmpt2 6963 |
. . . . . . . . . 10
β’ ((π β (-Ο[,]Ο) β§
if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))) β β) β
(πΎβπ ) = if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
86 | 39, 83, 85 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (πΎβπ ) = if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
87 | 86, 83 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β (πΎβπ ) β β) |
88 | 68, 87 | remulcld 11193 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β ((π»βπ ) Β· (πΎβπ )) β β) |
89 | | fourierdlem78.u |
. . . . . . . 8
β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) |
90 | 89 | fvmpt2 6963 |
. . . . . . 7
β’ ((π β (-Ο[,]Ο) β§
((π»βπ ) Β· (πΎβπ )) β β) β (πβπ ) = ((π»βπ ) Β· (πΎβπ ))) |
91 | 39, 88, 90 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β (πβπ ) = ((π»βπ ) Β· (πΎβπ ))) |
92 | 91, 88 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (πβπ ) β β) |
93 | | fourierdlem78.n |
. . . . . . . . . . 11
β’ (π β π β β) |
94 | 93 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
95 | 71, 78 | rereccld 11990 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (1 / 2) β
β) |
96 | 94, 95 | readdcld 11192 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (π + (1 / 2)) β β) |
97 | 96, 9 | remulcld 11193 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β ((π + (1 / 2)) Β· π ) β β) |
98 | 97 | resincld 16033 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β (sinβ((π + (1 / 2)) Β· π )) β β) |
99 | | fourierdlem78.s |
. . . . . . . 8
β’ π = (π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π ))) |
100 | 99 | fvmpt2 6963 |
. . . . . . 7
β’ ((π β (-Ο[,]Ο) β§
(sinβ((π + (1 / 2))
Β· π )) β
β) β (πβπ ) = (sinβ((π + (1 / 2)) Β· π ))) |
101 | 39, 98, 100 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β (πβπ ) = (sinβ((π + (1 / 2)) Β· π ))) |
102 | 101, 98 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (πβπ ) β β) |
103 | 92, 102 | remulcld 11193 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β ((πβπ ) Β· (πβπ )) β β) |
104 | | eqid 2733 |
. . . 4
β’ (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))) = (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))) |
105 | 103, 104 | fmptd 7066 |
. . 3
β’ (π β (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))):(π΄(,)π΅)βΆβ) |
106 | | ax-resscn 11116 |
. . . . 5
β’ β
β β |
107 | 106 | a1i 11 |
. . . 4
β’ (π β β β
β) |
108 | 91 | mpteq2dva 5209 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ (πβπ )) = (π β (π΄(,)π΅) β¦ ((π»βπ ) Β· (πΎβπ )))) |
109 | 61 | iffalsed 4501 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) = (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) |
110 | 55 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
111 | 9 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
112 | 110, 111,
62 | divrecd 11942 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (((πΉβ(π + π )) β if(0 < π , π, π)) / π ) = (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π ))) |
113 | 67, 109, 112 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (π»βπ ) = (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π ))) |
114 | 113 | mpteq2dva 5209 |
. . . . . . . 8
β’ (π β (π β (π΄(,)π΅) β¦ (π»βπ )) = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π )))) |
115 | 50 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) β β) |
116 | 54 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β if(0 < π , π, π) β β) |
117 | 115, 116 | negsubd 11526 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) + -if(0 < π , π, π)) = ((πΉβ(π + π )) β if(0 < π , π, π))) |
118 | 117 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β if(0 < π , π, π)) = ((πΉβ(π + π )) + -if(0 < π , π, π))) |
119 | 118 | mpteq2dva 5209 |
. . . . . . . . . 10
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) = (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) + -if(0 < π , π, π)))) |
120 | 14, 47 | readdcld 11192 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ + π) β β) |
121 | 120 | rexrd 11213 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ + π) β
β*) |
122 | 121 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄(,)π΅)) β (π΄ + π) β
β*) |
123 | 22, 47 | readdcld 11192 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΅ + π) β β) |
124 | 123 | rexrd 11213 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅ + π) β
β*) |
125 | 124 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄(,)π΅)) β (π΅ + π) β
β*) |
126 | 14 | recnd 11191 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β β) |
127 | 47 | recnd 11191 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
128 | 126, 127 | addcomd 11365 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ + π) = (π + π΄)) |
129 | 128 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄(,)π΅)) β (π΄ + π) = (π + π΄)) |
130 | 15, 9, 48, 27 | ltadd2dd 11322 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΄) < (π + π )) |
131 | 129, 130 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄(,)π΅)) β (π΄ + π) < (π + π )) |
132 | 9, 30, 48, 32 | ltadd2dd 11322 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) < (π + π΅)) |
133 | 22 | recnd 11191 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β β) |
134 | 127, 133 | addcomd 11365 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π + π΅) = (π΅ + π)) |
135 | 134 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΅) = (π΅ + π)) |
136 | 132, 135 | breqtrd 5135 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) < (π΅ + π)) |
137 | 122, 125,
49, 131, 136 | eliood 43826 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β ((π΄ + π)(,)(π΅ + π))) |
138 | | fvres 6865 |
. . . . . . . . . . . . . . 15
β’ ((π + π ) β ((π΄ + π)(,)(π΅ + π)) β ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π )) = (πΉβ(π + π ))) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π )) = (πΉβ(π + π ))) |
140 | 139 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) = ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π ))) |
141 | 140 | mpteq2dva 5209 |
. . . . . . . . . . . 12
β’ (π β (π β (π΄(,)π΅) β¦ (πΉβ(π + π ))) = (π β (π΄(,)π΅) β¦ ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π )))) |
142 | | ioosscn 13335 |
. . . . . . . . . . . . . 14
β’ ((π΄ + π)(,)(π΅ + π)) β β |
143 | 142 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β ((π΄ + π)(,)(π΅ + π)) β β) |
144 | | fourierdlem78.fcn |
. . . . . . . . . . . . 13
β’ (π β (πΉ βΎ ((π΄ + π)(,)(π΅ + π))) β (((π΄ + π)(,)(π΅ + π))βcnββ)) |
145 | | ioosscn 13335 |
. . . . . . . . . . . . . 14
β’ (π΄(,)π΅) β β |
146 | 145 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (π΄(,)π΅) β β) |
147 | 143, 144,
146, 127, 137 | fourierdlem23 44461 |
. . . . . . . . . . . 12
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π ))) β ((π΄(,)π΅)βcnββ)) |
148 | 141, 147 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π β (π β (π΄(,)π΅) β¦ (πΉβ(π + π ))) β ((π΄(,)π΅)βcnββ)) |
149 | | 0red 11166 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β 0 β β) |
150 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β π΄ β β) |
151 | 8 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β π β β) |
152 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β 0 β€ π΄) |
153 | 27 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β π΄ < π ) |
154 | 149, 150,
151, 152, 153 | lelttrd 11321 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β 0 < π ) |
155 | 154 | iftrued 4498 |
. . . . . . . . . . . . . . 15
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β if(0 < π , π, π) = π) |
156 | 155 | negeqd 11403 |
. . . . . . . . . . . . . 14
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β -if(0 < π , π, π) = -π) |
157 | 156 | mpteq2dva 5209 |
. . . . . . . . . . . . 13
β’ ((π β§ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) = (π β (π΄(,)π΅) β¦ -π)) |
158 | 51 | renegcld 11590 |
. . . . . . . . . . . . . . . 16
β’ (π β -π β β) |
159 | 158 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (π β -π β β) |
160 | | ssid 3970 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β β β
β) |
162 | 146, 159,
161 | constcncfg 44203 |
. . . . . . . . . . . . . 14
β’ (π β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
164 | 157, 163 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ ((π β§ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
165 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ 0 β€ π΄) β π) |
166 | 14 | rexrd 11213 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β
β*) |
167 | 166 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β π΄ β
β*) |
168 | 23 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β π΅ β
β*) |
169 | | 0red 11166 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β 0 β
β) |
170 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ 0 β€ π΄) β Β¬ 0 β€ π΄) |
171 | 14 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ 0 β€ π΄) β π΄ β β) |
172 | | 0red 11166 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ 0 β€ π΄) β 0 β
β) |
173 | 171, 172 | ltnled 11310 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ 0 β€ π΄) β (π΄ < 0 β Β¬ 0 β€ π΄)) |
174 | 170, 173 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ 0 β€ π΄) β π΄ < 0) |
175 | 174 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β π΄ < 0) |
176 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ π΅ β€ 0) β Β¬ π΅ β€ 0) |
177 | | 0red 11166 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ π΅ β€ 0) β 0 β
β) |
178 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ π΅ β€ 0) β π΅ β β) |
179 | 177, 178 | ltnled 11310 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ π΅ β€ 0) β (0 < π΅ β Β¬ π΅ β€ 0)) |
180 | 176, 179 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ π΅ β€ 0) β 0 < π΅) |
181 | 180 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β 0 < π΅) |
182 | 167, 168,
169, 175, 181 | eliood 43826 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β 0 β (π΄(,)π΅)) |
183 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β Β¬ 0 β (π΄(,)π΅)) |
184 | 182, 183 | condan 817 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ 0 β€ π΄) β π΅ β€ 0) |
185 | 8 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π β β) |
186 | | 0red 11166 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β 0 β β) |
187 | 22 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π΅ β β) |
188 | 32 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π < π΅) |
189 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π΅ β€ 0) |
190 | 185, 187,
186, 188, 189 | ltletrd 11323 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π < 0) |
191 | 185, 186,
190 | ltnsymd 11312 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β Β¬ 0 < π ) |
192 | 191 | iffalsed 4501 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β if(0 < π , π, π) = π) |
193 | 192 | negeqd 11403 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β -if(0 < π , π, π) = -π) |
194 | 193 | mpteq2dva 5209 |
. . . . . . . . . . . . . 14
β’ ((π β§ π΅ β€ 0) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) = (π β (π΄(,)π΅) β¦ -π)) |
195 | 52 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
196 | 195 | negcld 11507 |
. . . . . . . . . . . . . . . 16
β’ (π β -π β β) |
197 | 146, 196,
161 | constcncfg 44203 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
198 | 197 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π΅ β€ 0) β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
199 | 194, 198 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π΅ β€ 0) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
200 | 165, 184,
199 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
201 | 164, 200 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ (π β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
202 | 148, 201 | addcncf 24831 |
. . . . . . . . . 10
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) + -if(0 < π , π, π))) β ((π΄(,)π΅)βcnββ)) |
203 | 119, 202 | eqeltrd 2834 |
. . . . . . . . 9
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) β ((π΄(,)π΅)βcnββ)) |
204 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β (β β {0})
β¦ (1 / π )) = (π β (β β {0})
β¦ (1 / π )) |
205 | | 1cnd 11158 |
. . . . . . . . . . 11
β’ (π β 1 β
β) |
206 | 204 | cdivcncf 24307 |
. . . . . . . . . . 11
β’ (1 β
β β (π β
(β β {0}) β¦ (1 / π )) β ((β β {0})βcnββ)) |
207 | 205, 206 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β (β β {0}) β¦ (1 /
π )) β ((β
β {0})βcnββ)) |
208 | | velsn 4606 |
. . . . . . . . . . . . . 14
β’ (π β {0} β π = 0) |
209 | 61, 208 | sylnibr 329 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΄(,)π΅)) β Β¬ π β {0}) |
210 | 111, 209 | eldifd 3925 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄(,)π΅)) β π β (β β
{0})) |
211 | 210 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ β (π΄(,)π΅)π β (β β
{0})) |
212 | | dfss3 3936 |
. . . . . . . . . . 11
β’ ((π΄(,)π΅) β (β β {0}) β
βπ β (π΄(,)π΅)π β (β β
{0})) |
213 | 211, 212 | sylibr 233 |
. . . . . . . . . 10
β’ (π β (π΄(,)π΅) β (β β
{0})) |
214 | 9, 62 | rereccld 11990 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (1 / π ) β β) |
215 | 214 | recnd 11191 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (1 / π ) β β) |
216 | 204, 207,
213, 161, 215 | cncfmptssg 44202 |
. . . . . . . . 9
β’ (π β (π β (π΄(,)π΅) β¦ (1 / π )) β ((π΄(,)π΅)βcnββ)) |
217 | 203, 216 | mulcncf 24833 |
. . . . . . . 8
β’ (π β (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π ))) β ((π΄(,)π΅)βcnββ)) |
218 | 114, 217 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (π β (π΄(,)π΅) β¦ (π»βπ )) β ((π΄(,)π΅)βcnββ)) |
219 | 61 | iffalsed 4501 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))) = (π / (2 Β· (sinβ(π / 2))))) |
220 | 74 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (2 Β· (sinβ(π / 2))) β
β) |
221 | 111, 220,
81 | divrecd 11942 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (π / (2 Β· (sinβ(π / 2)))) = (π Β· (1 / (2 Β· (sinβ(π / 2)))))) |
222 | 86, 219, 221 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (πΎβπ ) = (π Β· (1 / (2 Β· (sinβ(π / 2)))))) |
223 | 222 | mpteq2dva 5209 |
. . . . . . . 8
β’ (π β (π β (π΄(,)π΅) β¦ (πΎβπ )) = (π β (π΄(,)π΅) β¦ (π Β· (1 / (2 Β· (sinβ(π / 2))))))) |
224 | 219, 221 | eqtr2d 2774 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (π Β· (1 / (2 Β· (sinβ(π / 2))))) = if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
225 | 224 | mpteq2dva 5209 |
. . . . . . . . 9
β’ (π β (π β (π΄(,)π΅) β¦ (π Β· (1 / (2 Β· (sinβ(π / 2)))))) = (π β (π΄(,)π΅) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))) |
226 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β (-Ο[,]Ο) β¦
if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
227 | | cncfss 24285 |
. . . . . . . . . . . 12
β’ ((β
β β β§ β β β) β
((-Ο[,]Ο)βcnββ)
β ((-Ο[,]Ο)βcnββ)) |
228 | 106, 160,
227 | mp2an 691 |
. . . . . . . . . . 11
β’
((-Ο[,]Ο)βcnββ) β ((-Ο[,]Ο)βcnββ) |
229 | 226 | fourierdlem62 44499 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,]Ο) β¦
if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β
((-Ο[,]Ο)βcnββ) |
230 | 229 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β ((-Ο[,]Ο)βcnββ)) |
231 | 228, 230 | sselid 3946 |
. . . . . . . . . 10
β’ (π β (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β ((-Ο[,]Ο)βcnββ)) |
232 | 83 | recnd 11191 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))) β β) |
233 | 226, 231,
41, 161, 232 | cncfmptssg 44202 |
. . . . . . . . 9
β’ (π β (π β (π΄(,)π΅) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β ((π΄(,)π΅)βcnββ)) |
234 | 225, 233 | eqeltrd 2834 |
. . . . . . . 8
β’ (π β (π β (π΄(,)π΅) β¦ (π Β· (1 / (2 Β· (sinβ(π / 2)))))) β ((π΄(,)π΅)βcnββ)) |
235 | 223, 234 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (π β (π΄(,)π΅) β¦ (πΎβπ )) β ((π΄(,)π΅)βcnββ)) |
236 | 218, 235 | mulcncf 24833 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ ((π»βπ ) Β· (πΎβπ ))) β ((π΄(,)π΅)βcnββ)) |
237 | 108, 236 | eqeltrd 2834 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β¦ (πβπ )) β ((π΄(,)π΅)βcnββ)) |
238 | 101 | mpteq2dva 5209 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ (πβπ )) = (π β (π΄(,)π΅) β¦ (sinβ((π + (1 / 2)) Β· π )))) |
239 | | sincn 25826 |
. . . . . . . 8
β’ sin
β (ββcnββ) |
240 | 239 | a1i 11 |
. . . . . . 7
β’ (π β sin β
(ββcnββ)) |
241 | | halfre 12375 |
. . . . . . . . . . . 12
β’ (1 / 2)
β β |
242 | 241 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (1 / 2) β
β) |
243 | 93, 242 | readdcld 11192 |
. . . . . . . . . 10
β’ (π β (π + (1 / 2)) β β) |
244 | 243 | recnd 11191 |
. . . . . . . . 9
β’ (π β (π + (1 / 2)) β β) |
245 | 146, 244,
161 | constcncfg 44203 |
. . . . . . . 8
β’ (π β (π β (π΄(,)π΅) β¦ (π + (1 / 2))) β ((π΄(,)π΅)βcnββ)) |
246 | 146, 161 | idcncfg 44204 |
. . . . . . . 8
β’ (π β (π β (π΄(,)π΅) β¦ π ) β ((π΄(,)π΅)βcnββ)) |
247 | 245, 246 | mulcncf 24833 |
. . . . . . 7
β’ (π β (π β (π΄(,)π΅) β¦ ((π + (1 / 2)) Β· π )) β ((π΄(,)π΅)βcnββ)) |
248 | 240, 247 | cncfmpt1f 24300 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ (sinβ((π + (1 / 2)) Β· π ))) β ((π΄(,)π΅)βcnββ)) |
249 | 238, 248 | eqeltrd 2834 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β¦ (πβπ )) β ((π΄(,)π΅)βcnββ)) |
250 | 237, 249 | mulcncf 24833 |
. . . 4
β’ (π β (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))) β ((π΄(,)π΅)βcnββ)) |
251 | | cncfcdm 24284 |
. . . 4
β’ ((β
β β β§ (π
β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))) β ((π΄(,)π΅)βcnββ)) β ((π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))) β ((π΄(,)π΅)βcnββ) β (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))):(π΄(,)π΅)βΆβ)) |
252 | 107, 250,
251 | syl2anc 585 |
. . 3
β’ (π β ((π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))) β ((π΄(,)π΅)βcnββ) β (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))):(π΄(,)π΅)βΆβ)) |
253 | 105, 252 | mpbird 257 |
. 2
β’ (π β (π β (π΄(,)π΅) β¦ ((πβπ ) Β· (πβπ ))) β ((π΄(,)π΅)βcnββ)) |
254 | 43, 253 | eqeltrd 2834 |
1
β’ (π β (πΊ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) |