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