Step | Hyp | Ref
| Expression |
1 | | fourierdlem114.f |
. 2
β’ (π β πΉ:ββΆβ) |
2 | | fourierdlem114.t |
. 2
β’ π = (2 Β·
Ο) |
3 | | fourierdlem114.per |
. 2
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
4 | | fourierdlem114.x |
. 2
β’ (π β π β β) |
5 | | fourierdlem114.l |
. 2
β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) |
6 | | fourierdlem114.r |
. 2
β’ (π β π
β ((πΉ βΎ (π(,)+β)) limβ π)) |
7 | | fourierdlem114.p |
. 2
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
8 | | fourierdlem114.m |
. . 3
β’ π = ((β―βπ») β 1) |
9 | | 2z 12542 |
. . . . . 6
β’ 2 β
β€ |
10 | 9 | a1i 11 |
. . . . 5
β’ (π β 2 β
β€) |
11 | | fourierdlem114.h |
. . . . . . . 8
β’ π» = ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) |
12 | | tpfi 9274 |
. . . . . . . . . 10
β’ {-Ο,
Ο, (πΈβπ)} β Fin |
13 | 12 | a1i 11 |
. . . . . . . . 9
β’ (π β {-Ο, Ο, (πΈβπ)} β Fin) |
14 | | pire 25831 |
. . . . . . . . . . . . . . 15
β’ Ο
β β |
15 | 14 | renegcli 11469 |
. . . . . . . . . . . . . 14
β’ -Ο
β β |
16 | 15 | rexri 11220 |
. . . . . . . . . . . . 13
β’ -Ο
β β* |
17 | 14 | rexri 11220 |
. . . . . . . . . . . . 13
β’ Ο
β β* |
18 | | negpilt0 43588 |
. . . . . . . . . . . . . . 15
β’ -Ο
< 0 |
19 | | pipos 25833 |
. . . . . . . . . . . . . . 15
β’ 0 <
Ο |
20 | | 0re 11164 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
21 | 15, 20, 14 | lttri 11288 |
. . . . . . . . . . . . . . 15
β’ ((-Ο
< 0 β§ 0 < Ο) β -Ο < Ο) |
22 | 18, 19, 21 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ -Ο
< Ο |
23 | 15, 14, 22 | ltleii 11285 |
. . . . . . . . . . . . 13
β’ -Ο
β€ Ο |
24 | | prunioo 13405 |
. . . . . . . . . . . . 13
β’ ((-Ο
β β* β§ Ο β β* β§ -Ο
β€ Ο) β ((-Ο(,)Ο) βͺ {-Ο, Ο}) =
(-Ο[,]Ο)) |
25 | 16, 17, 23, 24 | mp3an 1462 |
. . . . . . . . . . . 12
β’
((-Ο(,)Ο) βͺ {-Ο, Ο}) = (-Ο[,]Ο) |
26 | 25 | difeq1i 4083 |
. . . . . . . . . . 11
β’
(((-Ο(,)Ο) βͺ {-Ο, Ο}) β dom πΊ) = ((-Ο[,]Ο) β dom πΊ) |
27 | | difundir 4245 |
. . . . . . . . . . 11
β’
(((-Ο(,)Ο) βͺ {-Ο, Ο}) β dom πΊ) = (((-Ο(,)Ο) β dom πΊ) βͺ ({-Ο, Ο} β
dom πΊ)) |
28 | 26, 27 | eqtr3i 2767 |
. . . . . . . . . 10
β’
((-Ο[,]Ο) β dom πΊ) = (((-Ο(,)Ο) β dom πΊ) βͺ ({-Ο, Ο} β
dom πΊ)) |
29 | | fourierdlem114.dmdv |
. . . . . . . . . . 11
β’ (π β ((-Ο(,)Ο) β
dom πΊ) β
Fin) |
30 | | prfi 9273 |
. . . . . . . . . . . 12
β’ {-Ο,
Ο} β Fin |
31 | | diffi 9130 |
. . . . . . . . . . . 12
β’ ({-Ο,
Ο} β Fin β ({-Ο, Ο} β dom πΊ) β Fin) |
32 | 30, 31 | mp1i 13 |
. . . . . . . . . . 11
β’ (π β ({-Ο, Ο} β dom
πΊ) β
Fin) |
33 | | unfi 9123 |
. . . . . . . . . . 11
β’
((((-Ο(,)Ο) β dom πΊ) β Fin β§ ({-Ο, Ο} β
dom πΊ) β Fin) β
(((-Ο(,)Ο) β dom πΊ) βͺ ({-Ο, Ο} β dom πΊ)) β Fin) |
34 | 29, 32, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (((-Ο(,)Ο) β
dom πΊ) βͺ ({-Ο, Ο}
β dom πΊ)) β
Fin) |
35 | 28, 34 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β ((-Ο[,]Ο) β
dom πΊ) β
Fin) |
36 | | unfi 9123 |
. . . . . . . . 9
β’ (({-Ο,
Ο, (πΈβπ)} β Fin β§
((-Ο[,]Ο) β dom πΊ) β Fin) β ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) β Fin) |
37 | 13, 35, 36 | syl2anc 585 |
. . . . . . . 8
β’ (π β ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) β Fin) |
38 | 11, 37 | eqeltrid 2842 |
. . . . . . 7
β’ (π β π» β Fin) |
39 | | hashcl 14263 |
. . . . . . 7
β’ (π» β Fin β
(β―βπ») β
β0) |
40 | 38, 39 | syl 17 |
. . . . . 6
β’ (π β (β―βπ») β
β0) |
41 | 40 | nn0zd 12532 |
. . . . 5
β’ (π β (β―βπ») β
β€) |
42 | 15, 22 | ltneii 11275 |
. . . . . . 7
β’ -Ο
β Ο |
43 | | hashprg 14302 |
. . . . . . . 8
β’ ((-Ο
β β β§ Ο β β) β (-Ο β Ο β
(β―β{-Ο, Ο}) = 2)) |
44 | 15, 14, 43 | mp2an 691 |
. . . . . . 7
β’ (-Ο
β Ο β (β―β{-Ο, Ο}) = 2) |
45 | 42, 44 | mpbi 229 |
. . . . . 6
β’
(β―β{-Ο, Ο}) = 2 |
46 | 12 | elexi 3467 |
. . . . . . . . . 10
β’ {-Ο,
Ο, (πΈβπ)} β V |
47 | | ovex 7395 |
. . . . . . . . . . 11
β’
(-Ο[,]Ο) β V |
48 | | difexg 5289 |
. . . . . . . . . . 11
β’
((-Ο[,]Ο) β V β ((-Ο[,]Ο) β dom πΊ) β V) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . 10
β’
((-Ο[,]Ο) β dom πΊ) β V |
50 | 46, 49 | unex 7685 |
. . . . . . . . 9
β’ ({-Ο,
Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β
dom πΊ)) β
V |
51 | 11, 50 | eqeltri 2834 |
. . . . . . . 8
β’ π» β V |
52 | | negex 11406 |
. . . . . . . . . . 11
β’ -Ο
β V |
53 | 52 | tpid1 4734 |
. . . . . . . . . 10
β’ -Ο
β {-Ο, Ο, (πΈβπ)} |
54 | 14 | elexi 3467 |
. . . . . . . . . . 11
β’ Ο
β V |
55 | 54 | tpid2 4736 |
. . . . . . . . . 10
β’ Ο
β {-Ο, Ο, (πΈβπ)} |
56 | | prssi 4786 |
. . . . . . . . . 10
β’ ((-Ο
β {-Ο, Ο, (πΈβπ)} β§ Ο β {-Ο, Ο, (πΈβπ)}) β {-Ο, Ο} β {-Ο,
Ο, (πΈβπ)}) |
57 | 53, 55, 56 | mp2an 691 |
. . . . . . . . 9
β’ {-Ο,
Ο} β {-Ο, Ο, (πΈβπ)} |
58 | | ssun1 4137 |
. . . . . . . . . 10
β’ {-Ο,
Ο, (πΈβπ)} β ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) |
59 | 58, 11 | sseqtrri 3986 |
. . . . . . . . 9
β’ {-Ο,
Ο, (πΈβπ)} β π» |
60 | 57, 59 | sstri 3958 |
. . . . . . . 8
β’ {-Ο,
Ο} β π» |
61 | | hashss 14316 |
. . . . . . . 8
β’ ((π» β V β§ {-Ο, Ο}
β π») β
(β―β{-Ο, Ο}) β€ (β―βπ»)) |
62 | 51, 60, 61 | mp2an 691 |
. . . . . . 7
β’
(β―β{-Ο, Ο}) β€ (β―βπ») |
63 | 62 | a1i 11 |
. . . . . 6
β’ (π β (β―β{-Ο,
Ο}) β€ (β―βπ»)) |
64 | 45, 63 | eqbrtrrid 5146 |
. . . . 5
β’ (π β 2 β€
(β―βπ»)) |
65 | | eluz2 12776 |
. . . . 5
β’
((β―βπ»)
β (β€β₯β2) β (2 β β€ β§
(β―βπ») β
β€ β§ 2 β€ (β―βπ»))) |
66 | 10, 41, 64, 65 | syl3anbrc 1344 |
. . . 4
β’ (π β (β―βπ») β
(β€β₯β2)) |
67 | | uz2m1nn 12855 |
. . . 4
β’
((β―βπ»)
β (β€β₯β2) β ((β―βπ») β 1) β
β) |
68 | 66, 67 | syl 17 |
. . 3
β’ (π β ((β―βπ») β 1) β
β) |
69 | 8, 68 | eqeltrid 2842 |
. 2
β’ (π β π β β) |
70 | 15 | a1i 11 |
. . . . . . . . . . 11
β’ (π β -Ο β
β) |
71 | 14 | a1i 11 |
. . . . . . . . . . 11
β’ (π β Ο β
β) |
72 | | negpitopissre 25912 |
. . . . . . . . . . . 12
β’
(-Ο(,]Ο) β β |
73 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β -Ο <
Ο) |
74 | | picn 25832 |
. . . . . . . . . . . . . . . 16
β’ Ο
β β |
75 | 74 | 2timesi 12298 |
. . . . . . . . . . . . . . 15
β’ (2
Β· Ο) = (Ο + Ο) |
76 | 74, 74 | subnegi 11487 |
. . . . . . . . . . . . . . 15
β’ (Ο
β -Ο) = (Ο + Ο) |
77 | 75, 2, 76 | 3eqtr4i 2775 |
. . . . . . . . . . . . . 14
β’ π = (Ο β
-Ο) |
78 | | fourierdlem114.e |
. . . . . . . . . . . . . 14
β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((Ο β π₯) / π)) Β· π))) |
79 | 70, 71, 73, 77, 78 | fourierdlem4 44426 |
. . . . . . . . . . . . 13
β’ (π β πΈ:ββΆ(-Ο(,]Ο)) |
80 | 79, 4 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (π β (πΈβπ) β (-Ο(,]Ο)) |
81 | 72, 80 | sselid 3947 |
. . . . . . . . . . 11
β’ (π β (πΈβπ) β β) |
82 | 70, 71, 81 | 3jca 1129 |
. . . . . . . . . 10
β’ (π β (-Ο β β
β§ Ο β β β§ (πΈβπ) β β)) |
83 | | fvex 6860 |
. . . . . . . . . . 11
β’ (πΈβπ) β V |
84 | 52, 54, 83 | tpss 4800 |
. . . . . . . . . 10
β’ ((-Ο
β β β§ Ο β β β§ (πΈβπ) β β) β {-Ο, Ο,
(πΈβπ)} β β) |
85 | 82, 84 | sylib 217 |
. . . . . . . . 9
β’ (π β {-Ο, Ο, (πΈβπ)} β β) |
86 | | iccssre 13353 |
. . . . . . . . . . 11
β’ ((-Ο
β β β§ Ο β β) β (-Ο[,]Ο) β
β) |
87 | 15, 14, 86 | mp2an 691 |
. . . . . . . . . 10
β’
(-Ο[,]Ο) β β |
88 | | ssdifss 4100 |
. . . . . . . . . 10
β’
((-Ο[,]Ο) β β β ((-Ο[,]Ο) β dom πΊ) β
β) |
89 | 87, 88 | mp1i 13 |
. . . . . . . . 9
β’ (π β ((-Ο[,]Ο) β
dom πΊ) β
β) |
90 | 85, 89 | unssd 4151 |
. . . . . . . 8
β’ (π β ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) β
β) |
91 | 11, 90 | eqsstrid 3997 |
. . . . . . 7
β’ (π β π» β β) |
92 | | fourierdlem114.q |
. . . . . . 7
β’ π = (β©ππ Isom < , < ((0...π), π»)) |
93 | 38, 91, 92, 8 | fourierdlem36 44458 |
. . . . . 6
β’ (π β π Isom < , < ((0...π), π»)) |
94 | | isof1o 7273 |
. . . . . 6
β’ (π Isom < , < ((0...π), π») β π:(0...π)β1-1-ontoβπ») |
95 | | f1of 6789 |
. . . . . 6
β’ (π:(0...π)β1-1-ontoβπ» β π:(0...π)βΆπ») |
96 | 93, 94, 95 | 3syl 18 |
. . . . 5
β’ (π β π:(0...π)βΆπ») |
97 | 96, 91 | fssd 6691 |
. . . 4
β’ (π β π:(0...π)βΆβ) |
98 | | reex 11149 |
. . . . 5
β’ β
β V |
99 | | ovex 7395 |
. . . . 5
β’
(0...π) β
V |
100 | 98, 99 | elmap 8816 |
. . . 4
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
101 | 97, 100 | sylibr 233 |
. . 3
β’ (π β π β (β βm
(0...π))) |
102 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (0 =
π β (πβ0) = (πβπ)) |
103 | 102 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ 0 = π) β (πβ0) = (πβπ)) |
104 | 97 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
105 | 104 | leidd 11728 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (πβπ) β€ (πβπ)) |
106 | 105 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ 0 = π) β (πβπ) β€ (πβπ)) |
107 | 103, 106 | eqbrtrd 5132 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ 0 = π) β (πβ0) β€ (πβπ)) |
108 | | elfzelz 13448 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β€) |
109 | 108 | zred 12614 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β) |
110 | 109 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ Β¬ 0 = π) β π β β) |
111 | | elfzle1 13451 |
. . . . . . . . . . . 12
β’ (π β (0...π) β 0 β€ π) |
112 | 111 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ Β¬ 0 = π) β 0 β€ π) |
113 | | neqne 2952 |
. . . . . . . . . . . . 13
β’ (Β¬ 0
= π β 0 β π) |
114 | 113 | necomd 3000 |
. . . . . . . . . . . 12
β’ (Β¬ 0
= π β π β 0) |
115 | 114 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ Β¬ 0 = π) β π β 0) |
116 | 110, 112,
115 | ne0gt0d 11299 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ Β¬ 0 = π) β 0 < π) |
117 | | nnssnn0 12423 |
. . . . . . . . . . . . . . . . 17
β’ β
β β0 |
118 | | nn0uz 12812 |
. . . . . . . . . . . . . . . . 17
β’
β0 = (β€β₯β0) |
119 | 117, 118 | sseqtri 3985 |
. . . . . . . . . . . . . . . 16
β’ β
β (β€β₯β0) |
120 | 119, 69 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’ (π β π β
(β€β₯β0)) |
121 | | eluzfz1 13455 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β 0 β (0...π)) |
123 | 96, 122 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (π β (πβ0) β π») |
124 | 91, 123 | sseldd 3950 |
. . . . . . . . . . . 12
β’ (π β (πβ0) β β) |
125 | 124 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ 0 < π) β (πβ0) β β) |
126 | 104 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ 0 < π) β (πβπ) β β) |
127 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ 0 < π) β 0 < π) |
128 | 93 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ 0 < π) β π Isom < , < ((0...π), π»)) |
129 | 122 | anim1i 616 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (0 β (0...π) β§ π β (0...π))) |
130 | 129 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ 0 < π) β (0 β (0...π) β§ π β (0...π))) |
131 | | isorel 7276 |
. . . . . . . . . . . . 13
β’ ((π Isom < , < ((0...π), π») β§ (0 β (0...π) β§ π β (0...π))) β (0 < π β (πβ0) < (πβπ))) |
132 | 128, 130,
131 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ 0 < π) β (0 < π β (πβ0) < (πβπ))) |
133 | 127, 132 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ 0 < π) β (πβ0) < (πβπ)) |
134 | 125, 126,
133 | ltled 11310 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ 0 < π) β (πβ0) β€ (πβπ)) |
135 | 116, 134 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ Β¬ 0 = π) β (πβ0) β€ (πβπ)) |
136 | 107, 135 | pm2.61dan 812 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β (πβ0) β€ (πβπ)) |
137 | 136 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β (πβ0) β€ (πβπ)) |
138 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β (πβπ) = -Ο) |
139 | 137, 138 | breqtrd 5136 |
. . . . . 6
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β (πβ0) β€ -Ο) |
140 | 70 | rexrd 11212 |
. . . . . . . 8
β’ (π β -Ο β
β*) |
141 | 71 | rexrd 11212 |
. . . . . . . 8
β’ (π β Ο β
β*) |
142 | | lbicc2 13388 |
. . . . . . . . . . . . . 14
β’ ((-Ο
β β* β§ Ο β β* β§ -Ο
β€ Ο) β -Ο β (-Ο[,]Ο)) |
143 | 16, 17, 23, 142 | mp3an 1462 |
. . . . . . . . . . . . 13
β’ -Ο
β (-Ο[,]Ο) |
144 | 143 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β -Ο β
(-Ο[,]Ο)) |
145 | | ubicc2 13389 |
. . . . . . . . . . . . . 14
β’ ((-Ο
β β* β§ Ο β β* β§ -Ο
β€ Ο) β Ο β (-Ο[,]Ο)) |
146 | 16, 17, 23, 145 | mp3an 1462 |
. . . . . . . . . . . . 13
β’ Ο
β (-Ο[,]Ο) |
147 | 146 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β Ο β
(-Ο[,]Ο)) |
148 | | iocssicc 13361 |
. . . . . . . . . . . . 13
β’
(-Ο(,]Ο) β (-Ο[,]Ο) |
149 | 148, 80 | sselid 3947 |
. . . . . . . . . . . 12
β’ (π β (πΈβπ) β (-Ο[,]Ο)) |
150 | | tpssi 4801 |
. . . . . . . . . . . 12
β’ ((-Ο
β (-Ο[,]Ο) β§ Ο β (-Ο[,]Ο) β§ (πΈβπ) β (-Ο[,]Ο)) β {-Ο,
Ο, (πΈβπ)} β
(-Ο[,]Ο)) |
151 | 144, 147,
149, 150 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β {-Ο, Ο, (πΈβπ)} β (-Ο[,]Ο)) |
152 | | difssd 4097 |
. . . . . . . . . . 11
β’ (π β ((-Ο[,]Ο) β
dom πΊ) β
(-Ο[,]Ο)) |
153 | 151, 152 | unssd 4151 |
. . . . . . . . . 10
β’ (π β ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) β
(-Ο[,]Ο)) |
154 | 11, 153 | eqsstrid 3997 |
. . . . . . . . 9
β’ (π β π» β (-Ο[,]Ο)) |
155 | 154, 123 | sseldd 3950 |
. . . . . . . 8
β’ (π β (πβ0) β
(-Ο[,]Ο)) |
156 | | iccgelb 13327 |
. . . . . . . 8
β’ ((-Ο
β β* β§ Ο β β* β§ (πβ0) β (-Ο[,]Ο))
β -Ο β€ (πβ0)) |
157 | 140, 141,
155, 156 | syl3anc 1372 |
. . . . . . 7
β’ (π β -Ο β€ (πβ0)) |
158 | 157 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β -Ο β€ (πβ0)) |
159 | 124 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β (πβ0) β β) |
160 | 15 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β -Ο β
β) |
161 | 159, 160 | letri3d 11304 |
. . . . . 6
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β ((πβ0) = -Ο β ((πβ0) β€ -Ο β§ -Ο β€ (πβ0)))) |
162 | 139, 158,
161 | mpbir2and 712 |
. . . . 5
β’ (((π β§ π β (0...π)) β§ (πβπ) = -Ο) β (πβ0) = -Ο) |
163 | 59, 53 | sselii 3946 |
. . . . . . 7
β’ -Ο
β π» |
164 | | f1ofo 6796 |
. . . . . . . . 9
β’ (π:(0...π)β1-1-ontoβπ» β π:(0...π)βontoβπ») |
165 | 94, 164 | syl 17 |
. . . . . . . 8
β’ (π Isom < , < ((0...π), π») β π:(0...π)βontoβπ») |
166 | | forn 6764 |
. . . . . . . 8
β’ (π:(0...π)βontoβπ» β ran π = π») |
167 | 93, 165, 166 | 3syl 18 |
. . . . . . 7
β’ (π β ran π = π») |
168 | 163, 167 | eleqtrrid 2845 |
. . . . . 6
β’ (π β -Ο β ran π) |
169 | | ffn 6673 |
. . . . . . 7
β’ (π:(0...π)βΆπ» β π Fn (0...π)) |
170 | | fvelrnb 6908 |
. . . . . . 7
β’ (π Fn (0...π) β (-Ο β ran π β βπ β (0...π)(πβπ) = -Ο)) |
171 | 96, 169, 170 | 3syl 18 |
. . . . . 6
β’ (π β (-Ο β ran π β βπ β (0...π)(πβπ) = -Ο)) |
172 | 168, 171 | mpbid 231 |
. . . . 5
β’ (π β βπ β (0...π)(πβπ) = -Ο) |
173 | 162, 172 | r19.29a 3160 |
. . . 4
β’ (π β (πβ0) = -Ο) |
174 | 59, 55 | sselii 3946 |
. . . . . . 7
β’ Ο
β π» |
175 | 174, 167 | eleqtrrid 2845 |
. . . . . 6
β’ (π β Ο β ran π) |
176 | | fvelrnb 6908 |
. . . . . . 7
β’ (π Fn (0...π) β (Ο β ran π β βπ β (0...π)(πβπ) = Ο)) |
177 | 96, 169, 176 | 3syl 18 |
. . . . . 6
β’ (π β (Ο β ran π β βπ β (0...π)(πβπ) = Ο)) |
178 | 175, 177 | mpbid 231 |
. . . . 5
β’ (π β βπ β (0...π)(πβπ) = Ο) |
179 | 96, 154 | fssd 6691 |
. . . . . . . . . 10
β’ (π β π:(0...π)βΆ(-Ο[,]Ο)) |
180 | | eluzfz2 13456 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β0) β π β (0...π)) |
181 | 120, 180 | syl 17 |
. . . . . . . . . 10
β’ (π β π β (0...π)) |
182 | 179, 181 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ (π β (πβπ) β (-Ο[,]Ο)) |
183 | | iccleub 13326 |
. . . . . . . . 9
β’ ((-Ο
β β* β§ Ο β β* β§ (πβπ) β (-Ο[,]Ο)) β (πβπ) β€ Ο) |
184 | 140, 141,
182, 183 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (πβπ) β€ Ο) |
185 | 184 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β (πβπ) β€ Ο) |
186 | | id 22 |
. . . . . . . . . 10
β’ ((πβπ) = Ο β (πβπ) = Ο) |
187 | 186 | eqcomd 2743 |
. . . . . . . . 9
β’ ((πβπ) = Ο β Ο = (πβπ)) |
188 | 187 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β Ο = (πβπ)) |
189 | 105 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π = π) β (πβπ) β€ (πβπ)) |
190 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
191 | 190 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π = π) β (πβπ) = (πβπ)) |
192 | 189, 191 | breqtrd 5136 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π = π) β (πβπ) β€ (πβπ)) |
193 | 109 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ Β¬ π = π) β π β β) |
194 | | elfzel2 13446 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β π β β€) |
195 | 194 | zred 12614 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β) |
196 | 195 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ Β¬ π = π) β π β β) |
197 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β€ π) |
198 | 197 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ Β¬ π = π) β π β€ π) |
199 | | neqne 2952 |
. . . . . . . . . . . . . 14
β’ (Β¬
π = π β π β π) |
200 | 199 | necomd 3000 |
. . . . . . . . . . . . 13
β’ (Β¬
π = π β π β π) |
201 | 200 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ Β¬ π = π) β π β π) |
202 | 193, 196,
198, 201 | leneltd 11316 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ Β¬ π = π) β π < π) |
203 | 104 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
204 | 87, 182 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (π β (πβπ) β β) |
205 | 204 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
206 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ π < π) β π < π) |
207 | 93 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0...π)) β§ π < π) β π Isom < , < ((0...π), π»)) |
208 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π)) β π β (0...π)) |
209 | 181 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π)) β π β (0...π)) |
210 | 208, 209 | jca 513 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...π)) β (π β (0...π) β§ π β (0...π))) |
211 | 210 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0...π)) β§ π < π) β (π β (0...π) β§ π β (0...π))) |
212 | | isorel 7276 |
. . . . . . . . . . . . . 14
β’ ((π Isom < , < ((0...π), π») β§ (π β (0...π) β§ π β (0...π))) β (π < π β (πβπ) < (πβπ))) |
213 | 207, 211,
212 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ π < π) β (π < π β (πβπ) < (πβπ))) |
214 | 206, 213 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π < π) β (πβπ) < (πβπ)) |
215 | 203, 205,
214 | ltled 11310 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π < π) β (πβπ) β€ (πβπ)) |
216 | 202, 215 | syldan 592 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ Β¬ π = π) β (πβπ) β€ (πβπ)) |
217 | 192, 216 | pm2.61dan 812 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β (πβπ) β€ (πβπ)) |
218 | 217 | 3adant3 1133 |
. . . . . . . 8
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β (πβπ) β€ (πβπ)) |
219 | 188, 218 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β Ο β€ (πβπ)) |
220 | 204 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β (πβπ) β β) |
221 | 14 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β Ο β
β) |
222 | 220, 221 | letri3d 11304 |
. . . . . . 7
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β ((πβπ) = Ο β ((πβπ) β€ Ο β§ Ο β€ (πβπ)))) |
223 | 185, 219,
222 | mpbir2and 712 |
. . . . . 6
β’ ((π β§ π β (0...π) β§ (πβπ) = Ο) β (πβπ) = Ο) |
224 | 223 | rexlimdv3a 3157 |
. . . . 5
β’ (π β (βπ β (0...π)(πβπ) = Ο β (πβπ) = Ο)) |
225 | 178, 224 | mpd 15 |
. . . 4
β’ (π β (πβπ) = Ο) |
226 | | elfzoelz 13579 |
. . . . . . . . 9
β’ (π β (0..^π) β π β β€) |
227 | 226 | zred 12614 |
. . . . . . . 8
β’ (π β (0..^π) β π β β) |
228 | 227 | ltp1d 12092 |
. . . . . . 7
β’ (π β (0..^π) β π < (π + 1)) |
229 | 228 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β π < (π + 1)) |
230 | | elfzofz 13595 |
. . . . . . . 8
β’ (π β (0..^π) β π β (0...π)) |
231 | | fzofzp1 13676 |
. . . . . . . 8
β’ (π β (0..^π) β (π + 1) β (0...π)) |
232 | 230, 231 | jca 513 |
. . . . . . 7
β’ (π β (0..^π) β (π β (0...π) β§ (π + 1) β (0...π))) |
233 | | isorel 7276 |
. . . . . . 7
β’ ((π Isom < , < ((0...π), π») β§ (π β (0...π) β§ (π + 1) β (0...π))) β (π < (π + 1) β (πβπ) < (πβ(π + 1)))) |
234 | 93, 232, 233 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π < (π + 1) β (πβπ) < (πβ(π + 1)))) |
235 | 229, 234 | mpbid 231 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
236 | 235 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
237 | 173, 225,
236 | jca31 516 |
. . 3
β’ (π β (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
238 | 7 | fourierdlem2 44424 |
. . . 4
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
239 | 69, 238 | syl 17 |
. . 3
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
240 | 101, 237,
239 | mpbir2and 712 |
. 2
β’ (π β π β (πβπ)) |
241 | | fourierdlem114.g |
. . . . 5
β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) |
242 | 241 | reseq1i 5938 |
. . . 4
β’ (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = (((β D πΉ) βΎ (-Ο(,)Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) |
243 | 16 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β -Ο β
β*) |
244 | 17 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β Ο β
β*) |
245 | 179 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ(-Ο[,]Ο)) |
246 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β π β (0..^π)) |
247 | 243, 244,
245, 246 | fourierdlem27 44449 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β
(-Ο(,)Ο)) |
248 | 247 | resabs1d 5973 |
. . . 4
β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ (-Ο(,)Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))) |
249 | 242, 248 | eqtr2id 2790 |
. . 3
β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) = (πΊ βΎ ((πβπ)(,)(πβ(π + 1))))) |
250 | | fourierdlem114.gcn |
. . . 4
β’ (π β πΊ β (dom πΊβcnββ)) |
251 | 250, 7, 69, 240, 11, 167 | fourierdlem38 44460 |
. . 3
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
252 | 249, 251 | eqeltrd 2838 |
. 2
β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
253 | 249 | oveq1d 7377 |
. . 3
β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
254 | 250 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β πΊ β (dom πΊβcnββ)) |
255 | | fourierdlem114.rlim |
. . . . . 6
β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β
) |
256 | 255 | adantlr 714 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β
) |
257 | | fourierdlem114.llim |
. . . . . 6
β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β
) |
258 | 257 | adantlr 714 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β
) |
259 | 93 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π Isom < , < ((0...π), π»)) |
260 | 259, 94, 95 | 3syl 18 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆπ») |
261 | 81 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πΈβπ) β β) |
262 | 259, 165,
166 | 3syl 18 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ran π = π») |
263 | 254, 256,
258, 259, 260, 246, 235, 247, 261, 11, 262 | fourierdlem46 44467 |
. . . 4
β’ ((π β§ π β (0..^π)) β (((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) β β
β§ ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β β
)) |
264 | 263 | simpld 496 |
. . 3
β’ ((π β§ π β (0..^π)) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) β β
) |
265 | 253, 264 | eqnetrd 3012 |
. 2
β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) β β
) |
266 | 249 | oveq1d 7377 |
. . 3
β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
267 | 263 | simprd 497 |
. . 3
β’ ((π β§ π β (0..^π)) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β β
) |
268 | 266, 267 | eqnetrd 3012 |
. 2
β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β β
) |
269 | | fourierdlem114.a |
. 2
β’ π΄ = (π β β0 β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
270 | | fourierdlem114.b |
. 2
β’ π΅ = (π β β β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
271 | | fourierdlem114.s |
. 2
β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
272 | 83 | tpid3 4739 |
. . . . 5
β’ (πΈβπ) β {-Ο, Ο, (πΈβπ)} |
273 | | elun1 4141 |
. . . . 5
β’ ((πΈβπ) β {-Ο, Ο, (πΈβπ)} β (πΈβπ) β ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ))) |
274 | 272, 273 | mp1i 13 |
. . . 4
β’ (π β (πΈβπ) β ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ))) |
275 | 274, 11 | eleqtrrdi 2849 |
. . 3
β’ (π β (πΈβπ) β π») |
276 | 275, 167 | eleqtrrd 2841 |
. 2
β’ (π β (πΈβπ) β ran π) |
277 | 1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276 | fourierdlem113 44534 |
1
β’ (π β (seq1( + , π) β (((πΏ + π
) / 2) β ((π΄β0) / 2)) β§ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π
) / 2))) |