Step | Hyp | Ref
| Expression |
1 | | fourierdlem88.o |
. 2
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
2 | | fourierdlem88.m |
. 2
β’ (π β π β β) |
3 | | pire 25853 |
. . . . 5
β’ Ο
β β |
4 | 3 | a1i 11 |
. . . 4
β’ (π β Ο β
β) |
5 | 4 | renegcld 11592 |
. . 3
β’ (π β -Ο β
β) |
6 | | fourierdlem88.v |
. . . . . . 7
β’ (π β π β (πβπ)) |
7 | | fourierdlem88.1 |
. . . . . . . . 9
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
8 | 7 | fourierdlem2 44452 |
. . . . . . . 8
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
9 | 2, 8 | syl 17 |
. . . . . . 7
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
10 | 6, 9 | mpbid 231 |
. . . . . 6
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
11 | 10 | simpld 496 |
. . . . 5
β’ (π β π β (β βm
(0...π))) |
12 | | elmapi 8795 |
. . . . 5
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
13 | | frn 6681 |
. . . . 5
β’ (π:(0...π)βΆβ β ran π β
β) |
14 | 11, 12, 13 | 3syl 18 |
. . . 4
β’ (π β ran π β β) |
15 | | fourierdlem88.x |
. . . 4
β’ (π β π β ran π) |
16 | 14, 15 | sseldd 3949 |
. . 3
β’ (π β π β β) |
17 | | fourierdlem88.q |
. . 3
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
18 | 5, 4, 16, 7, 1, 2,
6, 17 | fourierdlem14 44464 |
. 2
β’ (π β π β (πβπ)) |
19 | | fourierdlem88.f |
. . . . . . 7
β’ (π β πΉ:ββΆβ) |
20 | | ioossre 13336 |
. . . . . . . . . 10
β’ (π(,)+β) β
β |
21 | 20 | a1i 11 |
. . . . . . . . 9
β’ (π β (π(,)+β) β
β) |
22 | 19, 21 | fssresd 6715 |
. . . . . . . 8
β’ (π β (πΉ βΎ (π(,)+β)):(π(,)+β)βΆβ) |
23 | | ax-resscn 11118 |
. . . . . . . . 9
β’ β
β β |
24 | 21, 23 | sstrdi 3960 |
. . . . . . . 8
β’ (π β (π(,)+β) β
β) |
25 | | eqid 2732 |
. . . . . . . . 9
β’
(TopOpenββfld) =
(TopOpenββfld) |
26 | | pnfxr 11219 |
. . . . . . . . . 10
β’ +β
β β* |
27 | 26 | a1i 11 |
. . . . . . . . 9
β’ (π β +β β
β*) |
28 | 16 | ltpnfd 13052 |
. . . . . . . . 9
β’ (π β π < +β) |
29 | 25, 27, 16, 28 | lptioo1cn 43989 |
. . . . . . . 8
β’ (π β π β
((limPtβ(TopOpenββfld))β(π(,)+β))) |
30 | | fourierdlem88.y |
. . . . . . . 8
β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) |
31 | 22, 24, 29, 30 | limcrecl 43972 |
. . . . . . 7
β’ (π β π β β) |
32 | | ioossre 13336 |
. . . . . . . . . 10
β’
(-β(,)π)
β β |
33 | 32 | a1i 11 |
. . . . . . . . 9
β’ (π β (-β(,)π) β
β) |
34 | 19, 33 | fssresd 6715 |
. . . . . . . 8
β’ (π β (πΉ βΎ (-β(,)π)):(-β(,)π)βΆβ) |
35 | 33, 23 | sstrdi 3960 |
. . . . . . . 8
β’ (π β (-β(,)π) β
β) |
36 | | mnfxr 11222 |
. . . . . . . . . 10
β’ -β
β β* |
37 | 36 | a1i 11 |
. . . . . . . . 9
β’ (π β -β β
β*) |
38 | 16 | mnfltd 13055 |
. . . . . . . . 9
β’ (π β -β < π) |
39 | 25, 37, 16, 38 | lptioo2cn 43988 |
. . . . . . . 8
β’ (π β π β
((limPtβ(TopOpenββfld))β(-β(,)π))) |
40 | | fourierdlem88.w |
. . . . . . . 8
β’ (π β π β ((πΉ βΎ (-β(,)π)) limβ π)) |
41 | 34, 35, 39, 40 | limcrecl 43972 |
. . . . . . 7
β’ (π β π β β) |
42 | | fourierdlem88.h |
. . . . . . 7
β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
43 | | fourierdlem88.k |
. . . . . . 7
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
44 | | fourierdlem88.u |
. . . . . . 7
β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) |
45 | 19, 16, 31, 41, 42, 43, 44 | fourierdlem55 44504 |
. . . . . 6
β’ (π β π:(-Ο[,]Ο)βΆβ) |
46 | 45 | ffvelcdmda 7041 |
. . . . 5
β’ ((π β§ π β (-Ο[,]Ο)) β (πβπ ) β β) |
47 | | fourierdlem88.n |
. . . . . . 7
β’ (π β π β β) |
48 | | fourierdlem88.s |
. . . . . . . 8
β’ π = (π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π ))) |
49 | 48 | fourierdlem5 44455 |
. . . . . . 7
β’ (π β β β π:(-Ο[,]Ο)βΆβ) |
50 | 47, 49 | syl 17 |
. . . . . 6
β’ (π β π:(-Ο[,]Ο)βΆβ) |
51 | 50 | ffvelcdmda 7041 |
. . . . 5
β’ ((π β§ π β (-Ο[,]Ο)) β (πβπ ) β β) |
52 | 46, 51 | remulcld 11195 |
. . . 4
β’ ((π β§ π β (-Ο[,]Ο)) β ((πβπ ) Β· (πβπ )) β β) |
53 | 52 | recnd 11193 |
. . 3
β’ ((π β§ π β (-Ο[,]Ο)) β ((πβπ ) Β· (πβπ )) β β) |
54 | | fourierdlem88.g |
. . 3
β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) |
55 | 53, 54 | fmptd 7068 |
. 2
β’ (π β πΊ:(-Ο[,]Ο)βΆβ) |
56 | | ssid 3970 |
. . . 4
β’ β
β β |
57 | | cncfss 24300 |
. . . 4
β’ ((β
β β β§ β β β) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
58 | 23, 56, 57 | mp2an 691 |
. . 3
β’ (((πβπ)(,)(πβ(π + 1)))βcnββ) β (((πβπ)(,)(πβ(π + 1)))βcnββ) |
59 | 19 | adantr 482 |
. . . 4
β’ ((π β§ π β (0..^π)) β πΉ:ββΆβ) |
60 | 1, 2, 18 | fourierdlem15 44465 |
. . . . . 6
β’ (π β π:(0...π)βΆ(-Ο[,]Ο)) |
61 | 60 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ(-Ο[,]Ο)) |
62 | | elfzofz 13599 |
. . . . . 6
β’ (π β (0..^π) β π β (0...π)) |
63 | 62 | adantl 483 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
64 | 61, 63 | ffvelcdmd 7042 |
. . . 4
β’ ((π β§ π β (0..^π)) β (πβπ) β (-Ο[,]Ο)) |
65 | | fzofzp1 13680 |
. . . . . 6
β’ (π β (0..^π) β (π + 1) β (0...π)) |
66 | 65 | adantl 483 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
67 | 61, 66 | ffvelcdmd 7042 |
. . . 4
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
(-Ο[,]Ο)) |
68 | 16 | adantr 482 |
. . . 4
β’ ((π β§ π β (0..^π)) β π β β) |
69 | 7, 2, 6, 15 | fourierdlem12 44462 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) |
70 | 68 | recnd 11193 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β β) |
71 | 70 | addlidd 11366 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (0 + π) = π) |
72 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β Ο β
β) |
73 | 72 | renegcld 11592 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β -Ο β
β) |
74 | 73, 68 | readdcld 11194 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (-Ο + π) β β) |
75 | 72, 68 | readdcld 11194 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (Ο + π) β β) |
76 | 74, 75 | iccssred 13362 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((-Ο + π)[,](Ο + π)) β β) |
77 | 7, 2, 6 | fourierdlem15 44465 |
. . . . . . . . . . . . . . 15
β’ (π β π:(0...π)βΆ((-Ο + π)[,](Ο + π))) |
78 | 77 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ((-Ο + π)[,](Ο + π))) |
79 | 78, 63 | ffvelcdmd 7042 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β ((-Ο + π)[,](Ο + π))) |
80 | 76, 79 | sseldd 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
81 | 80, 68 | resubcld 11593 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) β β) |
82 | 17 | fvmpt2 6965 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ ((πβπ) β π) β β) β (πβπ) = ((πβπ) β π)) |
83 | 63, 81, 82 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβπ) = ((πβπ) β π)) |
84 | 83 | oveq1d 7378 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((πβπ) + π) = (((πβπ) β π) + π)) |
85 | 80 | recnd 11193 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
86 | 85, 70 | npcand 11526 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (((πβπ) β π) + π) = (πβπ)) |
87 | 84, 86 | eqtrd 2772 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πβπ) + π) = (πβπ)) |
88 | | fveq2 6848 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
89 | 88 | oveq1d 7378 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
90 | 89 | cbvmptv 5224 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
91 | 17, 90 | eqtri 2760 |
. . . . . . . . . . . 12
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
92 | 91 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π = (π β (0...π) β¦ ((πβπ) β π))) |
93 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π = (π + 1)) β π = (π + 1)) |
94 | 93 | fveq2d 6852 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π = (π + 1)) β (πβπ) = (πβ(π + 1))) |
95 | 94 | oveq1d 7378 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π = (π + 1)) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
96 | 78, 66 | ffvelcdmd 7042 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β ((-Ο + π)[,](Ο + π))) |
97 | 76, 96 | sseldd 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
98 | 97, 68 | resubcld 11593 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β π) β β) |
99 | 92, 95, 66, 98 | fvmptd 6961 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
100 | 99 | oveq1d 7378 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) + π) = (((πβ(π + 1)) β π) + π)) |
101 | 97 | recnd 11193 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
102 | 101, 70 | npcand 11526 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (((πβ(π + 1)) β π) + π) = (πβ(π + 1))) |
103 | 100, 102 | eqtrd 2772 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) + π) = (πβ(π + 1))) |
104 | 87, 103 | oveq12d 7381 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (((πβπ) + π)(,)((πβ(π + 1)) + π)) = ((πβπ)(,)(πβ(π + 1)))) |
105 | 71, 104 | eleq12d 2827 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((0 + π) β (((πβπ) + π)(,)((πβ(π + 1)) + π)) β π β ((πβπ)(,)(πβ(π + 1))))) |
106 | 69, 105 | mtbird 325 |
. . . . 5
β’ ((π β§ π β (0..^π)) β Β¬ (0 + π) β (((πβπ) + π)(,)((πβ(π + 1)) + π))) |
107 | | 0red 11168 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β 0 β β) |
108 | 83, 81 | eqeltrd 2833 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
109 | 99, 98 | eqeltrd 2833 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
110 | 107, 108,
109, 68 | eliooshift 43846 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (0 β ((πβπ)(,)(πβ(π + 1))) β (0 + π) β (((πβπ) + π)(,)((πβ(π + 1)) + π)))) |
111 | 106, 110 | mtbird 325 |
. . . 4
β’ ((π β§ π β (0..^π)) β Β¬ 0 β ((πβπ)(,)(πβ(π + 1)))) |
112 | | fourierdlem88.fcn |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
113 | 104 | reseq2d 5943 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πΉ βΎ (((πβπ) + π)(,)((πβ(π + 1)) + π))) = (πΉ βΎ ((πβπ)(,)(πβ(π + 1))))) |
114 | 104 | oveq1d 7378 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((((πβπ) + π)(,)((πβ(π + 1)) + π))βcnββ) = (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
115 | 112, 113,
114 | 3eltr4d 2848 |
. . . 4
β’ ((π β§ π β (0..^π)) β (πΉ βΎ (((πβπ) + π)(,)((πβ(π + 1)) + π))) β ((((πβπ) + π)(,)((πβ(π + 1)) + π))βcnββ)) |
116 | 31 | adantr 482 |
. . . 4
β’ ((π β§ π β (0..^π)) β π β β) |
117 | 41 | adantr 482 |
. . . 4
β’ ((π β§ π β (0..^π)) β π β β) |
118 | 47 | adantr 482 |
. . . 4
β’ ((π β§ π β (0..^π)) β π β β) |
119 | 59, 64, 67, 68, 111, 115, 116, 117, 42, 43, 44, 118, 48, 54 | fourierdlem78 44527 |
. . 3
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
120 | 58, 119 | sselid 3946 |
. 2
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
121 | | eqid 2732 |
. . . 4
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) |
122 | | eqid 2732 |
. . . 4
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) |
123 | | eqid 2732 |
. . . 4
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ ))) |
124 | 3 | renegcli 11472 |
. . . . . . . . . . 11
β’ -Ο
β β |
125 | 124 | rexri 11223 |
. . . . . . . . . 10
β’ -Ο
β β* |
126 | 125 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β -Ο β
β*) |
127 | 3 | rexri 11223 |
. . . . . . . . . 10
β’ Ο
β β* |
128 | 127 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β Ο β
β*) |
129 | 61 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π:(0...π)βΆ(-Ο[,]Ο)) |
130 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (0..^π)) |
131 | 126, 128,
129, 130 | fourierdlem8 44458 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πβπ)[,](πβ(π + 1))) β
(-Ο[,]Ο)) |
132 | | ioossicc 13361 |
. . . . . . . . . 10
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
133 | 132 | sseli 3944 |
. . . . . . . . 9
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β ((πβπ)[,](πβ(π + 1)))) |
134 | 133 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β ((πβπ)[,](πβ(π + 1)))) |
135 | 131, 134 | sseldd 3949 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (-Ο[,]Ο)) |
136 | 19, 16, 31, 41, 42 | fourierdlem9 44459 |
. . . . . . . . . 10
β’ (π β π»:(-Ο[,]Ο)βΆβ) |
137 | 136 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π»:(-Ο[,]Ο)βΆβ) |
138 | 137, 135 | ffvelcdmd 7042 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π»βπ ) β β) |
139 | 43 | fourierdlem43 44493 |
. . . . . . . . . 10
β’ πΎ:(-Ο[,]Ο)βΆβ |
140 | 139 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β πΎ:(-Ο[,]Ο)βΆβ) |
141 | 140, 135 | ffvelcdmd 7042 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΎβπ ) β β) |
142 | 138, 141 | remulcld 11195 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((π»βπ ) Β· (πΎβπ )) β β) |
143 | 44 | fvmpt2 6965 |
. . . . . . 7
β’ ((π β (-Ο[,]Ο) β§
((π»βπ ) Β· (πΎβπ )) β β) β (πβπ ) = ((π»βπ ) Β· (πΎβπ ))) |
144 | 135, 142,
143 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ ) = ((π»βπ ) Β· (πΎβπ ))) |
145 | 144, 142 | eqeltrd 2833 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ ) β β) |
146 | 145 | recnd 11193 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ ) β β) |
147 | 47, 48 | fourierdlem18 44468 |
. . . . . . . . 9
β’ (π β π β ((-Ο[,]Ο)βcnββ)) |
148 | | cncff 24294 |
. . . . . . . . 9
β’ (π β
((-Ο[,]Ο)βcnββ)
β π:(-Ο[,]Ο)βΆβ) |
149 | 147, 148 | syl 17 |
. . . . . . . 8
β’ (π β π:(-Ο[,]Ο)βΆβ) |
150 | 149 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π:(-Ο[,]Ο)βΆβ) |
151 | 150 | adantr 482 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π:(-Ο[,]Ο)βΆβ) |
152 | 151, 135 | ffvelcdmd 7042 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ ) β β) |
153 | 152 | recnd 11193 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ ) β β) |
154 | | eqid 2732 |
. . . . . 6
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ )) |
155 | | eqid 2732 |
. . . . . 6
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΎβπ )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΎβπ )) |
156 | | eqid 2732 |
. . . . . 6
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π»βπ ) Β· (πΎβπ ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π»βπ ) Β· (πΎβπ ))) |
157 | 138 | recnd 11193 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π»βπ ) β β) |
158 | 141 | recnd 11193 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΎβπ ) β β) |
159 | | fourierdlem88.r |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
160 | | fourierdlem88.i |
. . . . . . . 8
β’ πΌ = (β D πΉ) |
161 | | fourierdlem88.ifn |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πΌ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
162 | 23 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β β β
β) |
163 | 161, 162 | fssd 6692 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πΌ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
164 | | fourierdlem88.d |
. . . . . . . 8
β’ (π β π· β ((πΌ βΎ (π(,)+β)) limβ π)) |
165 | | eqid 2732 |
. . . . . . . 8
β’ if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) = if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) |
166 | 16, 7, 19, 15, 30, 41, 42, 2, 6, 159, 17, 1, 160, 163, 164, 165 | fourierdlem75 44524 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
167 | 136 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π»:(-Ο[,]Ο)βΆβ) |
168 | 125 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β -Ο β
β*) |
169 | 127 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β Ο β
β*) |
170 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π β (0..^π)) |
171 | 168, 169,
61, 170 | fourierdlem8 44458 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β
(-Ο[,]Ο)) |
172 | 132, 171 | sstrid 3959 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β
(-Ο[,]Ο)) |
173 | 167, 172 | feqresmpt 6917 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π» βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ ))) |
174 | 173 | oveq1d 7378 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ )) limβ (πβπ))) |
175 | 166, 174 | eleqtrd 2835 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ )) limβ (πβπ))) |
176 | | limcresi 25287 |
. . . . . . . 8
β’ (πΎ limβ (πβπ)) β ((πΎ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) |
177 | 43 | fourierdlem62 44511 |
. . . . . . . . . 10
β’ πΎ β
((-Ο[,]Ο)βcnββ) |
178 | 177 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β πΎ β ((-Ο[,]Ο)βcnββ)) |
179 | 178, 64 | cnlimci 25291 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πΎβ(πβπ)) β (πΎ limβ (πβπ))) |
180 | 176, 179 | sselid 3946 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πΎβ(πβπ)) β ((πΎ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
181 | 139 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β πΎ:(-Ο[,]Ο)βΆβ) |
182 | 181, 172 | feqresmpt 6917 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πΎ βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΎβπ ))) |
183 | 182 | oveq1d 7378 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((πΎ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΎβπ )) limβ (πβπ))) |
184 | 180, 183 | eleqtrd 2835 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πΎβ(πβπ)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΎβπ )) limβ (πβπ))) |
185 | 154, 155,
156, 157, 158, 175, 184 | mullimc 43959 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) Β· (πΎβ(πβπ))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π»βπ ) Β· (πΎβπ ))) limβ (πβπ))) |
186 | 144 | eqcomd 2738 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((π»βπ ) Β· (πΎβπ )) = (πβπ )) |
187 | 186 | mpteq2dva 5211 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π»βπ ) Β· (πΎβπ ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ ))) |
188 | 187 | oveq1d 7378 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π»βπ ) Β· (πΎβπ ))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβπ))) |
189 | 185, 188 | eleqtrd 2835 |
. . . 4
β’ ((π β§ π β (0..^π)) β (if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) Β· (πΎβ(πβπ))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβπ))) |
190 | | limcresi 25287 |
. . . . . 6
β’ (π limβ (πβπ)) β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) |
191 | 147 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π β ((-Ο[,]Ο)βcnββ)) |
192 | 191, 64 | cnlimci 25291 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πβ(πβπ)) β (π limβ (πβπ))) |
193 | 190, 192 | sselid 3946 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πβ(πβπ)) β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
194 | 150, 172 | feqresmpt 6917 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ ))) |
195 | 194 | oveq1d 7378 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβπ))) |
196 | 193, 195 | eleqtrd 2835 |
. . . 4
β’ ((π β§ π β (0..^π)) β (πβ(πβπ)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβπ))) |
197 | 121, 122,
123, 146, 153, 189, 196 | mullimc 43959 |
. . 3
β’ ((π β§ π β (0..^π)) β ((if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) Β· (πΎβ(πβπ))) Β· (πβ(πβπ))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ ))) limβ (πβπ))) |
198 | 52, 54 | fmptd 7068 |
. . . . . . 7
β’ (π β πΊ:(-Ο[,]Ο)βΆβ) |
199 | 198 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β πΊ:(-Ο[,]Ο)βΆβ) |
200 | 199, 172 | feqresmpt 6917 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΊβπ ))) |
201 | 145, 152 | remulcld 11195 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πβπ ) Β· (πβπ )) β β) |
202 | 54 | fvmpt2 6965 |
. . . . . . 7
β’ ((π β (-Ο[,]Ο) β§
((πβπ ) Β· (πβπ )) β β) β (πΊβπ ) = ((πβπ ) Β· (πβπ ))) |
203 | 135, 201,
202 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΊβπ ) = ((πβπ ) Β· (πβπ ))) |
204 | 203 | mpteq2dva 5211 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΊβπ )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ )))) |
205 | 200, 204 | eqtr2d 2773 |
. . . 4
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ ))) = (πΊ βΎ ((πβπ)(,)(πβ(π + 1))))) |
206 | 205 | oveq1d 7378 |
. . 3
β’ ((π β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ ))) limβ (πβπ)) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
207 | 197, 206 | eleqtrd 2835 |
. 2
β’ ((π β§ π β (0..^π)) β ((if((πβπ) = π, π·, ((π
β if((πβπ) < π, π, π)) / (πβπ))) Β· (πΎβ(πβπ))) Β· (πβ(πβπ))) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
208 | | fourierdlem88.l |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
209 | | fourierdlem88.c |
. . . . . . . 8
β’ (π β πΆ β ((πΌ βΎ (-β(,)π)) limβ π)) |
210 | | eqid 2732 |
. . . . . . . 8
β’ if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) = if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) |
211 | 16, 7, 19, 15, 31, 40, 42, 2, 6, 208, 17, 1, 160, 161, 209, 210 | fourierdlem74 44523 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
212 | 173 | oveq1d 7378 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ )) limβ (πβ(π + 1)))) |
213 | 211, 212 | eleqtrd 2835 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ )) limβ (πβ(π + 1)))) |
214 | | limcresi 25287 |
. . . . . . . 8
β’ (πΎ limβ (πβ(π + 1))) β ((πΎ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) |
215 | 178, 67 | cnlimci 25291 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πΎβ(πβ(π + 1))) β (πΎ limβ (πβ(π + 1)))) |
216 | 214, 215 | sselid 3946 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πΎβ(πβ(π + 1))) β ((πΎ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
217 | 182 | oveq1d 7378 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((πΎ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΎβπ )) limβ (πβ(π + 1)))) |
218 | 216, 217 | eleqtrd 2835 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πΎβ(πβ(π + 1))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΎβπ )) limβ (πβ(π + 1)))) |
219 | 154, 155,
156, 157, 158, 213, 218 | mullimc 43959 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) Β· (πΎβ(πβ(π + 1)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π»βπ ) Β· (πΎβπ ))) limβ (πβ(π + 1)))) |
220 | 187 | oveq1d 7378 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π»βπ ) Β· (πΎβπ ))) limβ (πβ(π + 1))) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβ(π + 1)))) |
221 | 219, 220 | eleqtrd 2835 |
. . . 4
β’ ((π β§ π β (0..^π)) β (if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) Β· (πΎβ(πβ(π + 1)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβ(π + 1)))) |
222 | | limcresi 25287 |
. . . . . 6
β’ (π limβ (πβ(π + 1))) β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) |
223 | 191, 67 | cnlimci 25291 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πβ(πβ(π + 1))) β (π limβ (πβ(π + 1)))) |
224 | 222, 223 | sselid 3946 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πβ(πβ(π + 1))) β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
225 | 194 | oveq1d 7378 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβ(π + 1)))) |
226 | 224, 225 | eleqtrd 2835 |
. . . 4
β’ ((π β§ π β (0..^π)) β (πβ(πβ(π + 1))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πβπ )) limβ (πβ(π + 1)))) |
227 | 121, 122,
123, 146, 153, 221, 226 | mullimc 43959 |
. . 3
β’ ((π β§ π β (0..^π)) β ((if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) Β· (πΎβ(πβ(π + 1)))) Β· (πβ(πβ(π + 1)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ ))) limβ (πβ(π + 1)))) |
228 | 205 | oveq1d 7378 |
. . 3
β’ ((π β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πβπ ) Β· (πβπ ))) limβ (πβ(π + 1))) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
229 | 227, 228 | eleqtrd 2835 |
. 2
β’ ((π β§ π β (0..^π)) β ((if((πβ(π + 1)) = π, πΆ, ((πΏ β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) Β· (πΎβ(πβ(π + 1)))) Β· (πβ(πβ(π + 1)))) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
230 | 1, 2, 18, 55, 120, 207, 229 | fourierdlem69 44518 |
1
β’ (π β πΊ β
πΏ1) |