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