Step | Hyp | Ref
| Expression |
1 | | fourierdlem105.p |
. 2
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
2 | | fourierdlem105.t |
. 2
β’ π = (π΅ β π΄) |
3 | | fourierdlem105.m |
. 2
β’ (π β π β β) |
4 | | fourierdlem105.q |
. 2
β’ (π β π β (πβπ)) |
5 | | fourierdlem105.f |
. 2
β’ (π β πΉ:ββΆβ) |
6 | | fourierdlem105.6 |
. 2
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
7 | | fourierdlem105.fcn |
. 2
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
8 | | fourierdlem105.r |
. 2
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
9 | | fourierdlem105.l |
. 2
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
10 | | fourierdlem105.c |
. 2
β’ (π β πΆ β β) |
11 | | fourierdlem105.d |
. 2
β’ (π β π· β (πΆ(,)+β)) |
12 | | eqid 2737 |
. 2
β’ (π β β β¦ {π β (β
βm (0...π))
β£ (((πβ0) =
πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
13 | | eqid 2737 |
. 2
β’
((β―β({πΆ,
π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1) = ((β―β({πΆ, π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1) |
14 | | oveq1 7369 |
. . . . . . 7
β’ (π€ = π¦ β (π€ + (π Β· π)) = (π¦ + (π Β· π))) |
15 | 14 | eleq1d 2823 |
. . . . . 6
β’ (π€ = π¦ β ((π€ + (π Β· π)) β ran π β (π¦ + (π Β· π)) β ran π)) |
16 | 15 | rexbidv 3176 |
. . . . 5
β’ (π€ = π¦ β (βπ β β€ (π€ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· π)) β ran π)) |
17 | | oveq1 7369 |
. . . . . . . 8
β’ (π = π β (π Β· π) = (π Β· π)) |
18 | 17 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (π¦ + (π Β· π)) = (π¦ + (π Β· π))) |
19 | 18 | eleq1d 2823 |
. . . . . 6
β’ (π = π β ((π¦ + (π Β· π)) β ran π β (π¦ + (π Β· π)) β ran π)) |
20 | 19 | cbvrexvw 3229 |
. . . . 5
β’
(βπ β
β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· π)) β ran π) |
21 | 16, 20 | bitrdi 287 |
. . . 4
β’ (π€ = π¦ β (βπ β β€ (π€ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· π)) β ran π)) |
22 | 21 | cbvrabv 3420 |
. . 3
β’ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π} = {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} |
23 | 22 | uneq2i 4125 |
. 2
β’ ({πΆ, π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π}) = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) |
24 | | isoeq1 7267 |
. . 3
β’ (π = π β (π Isom < , <
((0...((β―β({πΆ,
π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({πΆ,
π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})))) |
25 | 24 | cbviotavw 6461 |
. 2
β’
(β©ππ Isom < , <
((0...((β―β({πΆ,
π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π}))) = (β©ππ Isom < , <
((0...((β―β({πΆ,
π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π}))) |
26 | | id 22 |
. . . 4
β’ (π€ = π₯ β π€ = π₯) |
27 | | oveq2 7370 |
. . . . . . 7
β’ (π€ = π₯ β (π΅ β π€) = (π΅ β π₯)) |
28 | 27 | oveq1d 7377 |
. . . . . 6
β’ (π€ = π₯ β ((π΅ β π€) / π) = ((π΅ β π₯) / π)) |
29 | 28 | fveq2d 6851 |
. . . . 5
β’ (π€ = π₯ β (ββ((π΅ β π€) / π)) = (ββ((π΅ β π₯) / π))) |
30 | 29 | oveq1d 7377 |
. . . 4
β’ (π€ = π₯ β ((ββ((π΅ β π€) / π)) Β· π) = ((ββ((π΅ β π₯) / π)) Β· π)) |
31 | 26, 30 | oveq12d 7380 |
. . 3
β’ (π€ = π₯ β (π€ + ((ββ((π΅ β π€) / π)) Β· π)) = (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
32 | 31 | cbvmptv 5223 |
. 2
β’ (π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π))) = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
33 | | eqeq1 2741 |
. . . 4
β’ (π€ = π¦ β (π€ = π΅ β π¦ = π΅)) |
34 | | id 22 |
. . . 4
β’ (π€ = π¦ β π€ = π¦) |
35 | 33, 34 | ifbieq2d 4517 |
. . 3
β’ (π€ = π¦ β if(π€ = π΅, π΄, π€) = if(π¦ = π΅, π΄, π¦)) |
36 | 35 | cbvmptv 5223 |
. 2
β’ (π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€)) = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) |
37 | | fveq2 6847 |
. . . . . . . 8
β’ (π§ = π₯ β ((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§) = ((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)) |
38 | 37 | fveq2d 6851 |
. . . . . . 7
β’ (π§ = π₯ β ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§)) = ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))) |
39 | 38 | breq2d 5122 |
. . . . . 6
β’ (π§ = π₯ β ((πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§)) β (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)))) |
40 | 39 | rabbidv 3418 |
. . . . 5
β’ (π§ = π₯ β {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))} = {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}) |
41 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
42 | 41 | breq1d 5120 |
. . . . . 6
β’ (π = π β ((πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)) β (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)))) |
43 | 42 | cbvrabv 3420 |
. . . . 5
β’ {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))} = {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))} |
44 | 40, 43 | eqtrdi 2793 |
. . . 4
β’ (π§ = π₯ β {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))} = {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}) |
45 | 44 | supeq1d 9389 |
. . 3
β’ (π§ = π₯ β sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))}, β, < ) = sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}, β, < )) |
46 | 45 | cbvmptv 5223 |
. 2
β’ (π§ β β β¦
sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))}, β, < )) = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}, β, < )) |
47 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 23, 25, 32, 36, 46 | fourierdlem100 44521 |
1
β’ (π β (π₯ β (πΆ[,]π·) β¦ (πΉβπ₯)) β
πΏ1) |