Step | Hyp | Ref
| Expression |
1 | | fourierdlem84.o |
. 2
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
2 | | fourierdlem84.m |
. 2
β’ (π β π β β) |
3 | | fourierdlem84.1 |
. . 3
β’ (π β π΄ β β) |
4 | | fourierdlem84.2 |
. . 3
β’ (π β π΅ β β) |
5 | | fourierdlem84.xre |
. . 3
β’ (π β π β β) |
6 | | fourierdlem84.p |
. . 3
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
7 | | fourierdlem84.v |
. . 3
β’ (π β π β (πβπ)) |
8 | | fourierdlem84.q |
. . 3
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
9 | 3, 4, 5, 6, 1, 2, 7, 8 | fourierdlem14 44452 |
. 2
β’ (π β π β (πβπ)) |
10 | | fourierdlem84.f |
. . . . . . 7
β’ (π β πΉ:ββΆβ) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (π΄[,]π΅)) β πΉ:ββΆβ) |
12 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (π΄[,]π΅)) β π β β) |
13 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π΄[,]π΅)) β π΄ β β) |
14 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π΄[,]π΅)) β π΅ β β) |
15 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (π΄[,]π΅)) β π β (π΄[,]π΅)) |
16 | | eliccre 43833 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β β§ π β (π΄[,]π΅)) β π β β) |
17 | 13, 14, 15, 16 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (π΄[,]π΅)) β π β β) |
18 | 12, 17 | readdcld 11192 |
. . . . . 6
β’ ((π β§ π β (π΄[,]π΅)) β (π + π ) β β) |
19 | 11, 18 | ffvelcdmd 7040 |
. . . . 5
β’ ((π β§ π β (π΄[,]π΅)) β (πΉβ(π + π )) β β) |
20 | | fourierdlem84.d |
. . . . . . . 8
β’ (π β π· β (ββcnββ)) |
21 | | cncff 24279 |
. . . . . . . 8
β’ (π· β (ββcnββ) β π·:ββΆβ) |
22 | 20, 21 | syl 17 |
. . . . . . 7
β’ (π β π·:ββΆβ) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (π΄[,]π΅)) β π·:ββΆβ) |
24 | 23, 17 | ffvelcdmd 7040 |
. . . . 5
β’ ((π β§ π β (π΄[,]π΅)) β (π·βπ ) β β) |
25 | 19, 24 | remulcld 11193 |
. . . 4
β’ ((π β§ π β (π΄[,]π΅)) β ((πΉβ(π + π )) Β· (π·βπ )) β β) |
26 | 25 | recnd 11191 |
. . 3
β’ ((π β§ π β (π΄[,]π΅)) β ((πΉβ(π + π )) Β· (π·βπ )) β β) |
27 | | fourierdlem84.g |
. . 3
β’ πΊ = (π β (π΄[,]π΅) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) |
28 | 26, 27 | fmptd 7066 |
. 2
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
29 | 27 | a1i 11 |
. . . . 5
β’ ((π β§ π β (0..^π)) β πΊ = (π β (π΄[,]π΅) β¦ ((πΉβ(π + π )) Β· (π·βπ )))) |
30 | 29 | reseq1d 5940 |
. . . 4
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π β (π΄[,]π΅) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) βΎ ((πβπ)(,)(πβ(π + 1))))) |
31 | | ioossicc 13359 |
. . . . . 6
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
32 | 3 | rexrd 11213 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
33 | 32 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π΄ β
β*) |
34 | 4 | rexrd 11213 |
. . . . . . . 8
β’ (π β π΅ β
β*) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π΅ β
β*) |
36 | 1, 2, 9 | fourierdlem15 44453 |
. . . . . . . 8
β’ (π β π:(0...π)βΆ(π΄[,]π΅)) |
37 | 36 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ(π΄[,]π΅)) |
38 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π β (0..^π)) |
39 | 33, 35, 37, 38 | fourierdlem8 44446 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β (π΄[,]π΅)) |
40 | 31, 39 | sstrid 3959 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β (π΄[,]π΅)) |
41 | 40 | resmptd 5998 |
. . . 4
β’ ((π β§ π β (0..^π)) β ((π β (π΄[,]π΅) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ )))) |
42 | 30, 41 | eqtrd 2773 |
. . 3
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ )))) |
43 | 3, 5 | readdcld 11192 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ + π) β β) |
44 | 4, 5 | readdcld 11192 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ + π) β β) |
45 | 43, 44 | iccssred 13360 |
. . . . . . . . . . . . 13
β’ (π β ((π΄ + π)[,](π΅ + π)) β β) |
46 | 45 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((π΄ + π)[,](π΅ + π)) β β) |
47 | 6, 2, 7 | fourierdlem15 44453 |
. . . . . . . . . . . . . 14
β’ (π β π:(0...π)βΆ((π΄ + π)[,](π΅ + π))) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ((π΄ + π)[,](π΅ + π))) |
49 | | elfzofz 13597 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β π β (0...π)) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
51 | 48, 50 | ffvelcdmd 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβπ) β ((π΄ + π)[,](π΅ + π))) |
52 | 46, 51 | sseldd 3949 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
53 | 52 | rexrd 11213 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
54 | 53 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
55 | | fzofzp1 13678 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β (π + 1) β (0...π)) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
57 | 48, 56 | ffvelcdmd 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β ((π΄ + π)[,](π΅ + π))) |
58 | 46, 57 | sseldd 3949 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
59 | 58 | rexrd 11213 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
60 | 59 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
61 | 5 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
62 | | elioore 13303 |
. . . . . . . . . . 11
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β β) |
63 | 62 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
64 | 61, 63 | readdcld 11192 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
65 | 5 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β π β β) |
67 | 3, 4 | iccssred 13360 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄[,]π΅) β β) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π΄[,]π΅) β β) |
69 | 37, 50 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (πβπ) β (π΄[,]π΅)) |
70 | 68, 69 | sseldd 3949 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
71 | 70 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
72 | 66, 71 | addcomd 11365 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (π + (πβπ)) = ((πβπ) + π)) |
73 | 5 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π β β) |
74 | 52, 73 | resubcld 11591 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) β β) |
75 | 8 | fvmpt2 6963 |
. . . . . . . . . . . . . 14
β’ ((π β (0...π) β§ ((πβπ) β π) β β) β (πβπ) = ((πβπ) β π)) |
76 | 50, 74, 75 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) = ((πβπ) β π)) |
77 | 76 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((πβπ) + π) = (((πβπ) β π) + π)) |
78 | 52 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
79 | 78, 66 | npcand 11524 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (((πβπ) β π) + π) = (πβπ)) |
80 | 72, 77, 79 | 3eqtrrd 2778 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (πβπ) = (π + (πβπ))) |
81 | 80 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) = (π + (πβπ))) |
82 | 70 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
83 | 70 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
84 | 83 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
85 | 37, 68 | fssd 6690 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
86 | 85, 56 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
87 | 86 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
88 | 87 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
89 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β ((πβπ)(,)(πβ(π + 1)))) |
90 | | ioogtlb 43823 |
. . . . . . . . . . . 12
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
91 | 84, 88, 89, 90 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
92 | 82, 63, 61, 91 | ltadd2dd 11322 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβπ)) < (π + π )) |
93 | 81, 92 | eqbrtrd 5131 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π )) |
94 | 86 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
95 | | iooltub 43838 |
. . . . . . . . . . . 12
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
96 | 84, 88, 89, 95 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
97 | 63, 94, 61, 96 | ltadd2dd 11322 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (π + (πβ(π + 1)))) |
98 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πβπ) = (πβπ)) |
99 | 98 | oveq1d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
100 | 99 | cbvmptv 5222 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
101 | 8, 100 | eqtri 2761 |
. . . . . . . . . . . . . . 15
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π = (π β (0...π) β¦ ((πβπ) β π))) |
103 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
104 | 103 | oveq1d 7376 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π = (π + 1)) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
106 | 58, 73 | resubcld 11591 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β π) β β) |
107 | 102, 105,
56, 106 | fvmptd 6959 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
108 | 107 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (π + (πβ(π + 1))) = (π + ((πβ(π + 1)) β π))) |
109 | 58 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
110 | 66, 109 | pncan3d 11523 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (π + ((πβ(π + 1)) β π)) = (πβ(π + 1))) |
111 | 108, 110 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
112 | 111 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
113 | 97, 112 | breqtrd 5135 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (πβ(π + 1))) |
114 | 54, 60, 64, 93, 113 | eliood 43826 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β ((πβπ)(,)(πβ(π + 1)))) |
115 | | fvres 6865 |
. . . . . . . 8
β’ ((π + π ) β ((πβπ)(,)(πβ(π + 1))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π )) = (πΉβ(π + π ))) |
116 | 114, 115 | syl 17 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π )) = (πΉβ(π + π ))) |
117 | 116 | eqcomd 2739 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π ))) |
118 | 117 | mpteq2dva 5209 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π )))) |
119 | | ioosscn 13335 |
. . . . . . 7
β’ ((πβπ)(,)(πβ(π + 1))) β β |
120 | 119 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
121 | | fourierdlem84.fcn |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
122 | | ioosscn 13335 |
. . . . . . 7
β’ ((πβπ)(,)(πβ(π + 1))) β β |
123 | 122 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
124 | 120, 121,
123, 66, 114 | fourierdlem23 44461 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
125 | 118, 124 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
126 | | eqid 2733 |
. . . . 5
β’ (π β β β¦ (π·βπ )) = (π β β β¦ (π·βπ )) |
127 | | ax-resscn 11116 |
. . . . . . . 8
β’ β
β β |
128 | | ssid 3970 |
. . . . . . . 8
β’ β
β β |
129 | | cncfss 24285 |
. . . . . . . 8
β’ ((β
β β β§ β β β) β (ββcnββ) β (ββcnββ)) |
130 | 127, 128,
129 | mp2an 691 |
. . . . . . 7
β’
(ββcnββ)
β (ββcnββ) |
131 | 22 | feqmptd 6914 |
. . . . . . . . 9
β’ (π β π· = (π β β β¦ (π·βπ ))) |
132 | 131 | eqcomd 2739 |
. . . . . . . 8
β’ (π β (π β β β¦ (π·βπ )) = π·) |
133 | 132, 20 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (π β β β¦ (π·βπ )) β (ββcnββ)) |
134 | 130, 133 | sselid 3946 |
. . . . . 6
β’ (π β (π β β β¦ (π·βπ )) β (ββcnββ)) |
135 | 134 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π β β β¦ (π·βπ )) β (ββcnββ)) |
136 | 40, 68 | sstrd 3958 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
137 | 128 | a1i 11 |
. . . . 5
β’ ((π β§ π β (0..^π)) β β β
β) |
138 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π·:ββΆβ) |
139 | 62 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
140 | 138, 139 | ffvelcdmd 7040 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π·βπ ) β β) |
141 | 140 | recnd 11191 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π·βπ ) β β) |
142 | 141 | adantlr 714 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π·βπ ) β β) |
143 | 126, 135,
136, 137, 142 | cncfmptssg 44202 |
. . . 4
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ )) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
144 | 125, 143 | mulcncf 24833 |
. . 3
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
145 | 42, 144 | eqeltrd 2834 |
. 2
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
146 | | eqid 2733 |
. . . 4
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) |
147 | | eqid 2733 |
. . . 4
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ )) |
148 | | eqid 2733 |
. . . 4
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) |
149 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β πΉ:ββΆβ) |
150 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
151 | 150, 139 | readdcld 11192 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
152 | 149, 151 | ffvelcdmd 7040 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
153 | 152 | recnd 11191 |
. . . . 5
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
154 | 153 | adantlr 714 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
155 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β πΉ:ββΆβ) |
156 | | ioossre 13334 |
. . . . . 6
β’ ((πβπ)(,)(πβ(π + 1))) β β |
157 | 156 | a1i 11 |
. . . . 5
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
158 | 82, 91 | gtned 11298 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (πβπ)) |
159 | | fourierdlem84.r |
. . . . . 6
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
160 | 80 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβπ)))) |
161 | 159, 160 | eleqtrd 2836 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβπ)))) |
162 | 155, 73, 136, 146, 114, 157, 158, 161, 71 | fourierdlem53 44490 |
. . . 4
β’ ((π β§ π β (0..^π)) β π
β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβπ))) |
163 | | limcresi 25272 |
. . . . . 6
β’ ((π β β β¦ (π·βπ )) limβ (πβπ)) β (((π β β β¦ (π·βπ )) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) |
164 | 130, 20 | sselid 3946 |
. . . . . . . . 9
β’ (π β π· β (ββcnββ)) |
165 | 164 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π· β (ββcnββ)) |
166 | 165, 70 | cnlimci 25276 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π·β(πβπ)) β (π· limβ (πβπ))) |
167 | 131 | oveq1d 7376 |
. . . . . . . 8
β’ (π β (π· limβ (πβπ)) = ((π β β β¦ (π·βπ )) limβ (πβπ))) |
168 | 167 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π· limβ (πβπ)) = ((π β β β¦ (π·βπ )) limβ (πβπ))) |
169 | 166, 168 | eleqtrd 2836 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π·β(πβπ)) β ((π β β β¦ (π·βπ )) limβ (πβπ))) |
170 | 163, 169 | sselid 3946 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π·β(πβπ)) β (((π β β β¦ (π·βπ )) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
171 | 136 | resmptd 5998 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((π β β β¦ (π·βπ )) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ ))) |
172 | 171 | oveq1d 7376 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (((π β β β¦ (π·βπ )) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ )) limβ (πβπ))) |
173 | 170, 172 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π β (0..^π)) β (π·β(πβπ)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ )) limβ (πβπ))) |
174 | 146, 147,
148, 154, 142, 162, 173 | mullimc 43947 |
. . 3
β’ ((π β§ π β (0..^π)) β (π
Β· (π·β(πβπ))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) limβ (πβπ))) |
175 | 27 | reseq1i 5937 |
. . . . 5
β’ (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π β (π΄[,]π΅) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) βΎ ((πβπ)(,)(πβ(π + 1)))) |
176 | 175, 41 | eqtr2id 2786 |
. . . 4
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) = (πΊ βΎ ((πβπ)(,)(πβ(π + 1))))) |
177 | 176 | oveq1d 7376 |
. . 3
β’ ((π β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) limβ (πβπ)) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
178 | 174, 177 | eleqtrd 2836 |
. 2
β’ ((π β§ π β (0..^π)) β (π
Β· (π·β(πβπ))) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
179 | 63, 96 | ltned 11299 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (πβ(π + 1))) |
180 | | fourierdlem84.l |
. . . . . 6
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
181 | 111 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = (π + (πβ(π + 1)))) |
182 | 181 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβ(π + 1))))) |
183 | 180, 182 | eleqtrd 2836 |
. . . . 5
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβ(π + 1))))) |
184 | 86 | recnd 11191 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
185 | 155, 73, 136, 146, 114, 157, 179, 183, 184 | fourierdlem53 44490 |
. . . 4
β’ ((π β§ π β (0..^π)) β πΏ β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβ(π + 1)))) |
186 | | limcresi 25272 |
. . . . . 6
β’ ((π β β β¦ (π·βπ )) limβ (πβ(π + 1))) β (((π β β β¦ (π·βπ )) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) |
187 | 165, 86 | cnlimci 25276 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π·β(πβ(π + 1))) β (π· limβ (πβ(π + 1)))) |
188 | 131 | oveq1d 7376 |
. . . . . . . 8
β’ (π β (π· limβ (πβ(π + 1))) = ((π β β β¦ (π·βπ )) limβ (πβ(π + 1)))) |
189 | 188 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π· limβ (πβ(π + 1))) = ((π β β β¦ (π·βπ )) limβ (πβ(π + 1)))) |
190 | 187, 189 | eleqtrd 2836 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π·β(πβ(π + 1))) β ((π β β β¦ (π·βπ )) limβ (πβ(π + 1)))) |
191 | 186, 190 | sselid 3946 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π·β(πβ(π + 1))) β (((π β β β¦ (π·βπ )) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
192 | 171 | oveq1d 7376 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (((π β β β¦ (π·βπ )) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ )) limβ (πβ(π + 1)))) |
193 | 191, 192 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π β (0..^π)) β (π·β(πβ(π + 1))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π·βπ )) limβ (πβ(π + 1)))) |
194 | 146, 147,
148, 154, 142, 185, 193 | mullimc 43947 |
. . 3
β’ ((π β§ π β (0..^π)) β (πΏ Β· (π·β(πβ(π + 1)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) limβ (πβ(π + 1)))) |
195 | 176 | oveq1d 7376 |
. . 3
β’ ((π β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) limβ (πβ(π + 1))) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
196 | 194, 195 | eleqtrd 2836 |
. 2
β’ ((π β§ π β (0..^π)) β (πΏ Β· (π·β(πβ(π + 1)))) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
197 | 1, 2, 9, 28, 145, 178, 196 | fourierdlem69 44506 |
1
β’ (π β πΊ β
πΏ1) |