Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ ((π β§ π β β) β π β β) |
2 | | fourierdlem95.ass |
. . . . . . . . . 10
β’ (π β π΄ β ((-Ο[,]Ο) β
{0})) |
3 | 2 | difss2d 4099 |
. . . . . . . . 9
β’ (π β π΄ β (-Ο[,]Ο)) |
4 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π΄ β (-Ο[,]Ο)) |
5 | 4 | sselda 3949 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β π β (-Ο[,]Ο)) |
6 | | fourierdlem95.f |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
7 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΉ:ββΆβ) |
8 | | fourierdlem95.xre |
. . . . . . . . . 10
β’ (π β π β β) |
9 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
10 | | ioossre 13332 |
. . . . . . . . . . . . 13
β’ (π(,)+β) β
β |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (π(,)+β) β
β) |
12 | 6, 11 | fssresd 6714 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ (π(,)+β)):(π(,)+β)βΆβ) |
13 | | ioosscn 13333 |
. . . . . . . . . . . 12
β’ (π(,)+β) β
β |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π(,)+β) β
β) |
15 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(TopOpenββfld) =
(TopOpenββfld) |
16 | | pnfxr 11216 |
. . . . . . . . . . . . 13
β’ +β
β β* |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β +β β
β*) |
18 | 8 | ltpnfd 13049 |
. . . . . . . . . . . 12
β’ (π β π < +β) |
19 | 15, 17, 8, 18 | lptioo1cn 43961 |
. . . . . . . . . . 11
β’ (π β π β
((limPtβ(TopOpenββfld))β(π(,)+β))) |
20 | | fourierdlem95.y |
. . . . . . . . . . 11
β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) |
21 | 12, 14, 19, 20 | limcrecl 43944 |
. . . . . . . . . 10
β’ (π β π β β) |
22 | 21 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
23 | | ioossre 13332 |
. . . . . . . . . . . . 13
β’
(-β(,)π)
β β |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (-β(,)π) β
β) |
25 | 6, 24 | fssresd 6714 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ (-β(,)π)):(-β(,)π)βΆβ) |
26 | | ioosscn 13333 |
. . . . . . . . . . . 12
β’
(-β(,)π)
β β |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (-β(,)π) β
β) |
28 | | mnfxr 11219 |
. . . . . . . . . . . . 13
β’ -β
β β* |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β -β β
β*) |
30 | 8 | mnfltd 13052 |
. . . . . . . . . . . 12
β’ (π β -β < π) |
31 | 15, 29, 8, 30 | lptioo2cn 43960 |
. . . . . . . . . . 11
β’ (π β π β
((limPtβ(TopOpenββfld))β(-β(,)π))) |
32 | | fourierdlem95.w |
. . . . . . . . . . 11
β’ (π β π β ((πΉ βΎ (-β(,)π)) limβ π)) |
33 | 25, 27, 31, 32 | limcrecl 43944 |
. . . . . . . . . 10
β’ (π β π β β) |
34 | 33 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
35 | | fourierdlem95.h |
. . . . . . . . 9
β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
36 | | fourierdlem95.k |
. . . . . . . . 9
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
37 | | fourierdlem95.u |
. . . . . . . . 9
β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) |
38 | 1 | nnred 12175 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
39 | | fourierdlem95.s |
. . . . . . . . 9
β’ π = (π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π ))) |
40 | | fourierdlem95.g |
. . . . . . . . 9
β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) |
41 | 7, 9, 22, 34, 35, 36, 37, 38, 39, 40 | fourierdlem67 44488 |
. . . . . . . 8
β’ ((π β§ π β β) β πΊ:(-Ο[,]Ο)βΆβ) |
42 | 41 | ffvelcdmda 7040 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (-Ο[,]Ο)) β (πΊβπ ) β β) |
43 | 5, 42 | syldan 592 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π΄) β (πΊβπ ) β β) |
44 | | fourierdlem95.admvol |
. . . . . . . 8
β’ (π β π΄ β dom vol) |
45 | 44 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π΄ β dom vol) |
46 | 41 | feqmptd 6915 |
. . . . . . . 8
β’ ((π β§ π β β) β πΊ = (π β (-Ο[,]Ο) β¦ (πΊβπ ))) |
47 | | fourierdlem95.p |
. . . . . . . . 9
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
48 | | fourierdlem95.x |
. . . . . . . . . 10
β’ (π β π β ran π) |
49 | 48 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β ran π) |
50 | 20 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β ((πΉ βΎ (π(,)+β)) limβ π)) |
51 | 32 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β ((πΉ βΎ (-β(,)π)) limβ π)) |
52 | | fourierdlem95.m |
. . . . . . . . . 10
β’ (π β π β β) |
53 | 52 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
54 | | fourierdlem95.v |
. . . . . . . . . 10
β’ (π β π β (πβπ)) |
55 | 54 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β (πβπ)) |
56 | | fourierdlem95.fcn |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
57 | 56 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
58 | | fourierdlem95.r |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
59 | 58 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
60 | | fourierdlem95.l |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
61 | 60 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
62 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
63 | 62 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
64 | 63 | cbvmptv 5223 |
. . . . . . . . 9
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
65 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦ {π β (β
βm (0...π))
β£ (((πβ0) =
-Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
66 | | fourierdlem95.i |
. . . . . . . . 9
β’ πΌ = (β D πΉ) |
67 | | fourierdlem95.ifn |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πΌ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
68 | 67 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΌ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
69 | | fourierdlem95.b |
. . . . . . . . . 10
β’ (π β π΅ β ((πΌ βΎ (-β(,)π)) limβ π)) |
70 | 69 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β π΅ β ((πΌ βΎ (-β(,)π)) limβ π)) |
71 | | fourierdlem95.c |
. . . . . . . . . 10
β’ (π β πΆ β ((πΌ βΎ (π(,)+β)) limβ π)) |
72 | 71 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΆ β ((πΌ βΎ (π(,)+β)) limβ π)) |
73 | 47, 7, 49, 50, 51, 35, 36, 37, 38, 39, 40, 53, 55, 57, 59, 61, 64, 65, 66, 68, 70, 72 | fourierdlem88 44509 |
. . . . . . . 8
β’ ((π β§ π β β) β πΊ β
πΏ1) |
74 | 46, 73 | eqeltrrd 2839 |
. . . . . . 7
β’ ((π β§ π β β) β (π β (-Ο[,]Ο) β¦ (πΊβπ )) β
πΏ1) |
75 | 4, 45, 42, 74 | iblss 25185 |
. . . . . 6
β’ ((π β§ π β β) β (π β π΄ β¦ (πΊβπ )) β
πΏ1) |
76 | 43, 75 | itgrecl 25178 |
. . . . 5
β’ ((π β§ π β β) β β«π΄(πΊβπ ) dπ β β) |
77 | | pire 25831 |
. . . . . 6
β’ Ο
β β |
78 | 77 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β Ο β
β) |
79 | | pipos 25833 |
. . . . . . 7
β’ 0 <
Ο |
80 | 77, 79 | gt0ne0ii 11698 |
. . . . . 6
β’ Ο β
0 |
81 | 80 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β Ο β
0) |
82 | 76, 78, 81 | redivcld 11990 |
. . . 4
β’ ((π β§ π β β) β (β«π΄(πΊβπ ) dπ / Ο) β β) |
83 | | fourierlemenplusacver2eqitgdirker.e |
. . . . 5
β’ πΈ = (π β β β¦ (β«π΄(πΊβπ ) dπ / Ο)) |
84 | 83 | fvmpt2 6964 |
. . . 4
β’ ((π β β β§
(β«π΄(πΊβπ ) dπ / Ο) β β) β (πΈβπ) = (β«π΄(πΊβπ ) dπ / Ο)) |
85 | 1, 82, 84 | syl2anc 585 |
. . 3
β’ ((π β§ π β β) β (πΈβπ) = (β«π΄(πΊβπ ) dπ / Ο)) |
86 | | fourierdlem95.o |
. . . . . . 7
β’ (π β π β β) |
87 | 86 | recnd 11190 |
. . . . . 6
β’ (π β π β β) |
88 | | 2cnd 12238 |
. . . . . 6
β’ (π β 2 β
β) |
89 | | 2ne0 12264 |
. . . . . . 7
β’ 2 β
0 |
90 | 89 | a1i 11 |
. . . . . 6
β’ (π β 2 β 0) |
91 | 87, 88, 90 | divrecd 11941 |
. . . . 5
β’ (π β (π / 2) = (π Β· (1 / 2))) |
92 | 91 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β (π / 2) = (π Β· (1 / 2))) |
93 | | fourierdlem95.itgdirker |
. . . . . 6
β’ ((π β§ π β β) β β«π΄((π·βπ)βπ ) dπ = (1 / 2)) |
94 | 93 | eqcomd 2743 |
. . . . 5
β’ ((π β§ π β β) β (1 / 2) = β«π΄((π·βπ)βπ ) dπ ) |
95 | 94 | oveq2d 7378 |
. . . 4
β’ ((π β§ π β β) β (π Β· (1 / 2)) = (π Β· β«π΄((π·βπ)βπ ) dπ )) |
96 | 92, 95 | eqtrd 2777 |
. . 3
β’ ((π β§ π β β) β (π / 2) = (π Β· β«π΄((π·βπ)βπ ) dπ )) |
97 | 85, 96 | oveq12d 7380 |
. 2
β’ ((π β§ π β β) β ((πΈβπ) + (π / 2)) = ((β«π΄(πΊβπ ) dπ / Ο) + (π Β· β«π΄((π·βπ)βπ ) dπ ))) |
98 | 2 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π β ((-Ο[,]Ο) β
{0})) |
99 | 98 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β π β ((-Ο[,]Ο) β
{0})) |
100 | | fourierdlem95.d |
. . . . . . . 8
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
101 | | eqid 2737 |
. . . . . . . 8
β’
((-Ο[,]Ο) β {0}) = ((-Ο[,]Ο) β
{0}) |
102 | 6, 8, 21, 33, 100, 35, 36, 37, 39, 40, 101 | fourierdlem66 44487 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((-Ο[,]Ο) β {0})) β
(πΊβπ ) = (Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )))) |
103 | 99, 102 | syldan 592 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π΄) β (πΊβπ ) = (Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )))) |
104 | 103 | itgeq2dv 25162 |
. . . . 5
β’ ((π β§ π β β) β β«π΄(πΊβπ ) dπ = β«π΄(Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) dπ ) |
105 | 104 | oveq1d 7377 |
. . . 4
β’ ((π β§ π β β) β (β«π΄(πΊβπ ) dπ / Ο) = (β«π΄(Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) dπ / Ο)) |
106 | 78 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π β β) β Ο β
β) |
107 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β πΉ:ββΆβ) |
108 | 8 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π β β) |
109 | | difss 4096 |
. . . . . . . . . . . . . 14
β’
((-Ο[,]Ο) β {0}) β (-Ο[,]Ο) |
110 | 77 | renegcli 11469 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β |
111 | | iccssre 13353 |
. . . . . . . . . . . . . . 15
β’ ((-Ο
β β β§ Ο β β) β (-Ο[,]Ο) β
β) |
112 | 110, 77, 111 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
(-Ο[,]Ο) β β |
113 | 109, 112 | sstri 3958 |
. . . . . . . . . . . . 13
β’
((-Ο[,]Ο) β {0}) β β |
114 | 113, 98 | sselid 3947 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π β β) |
115 | 108, 114 | readdcld 11191 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (π + π ) β β) |
116 | 107, 115 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (πΉβ(π + π )) β β) |
117 | 21, 33 | ifcld 4537 |
. . . . . . . . . . 11
β’ (π β if(0 < π , π, π) β β) |
118 | 117 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β if(0 < π , π, π) β β) |
119 | 116, 118 | resubcld 11590 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
120 | 119 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π΄) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
121 | 1 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π΄) β π β β) |
122 | 114 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π΄) β π β β) |
123 | 100 | dirkerre 44410 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β ((π·βπ)βπ ) β β) |
124 | 121, 122,
123 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π΄) β ((π·βπ)βπ ) β β) |
125 | 120, 124 | remulcld 11192 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) β β) |
126 | 103 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π΄) β (Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) = (πΊβπ )) |
127 | 126 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π΄) β ((Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) / Ο) = ((πΊβπ ) / Ο)) |
128 | | picn 25832 |
. . . . . . . . . . . . 13
β’ Ο
β β |
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π΄) β Ο β
β) |
130 | 125 | recnd 11190 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π΄) β (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) β β) |
131 | 80 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π΄) β Ο β 0) |
132 | 129, 130,
129, 131 | div23d 11975 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π΄) β ((Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) / Ο) = ((Ο / Ο) Β·
(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )))) |
133 | 43 | recnd 11190 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π΄) β (πΊβπ ) β β) |
134 | 133, 129,
131 | divrec2d 11942 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π΄) β ((πΊβπ ) / Ο) = ((1 / Ο) Β· (πΊβπ ))) |
135 | 127, 132,
134 | 3eqtr3rd 2786 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π΄) β ((1 / Ο) Β· (πΊβπ )) = ((Ο / Ο) Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )))) |
136 | 128, 80 | dividi 11895 |
. . . . . . . . . . . 12
β’ (Ο /
Ο) = 1 |
137 | 136 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π΄) β (Ο / Ο) = 1) |
138 | 137 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π΄) β ((Ο / Ο) Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) = (1 Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )))) |
139 | 130 | mulid2d 11180 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π΄) β (1 Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) = (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) |
140 | 135, 138,
139 | 3eqtrrd 2782 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π΄) β (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) = ((1 / Ο) Β· (πΊβπ ))) |
141 | 140 | mpteq2dva 5210 |
. . . . . . . 8
β’ ((π β§ π β β) β (π β π΄ β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) = (π β π΄ β¦ ((1 / Ο) Β· (πΊβπ )))) |
142 | 106, 81 | reccld 11931 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1 / Ο) β
β) |
143 | 142, 43, 75 | iblmulc2 25211 |
. . . . . . . 8
β’ ((π β§ π β β) β (π β π΄ β¦ ((1 / Ο) Β· (πΊβπ ))) β
πΏ1) |
144 | 141, 143 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π β β) β (π β π΄ β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) β
πΏ1) |
145 | 106, 125,
144 | itgmulc2 25214 |
. . . . . 6
β’ ((π β§ π β β) β (Ο Β·
β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ ) = β«π΄(Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) dπ ) |
146 | 145 | eqcomd 2743 |
. . . . 5
β’ ((π β§ π β β) β β«π΄(Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) dπ = (Ο Β· β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ )) |
147 | 146 | oveq1d 7377 |
. . . 4
β’ ((π β§ π β β) β (β«π΄(Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ ))) dπ / Ο) = ((Ο Β· β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ ) / Ο)) |
148 | 125, 144 | itgcl 25164 |
. . . . 5
β’ ((π β§ π β β) β β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ β β) |
149 | 148, 106,
81 | divcan3d 11943 |
. . . 4
β’ ((π β§ π β β) β ((Ο Β·
β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ ) / Ο) = β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ ) |
150 | 105, 147,
149 | 3eqtrd 2781 |
. . 3
β’ ((π β§ π β β) β (β«π΄(πΊβπ ) dπ / Ο) = β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ ) |
151 | 87 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β π β β) |
152 | 112 | sseli 3945 |
. . . . . . 7
β’ (π β (-Ο[,]Ο) β
π β
β) |
153 | 152, 123 | sylan2 594 |
. . . . . 6
β’ ((π β β β§ π β (-Ο[,]Ο)) β
((π·βπ)βπ ) β β) |
154 | 153 | adantll 713 |
. . . . 5
β’ (((π β§ π β β) β§ π β (-Ο[,]Ο)) β ((π·βπ)βπ ) β β) |
155 | 110 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β -Ο β
β) |
156 | | ax-resscn 11115 |
. . . . . . . . . 10
β’ β
β β |
157 | 156 | a1i 11 |
. . . . . . . . 9
β’ (π β β β β
β β) |
158 | | ssid 3971 |
. . . . . . . . 9
β’ β
β β |
159 | | cncfss 24278 |
. . . . . . . . 9
β’ ((β
β β β§ β β β) β
((-Ο[,]Ο)βcnββ)
β ((-Ο[,]Ο)βcnββ)) |
160 | 157, 158,
159 | sylancl 587 |
. . . . . . . 8
β’ (π β β β
((-Ο[,]Ο)βcnββ)
β ((-Ο[,]Ο)βcnββ)) |
161 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦ ((π·βπ)βπ )) = (π β β β¦ ((π·βπ)βπ )) |
162 | 100 | dirkerf 44412 |
. . . . . . . . . . 11
β’ (π β β β (π·βπ):ββΆβ) |
163 | 162 | feqmptd 6915 |
. . . . . . . . . 10
β’ (π β β β (π·βπ) = (π β β β¦ ((π·βπ)βπ ))) |
164 | 100 | dirkercncf 44422 |
. . . . . . . . . 10
β’ (π β β β (π·βπ) β (ββcnββ)) |
165 | 163, 164 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β β β (π β β β¦ ((π·βπ)βπ )) β (ββcnββ)) |
166 | 112 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
(-Ο[,]Ο) β β) |
167 | | ssid 3971 |
. . . . . . . . . 10
β’ β
β β |
168 | 167 | a1i 11 |
. . . . . . . . 9
β’ (π β β β β
β β) |
169 | 161, 165,
166, 168, 153 | cncfmptssg 44186 |
. . . . . . . 8
β’ (π β β β (π β (-Ο[,]Ο) β¦
((π·βπ)βπ )) β ((-Ο[,]Ο)βcnββ)) |
170 | 160, 169 | sseldd 3950 |
. . . . . . 7
β’ (π β β β (π β (-Ο[,]Ο) β¦
((π·βπ)βπ )) β ((-Ο[,]Ο)βcnββ)) |
171 | 170 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β (π β (-Ο[,]Ο) β¦ ((π·βπ)βπ )) β ((-Ο[,]Ο)βcnββ)) |
172 | | cniccibl 25221 |
. . . . . 6
β’ ((-Ο
β β β§ Ο β β β§ (π β (-Ο[,]Ο) β¦ ((π·βπ)βπ )) β ((-Ο[,]Ο)βcnββ)) β (π β (-Ο[,]Ο) β¦ ((π·βπ)βπ )) β
πΏ1) |
173 | 155, 78, 171, 172 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β β) β (π β (-Ο[,]Ο) β¦ ((π·βπ)βπ )) β
πΏ1) |
174 | 4, 45, 154, 173 | iblss 25185 |
. . . 4
β’ ((π β§ π β β) β (π β π΄ β¦ ((π·βπ)βπ )) β
πΏ1) |
175 | 151, 124,
174 | itgmulc2 25214 |
. . 3
β’ ((π β§ π β β) β (π Β· β«π΄((π·βπ)βπ ) dπ ) = β«π΄(π Β· ((π·βπ)βπ )) dπ ) |
176 | 150, 175 | oveq12d 7380 |
. 2
β’ ((π β§ π β β) β ((β«π΄(πΊβπ ) dπ / Ο) + (π Β· β«π΄((π·βπ)βπ ) dπ )) = (β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ + β«π΄(π Β· ((π·βπ)βπ )) dπ )) |
177 | 86 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π β π΄) β π β β) |
178 | 177, 124 | remulcld 11192 |
. . . 4
β’ (((π β§ π β β) β§ π β π΄) β (π Β· ((π·βπ)βπ )) β β) |
179 | 151, 124,
174 | iblmulc2 25211 |
. . . 4
β’ ((π β§ π β β) β (π β π΄ β¦ (π Β· ((π·βπ)βπ ))) β
πΏ1) |
180 | 125, 144,
178, 179 | itgadd 25205 |
. . 3
β’ ((π β§ π β β) β β«π΄((((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) + (π Β· ((π·βπ)βπ ))) dπ = (β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ + β«π΄(π Β· ((π·βπ)βπ )) dπ )) |
181 | | fourierdlem95.ifeqo |
. . . . . . . . 9
β’ ((π β§ π β π΄) β if(0 < π , π, π) = π) |
182 | 181 | eqcomd 2743 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π = if(0 < π , π, π)) |
183 | 182 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β π = if(0 < π , π, π)) |
184 | 183 | oveq1d 7377 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π΄) β (π Β· ((π·βπ)βπ )) = (if(0 < π , π, π) Β· ((π·βπ)βπ ))) |
185 | 184 | oveq2d 7378 |
. . . . 5
β’ (((π β§ π β β) β§ π β π΄) β ((((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) + (π Β· ((π·βπ)βπ ))) = ((((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) + (if(0 < π , π, π) Β· ((π·βπ)βπ )))) |
186 | 116 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (πΉβ(π + π )) β β) |
187 | 186 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β (πΉβ(π + π )) β β) |
188 | 118 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β π΄) β if(0 < π , π, π) β β) |
189 | 188 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β if(0 < π , π, π) β β) |
190 | 124 | recnd 11190 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β ((π·βπ)βπ ) β β) |
191 | 187, 189,
190 | subdird 11619 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π΄) β (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) = (((πΉβ(π + π )) Β· ((π·βπ)βπ )) β (if(0 < π , π, π) Β· ((π·βπ)βπ )))) |
192 | 191 | oveq1d 7377 |
. . . . 5
β’ (((π β§ π β β) β§ π β π΄) β ((((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) + (if(0 < π , π, π) Β· ((π·βπ)βπ ))) = ((((πΉβ(π + π )) Β· ((π·βπ)βπ )) β (if(0 < π , π, π) Β· ((π·βπ)βπ ))) + (if(0 < π , π, π) Β· ((π·βπ)βπ )))) |
193 | 187, 190 | mulcld 11182 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π΄) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
194 | 189, 190 | mulcld 11182 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π΄) β (if(0 < π , π, π) Β· ((π·βπ)βπ )) β β) |
195 | 193, 194 | npcand 11523 |
. . . . 5
β’ (((π β§ π β β) β§ π β π΄) β ((((πΉβ(π + π )) Β· ((π·βπ)βπ )) β (if(0 < π , π, π) Β· ((π·βπ)βπ ))) + (if(0 < π , π, π) Β· ((π·βπ)βπ ))) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
196 | 185, 192,
195 | 3eqtrd 2781 |
. . . 4
β’ (((π β§ π β β) β§ π β π΄) β ((((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) + (π Β· ((π·βπ)βπ ))) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
197 | 196 | itgeq2dv 25162 |
. . 3
β’ ((π β§ π β β) β β«π΄((((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) + (π Β· ((π·βπ)βπ ))) dπ = β«π΄((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
198 | 180, 197 | eqtr3d 2779 |
. 2
β’ ((π β§ π β β) β (β«π΄(((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )) dπ + β«π΄(π Β· ((π·βπ)βπ )) dπ ) = β«π΄((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
199 | 97, 176, 198 | 3eqtrd 2781 |
1
β’ ((π β§ π β β) β ((πΈβπ) + (π / 2)) = β«π΄((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |