Step | Hyp | Ref
| Expression |
1 | | fourierdlem108.a |
. 2
β’ (π β π΄ β β) |
2 | | fourierdlem108.b |
. 2
β’ (π β π΅ β β) |
3 | | fourierdlem108.t |
. 2
β’ π = (π΅ β π΄) |
4 | | fourierdlem108.x |
. 2
β’ (π β π β
β+) |
5 | | fourierdlem108.p |
. 2
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
6 | | fourierdlem108.m |
. 2
β’ (π β π β β) |
7 | | fourierdlem108.q |
. 2
β’ (π β π β (πβπ)) |
8 | | fourierdlem108.f |
. 2
β’ (π β πΉ:ββΆβ) |
9 | | fourierdlem108.fper |
. 2
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
10 | | fourierdlem108.fcn |
. 2
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
11 | | fourierdlem108.r |
. 2
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
12 | | fourierdlem108.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 | rgenw 3069 |
. . . . . 6
β’
βπ€ β
((π΄ β π)[,]π΄)(βπ β β€ (π€ + (π Β· π)) β ran π β βπ β β€ (π€ + (π Β· π)) β ran π) |
24 | | rabbi 3435 |
. . . . . 6
β’
(βπ€ β
((π΄ β π)[,]π΄)(βπ β β€ (π€ + (π Β· π)) β ran π β βπ β β€ (π€ + (π Β· π)) β ran π) β {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π} = {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}) |
25 | 23, 24 | mpbi 229 |
. . . . 5
β’ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π} = {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π} |
26 | 25 | uneq2i 4125 |
. . . 4
β’ ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}) = ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}) |
27 | 26 | fveq2i 6850 |
. . 3
β’
(β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) = (β―β({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) |
28 | 27 | oveq1i 7372 |
. 2
β’
((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1) = ((β―β({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1) |
29 | | isoeq5 7271 |
. . . . 5
β’ (({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}) = ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}) β (π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})))) |
30 | 26, 29 | ax-mp 5 |
. . . 4
β’ (π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}))) |
31 | | isoeq1 7267 |
. . . 4
β’ (π = π β (π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})))) |
32 | 30, 31 | bitrid 283 |
. . 3
β’ (π = π β (π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})))) |
33 | 32 | cbviotavw 6461 |
. 2
β’
(β©ππ Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}))) = (β©ππ Isom < , <
((0...((β―β({(π΄
β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π})) β 1)), ({(π΄ β π), π΄} βͺ {π€ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π€ + (π Β· π)) β ran π}))) |
34 | | id 22 |
. . . 4
β’ (π€ = π₯ β π€ = π₯) |
35 | | oveq2 7370 |
. . . . . . 7
β’ (π€ = π₯ β (π΅ β π€) = (π΅ β π₯)) |
36 | 35 | oveq1d 7377 |
. . . . . 6
β’ (π€ = π₯ β ((π΅ β π€) / π) = ((π΅ β π₯) / π)) |
37 | 36 | fveq2d 6851 |
. . . . 5
β’ (π€ = π₯ β (ββ((π΅ β π€) / π)) = (ββ((π΅ β π₯) / π))) |
38 | 37 | oveq1d 7377 |
. . . 4
β’ (π€ = π₯ β ((ββ((π΅ β π€) / π)) Β· π) = ((ββ((π΅ β π₯) / π)) Β· π)) |
39 | 34, 38 | oveq12d 7380 |
. . 3
β’ (π€ = π₯ β (π€ + ((ββ((π΅ β π€) / π)) Β· π)) = (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
40 | 39 | cbvmptv 5223 |
. 2
β’ (π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π))) = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
41 | | eqeq1 2741 |
. . . 4
β’ (π€ = π¦ β (π€ = π΅ β π¦ = π΅)) |
42 | | id 22 |
. . . 4
β’ (π€ = π¦ β π€ = π¦) |
43 | 41, 42 | ifbieq2d 4517 |
. . 3
β’ (π€ = π¦ β if(π€ = π΅, π΄, π€) = if(π¦ = π΅, π΄, π¦)) |
44 | 43 | cbvmptv 5223 |
. 2
β’ (π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€)) = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) |
45 | | fveq2 6847 |
. . . . . . . 8
β’ (π§ = π₯ β ((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§) = ((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)) |
46 | 45 | fveq2d 6851 |
. . . . . . 7
β’ (π§ = π₯ β ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§)) = ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))) |
47 | 46 | breq2d 5122 |
. . . . . 6
β’ (π§ = π₯ β ((πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§)) β (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)))) |
48 | 47 | rabbidv 3418 |
. . . . 5
β’ (π§ = π₯ β {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))} = {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}) |
49 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
50 | 49 | breq1d 5120 |
. . . . . 6
β’ (π = π β ((πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)) β (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯)))) |
51 | 50 | cbvrabv 3420 |
. . . . 5
β’ {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))} = {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))} |
52 | 48, 51 | eqtrdi 2793 |
. . . 4
β’ (π§ = π₯ β {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))} = {π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}) |
53 | 52 | supeq1d 9389 |
. . 3
β’ (π§ = π₯ β sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))}, β, < ) = sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}, β, < )) |
54 | 53 | cbvmptv 5223 |
. 2
β’ (π§ β β β¦
sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ§))}, β, < )) = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π€ β (π΄(,]π΅) β¦ if(π€ = π΅, π΄, π€))β((π€ β β β¦ (π€ + ((ββ((π΅ β π€) / π)) Β· π)))βπ₯))}, β, < )) |
55 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 18, 28, 33, 40, 44, 54 | fourierdlem107 44528 |
1
β’ (π β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |