Step | Hyp | Ref
| Expression |
1 | | prfi 9319 |
. . 3
β’ {ran
π, βͺ ran πΌ} β Fin |
2 | 1 | a1i 11 |
. 2
β’ (π β {ran π, βͺ ran πΌ} β Fin) |
3 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β βͺ {ran
π, βͺ ran πΌ}) β π β βͺ {ran
π, βͺ ran πΌ}) |
4 | | fourierdlem70.q |
. . . . . . . . . . 11
β’ (π β π:(0...π)βΆβ) |
5 | | ovex 7439 |
. . . . . . . . . . 11
β’
(0...π) β
V |
6 | | fex 7225 |
. . . . . . . . . . 11
β’ ((π:(0...π)βΆβ β§ (0...π) β V) β π β V) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . . . . 10
β’ (π β π β V) |
8 | | rnexg 7892 |
. . . . . . . . . 10
β’ (π β V β ran π β V) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
β’ (π β ran π β V) |
10 | | fzofi 13936 |
. . . . . . . . . . . 12
β’
(0..^π) β
Fin |
11 | | fourierdlem70.i |
. . . . . . . . . . . . 13
β’ πΌ = (π β (0..^π) β¦ ((πβπ)(,)(πβ(π + 1)))) |
12 | 11 | rnmptfi 43853 |
. . . . . . . . . . . 12
β’
((0..^π) β Fin
β ran πΌ β
Fin) |
13 | 10, 12 | ax-mp 5 |
. . . . . . . . . . 11
β’ ran πΌ β Fin |
14 | 13 | elexi 3494 |
. . . . . . . . . 10
β’ ran πΌ β V |
15 | 14 | uniex 7728 |
. . . . . . . . 9
β’ βͺ ran πΌ β V |
16 | | uniprg 4925 |
. . . . . . . . 9
β’ ((ran
π β V β§ βͺ ran πΌ β V) β βͺ {ran π, βͺ ran πΌ} = (ran π βͺ βͺ ran
πΌ)) |
17 | 9, 15, 16 | sylancl 587 |
. . . . . . . 8
β’ (π β βͺ {ran π, βͺ ran πΌ} = (ran π βͺ βͺ ran
πΌ)) |
18 | 17 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β βͺ {ran
π, βͺ ran πΌ}) β βͺ {ran
π, βͺ ran πΌ} = (ran π βͺ βͺ ran
πΌ)) |
19 | 3, 18 | eleqtrd 2836 |
. . . . . 6
β’ ((π β§ π β βͺ {ran
π, βͺ ran πΌ}) β π β (ran π βͺ βͺ ran
πΌ)) |
20 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π¦ β β β¦ {π£ β (β
βm (0...π¦))
β£ (((π£β0) =
π΄ β§ (π£βπ¦) = π΅) β§ βπ β (0..^π¦)(π£βπ) < (π£β(π + 1)))}) = (π¦ β β β¦ {π£ β (β βm
(0...π¦)) β£ (((π£β0) = π΄ β§ (π£βπ¦) = π΅) β§ βπ β (0..^π¦)(π£βπ) < (π£β(π + 1)))}) |
21 | | fourierdlem70.m |
. . . . . . . . . . 11
β’ (π β π β β) |
22 | | reex 11198 |
. . . . . . . . . . . . . . 15
β’ β
β V |
23 | 22, 5 | elmap 8862 |
. . . . . . . . . . . . . 14
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
24 | 4, 23 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π β π β (β βm
(0...π))) |
25 | | fourierdlem70.q0 |
. . . . . . . . . . . . . 14
β’ (π β (πβ0) = π΄) |
26 | | fourierdlem70.qm |
. . . . . . . . . . . . . 14
β’ (π β (πβπ) = π΅) |
27 | 25, 26 | jca 513 |
. . . . . . . . . . . . 13
β’ (π β ((πβ0) = π΄ β§ (πβπ) = π΅)) |
28 | | fourierdlem70.qlt |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
29 | 28 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
30 | 24, 27, 29 | jca32 517 |
. . . . . . . . . . . 12
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
31 | 20 | fourierdlem2 44812 |
. . . . . . . . . . . . 13
β’ (π β β β (π β ((π¦ β β β¦ {π£ β (β βm
(0...π¦)) β£ (((π£β0) = π΄ β§ (π£βπ¦) = π΅) β§ βπ β (0..^π¦)(π£βπ) < (π£β(π + 1)))})βπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
32 | 21, 31 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β ((π¦ β β β¦ {π£ β (β βm
(0...π¦)) β£ (((π£β0) = π΄ β§ (π£βπ¦) = π΅) β§ βπ β (0..^π¦)(π£βπ) < (π£β(π + 1)))})βπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
33 | 30, 32 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β π β ((π¦ β β β¦ {π£ β (β βm
(0...π¦)) β£ (((π£β0) = π΄ β§ (π£βπ¦) = π΅) β§ βπ β (0..^π¦)(π£βπ) < (π£β(π + 1)))})βπ)) |
34 | 20, 21, 33 | fourierdlem15 44825 |
. . . . . . . . . 10
β’ (π β π:(0...π)βΆ(π΄[,]π΅)) |
35 | 34 | frnd 6723 |
. . . . . . . . 9
β’ (π β ran π β (π΄[,]π΅)) |
36 | 35 | sselda 3982 |
. . . . . . . 8
β’ ((π β§ π β ran π) β π β (π΄[,]π΅)) |
37 | 36 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β (ran π βͺ βͺ ran
πΌ)) β§ π β ran π) β π β (π΄[,]π΅)) |
38 | | simpll 766 |
. . . . . . . 8
β’ (((π β§ π β (ran π βͺ βͺ ran
πΌ)) β§ Β¬ π β ran π) β π) |
39 | | elunnel1 4149 |
. . . . . . . . 9
β’ ((π β (ran π βͺ βͺ ran
πΌ) β§ Β¬ π β ran π) β π β βͺ ran
πΌ) |
40 | 39 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π β (ran π βͺ βͺ ran
πΌ)) β§ Β¬ π β ran π) β π β βͺ ran
πΌ) |
41 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ ran
πΌ) β π β βͺ ran πΌ) |
42 | 11 | funmpt2 6585 |
. . . . . . . . . . 11
β’ Fun πΌ |
43 | | elunirn 7247 |
. . . . . . . . . . 11
β’ (Fun
πΌ β (π β βͺ ran πΌ β βπ β dom πΌ π β (πΌβπ))) |
44 | 42, 43 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ ran
πΌ) β (π β βͺ ran πΌ β βπ β dom πΌ π β (πΌβπ))) |
45 | 41, 44 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β βͺ ran
πΌ) β βπ β dom πΌ π β (πΌβπ)) |
46 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom πΌ β π β dom πΌ) |
47 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ)(,)(πβ(π + 1))) β V |
48 | 47, 11 | dmmpti 6692 |
. . . . . . . . . . . . . . . . . 18
β’ dom πΌ = (0..^π) |
49 | 46, 48 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom πΌ β π β (0..^π)) |
50 | 11 | fvmpt2 7007 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0..^π) β§ ((πβπ)(,)(πβ(π + 1))) β V) β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
51 | 49, 47, 50 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π β dom πΌ β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
52 | 51 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β dom πΌ) β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
53 | | ioossicc 13407 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
54 | | fourierdlem70.a |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β β) |
55 | 54 | rexrd 11261 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β
β*) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom πΌ) β π΄ β
β*) |
57 | | fourierdlem70.2 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β β) |
58 | 57 | rexrd 11261 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β
β*) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom πΌ) β π΅ β
β*) |
60 | 34 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom πΌ) β π:(0...π)βΆ(π΄[,]π΅)) |
61 | 49 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom πΌ) β π β (0..^π)) |
62 | 56, 59, 60, 61 | fourierdlem8 44818 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β dom πΌ) β ((πβπ)[,](πβ(π + 1))) β (π΄[,]π΅)) |
63 | 53, 62 | sstrid 3993 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β dom πΌ) β ((πβπ)(,)(πβ(π + 1))) β (π΄[,]π΅)) |
64 | 52, 63 | eqsstrd 4020 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom πΌ) β (πΌβπ) β (π΄[,]π΅)) |
65 | 64 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β dom πΌ β§ π β (πΌβπ)) β (πΌβπ) β (π΄[,]π΅)) |
66 | | simp3 1139 |
. . . . . . . . . . . . 13
β’ ((π β§ π β dom πΌ β§ π β (πΌβπ)) β π β (πΌβπ)) |
67 | 65, 66 | sseldd 3983 |
. . . . . . . . . . . 12
β’ ((π β§ π β dom πΌ β§ π β (πΌβπ)) β π β (π΄[,]π΅)) |
68 | 67 | 3exp 1120 |
. . . . . . . . . . 11
β’ (π β (π β dom πΌ β (π β (πΌβπ) β π β (π΄[,]π΅)))) |
69 | 68 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ ran
πΌ) β (π β dom πΌ β (π β (πΌβπ) β π β (π΄[,]π΅)))) |
70 | 69 | rexlimdv 3154 |
. . . . . . . . 9
β’ ((π β§ π β βͺ ran
πΌ) β (βπ β dom πΌ π β (πΌβπ) β π β (π΄[,]π΅))) |
71 | 45, 70 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π β βͺ ran
πΌ) β π β (π΄[,]π΅)) |
72 | 38, 40, 71 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β (ran π βͺ βͺ ran
πΌ)) β§ Β¬ π β ran π) β π β (π΄[,]π΅)) |
73 | 37, 72 | pm2.61dan 812 |
. . . . . 6
β’ ((π β§ π β (ran π βͺ βͺ ran
πΌ)) β π β (π΄[,]π΅)) |
74 | 19, 73 | syldan 592 |
. . . . 5
β’ ((π β§ π β βͺ {ran
π, βͺ ran πΌ}) β π β (π΄[,]π΅)) |
75 | | fourierdlem70.f |
. . . . . 6
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
76 | 75 | ffvelcdmda 7084 |
. . . . 5
β’ ((π β§ π β (π΄[,]π΅)) β (πΉβπ ) β β) |
77 | 74, 76 | syldan 592 |
. . . 4
β’ ((π β§ π β βͺ {ran
π, βͺ ran πΌ}) β (πΉβπ ) β β) |
78 | 77 | recnd 11239 |
. . 3
β’ ((π β§ π β βͺ {ran
π, βͺ ran πΌ}) β (πΉβπ ) β β) |
79 | 78 | abscld 15380 |
. 2
β’ ((π β§ π β βͺ {ran
π, βͺ ran πΌ}) β (absβ(πΉβπ )) β β) |
80 | | simpr 486 |
. . . . . 6
β’ ((π β§ π€ = ran π) β π€ = ran π) |
81 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π€ = ran π) β π:(0...π)βΆβ) |
82 | | fzfid 13935 |
. . . . . . 7
β’ ((π β§ π€ = ran π) β (0...π) β Fin) |
83 | | rnffi 43857 |
. . . . . . 7
β’ ((π:(0...π)βΆβ β§ (0...π) β Fin) β ran π β Fin) |
84 | 81, 82, 83 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π€ = ran π) β ran π β Fin) |
85 | 80, 84 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π€ = ran π) β π€ β Fin) |
86 | 85 | adantlr 714 |
. . . 4
β’ (((π β§ π€ β {ran π, βͺ ran πΌ}) β§ π€ = ran π) β π€ β Fin) |
87 | 75 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π€ = ran π) β§ π β π€) β πΉ:(π΄[,]π΅)βΆβ) |
88 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ π€ = ran π) β§ π β π€) β π) |
89 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π€ = ran π β§ π β π€) β π β π€) |
90 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π€ = ran π β§ π β π€) β π€ = ran π) |
91 | 89, 90 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π€ = ran π β§ π β π€) β π β ran π) |
92 | 91 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π€ = ran π) β§ π β π€) β π β ran π) |
93 | 88, 92, 36 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π€ = ran π) β§ π β π€) β π β (π΄[,]π΅)) |
94 | 87, 93 | ffvelcdmd 7085 |
. . . . . . . 8
β’ (((π β§ π€ = ran π) β§ π β π€) β (πΉβπ ) β β) |
95 | 94 | recnd 11239 |
. . . . . . 7
β’ (((π β§ π€ = ran π) β§ π β π€) β (πΉβπ ) β β) |
96 | 95 | abscld 15380 |
. . . . . 6
β’ (((π β§ π€ = ran π) β§ π β π€) β (absβ(πΉβπ )) β β) |
97 | 96 | ralrimiva 3147 |
. . . . 5
β’ ((π β§ π€ = ran π) β βπ β π€ (absβ(πΉβπ )) β β) |
98 | 97 | adantlr 714 |
. . . 4
β’ (((π β§ π€ β {ran π, βͺ ran πΌ}) β§ π€ = ran π) β βπ β π€ (absβ(πΉβπ )) β β) |
99 | | fimaxre3 12157 |
. . . 4
β’ ((π€ β Fin β§ βπ β π€ (absβ(πΉβπ )) β β) β βπ§ β β βπ β π€ (absβ(πΉβπ )) β€ π§) |
100 | 86, 98, 99 | syl2anc 585 |
. . 3
β’ (((π β§ π€ β {ran π, βͺ ran πΌ}) β§ π€ = ran π) β βπ§ β β βπ β π€ (absβ(πΉβπ )) β€ π§) |
101 | | simpll 766 |
. . . 4
β’ (((π β§ π€ β {ran π, βͺ ran πΌ}) β§ Β¬ π€ = ran π) β π) |
102 | | neqne 2949 |
. . . . . 6
β’ (Β¬
π€ = ran π β π€ β ran π) |
103 | | elprn1 44336 |
. . . . . 6
β’ ((π€ β {ran π, βͺ ran πΌ} β§ π€ β ran π) β π€ = βͺ ran πΌ) |
104 | 102, 103 | sylan2 594 |
. . . . 5
β’ ((π€ β {ran π, βͺ ran πΌ} β§ Β¬ π€ = ran π) β π€ = βͺ ran πΌ) |
105 | 104 | adantll 713 |
. . . 4
β’ (((π β§ π€ β {ran π, βͺ ran πΌ}) β§ Β¬ π€ = ran π) β π€ = βͺ ran πΌ) |
106 | 10, 12 | mp1i 13 |
. . . . 5
β’ ((π β§ π€ = βͺ ran πΌ) β ran πΌ β Fin) |
107 | | ax-resscn 11164 |
. . . . . . . . . 10
β’ β
β β |
108 | 107 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
β) |
109 | 75, 108 | fssd 6733 |
. . . . . . . 8
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
110 | 109 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π€ = βͺ ran πΌ) β§ π β βͺ ran
πΌ) β πΉ:(π΄[,]π΅)βΆβ) |
111 | 71 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π€ = βͺ ran πΌ) β§ π β βͺ ran
πΌ) β π β (π΄[,]π΅)) |
112 | 110, 111 | ffvelcdmd 7085 |
. . . . . 6
β’ (((π β§ π€ = βͺ ran πΌ) β§ π β βͺ ran
πΌ) β (πΉβπ ) β β) |
113 | 112 | abscld 15380 |
. . . . 5
β’ (((π β§ π€ = βͺ ran πΌ) β§ π β βͺ ran
πΌ) β (absβ(πΉβπ )) β β) |
114 | 47, 11 | fnmpti 6691 |
. . . . . . . . . 10
β’ πΌ Fn (0..^π) |
115 | | fvelrnb 6950 |
. . . . . . . . . 10
β’ (πΌ Fn (0..^π) β (π‘ β ran πΌ β βπ β (0..^π)(πΌβπ) = π‘)) |
116 | 114, 115 | ax-mp 5 |
. . . . . . . . 9
β’ (π‘ β ran πΌ β βπ β (0..^π)(πΌβπ) = π‘) |
117 | 116 | biimpi 215 |
. . . . . . . 8
β’ (π‘ β ran πΌ β βπ β (0..^π)(πΌβπ) = π‘) |
118 | 117 | adantl 483 |
. . . . . . 7
β’ ((π β§ π‘ β ran πΌ) β βπ β (0..^π)(πΌβπ) = π‘) |
119 | 4 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
120 | | elfzofz 13645 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β π β (0...π)) |
121 | 120 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
122 | 119, 121 | ffvelcdmd 7085 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
123 | | fzofzp1 13726 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β (π + 1) β (0...π)) |
124 | 123 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
125 | 119, 124 | ffvelcdmd 7085 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
126 | | fourierdlem70.fcn |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
127 | | fourierdlem70.l |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
128 | | fourierdlem70.r |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
129 | 122, 125,
126, 127, 128 | cncfioobd 44600 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β βπ β β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ )) β€ π) |
130 | | fvres 6908 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((πβπ)(,)(πβ(π + 1))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ ) = (πΉβπ )) |
131 | 130 | fveq2d 6893 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ )) = (absβ(πΉβπ ))) |
132 | 131 | breq1d 5158 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πβπ)(,)(πβ(π + 1))) β ((absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ )) β€ π β (absβ(πΉβπ )) β€ π)) |
133 | 132 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ )) β€ π β (absβ(πΉβπ )) β€ π)) |
134 | 133 | ralbidva 3176 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (βπ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ )) β€ π β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ )) β€ π)) |
135 | 134 | rexbidv 3179 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (βπ β β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ )) β€ π β βπ β β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ )) β€ π)) |
136 | 129, 135 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β βπ β β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ )) β€ π) |
137 | 136 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β βπ β β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ )) β€ π) |
138 | 47, 50 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
139 | 138 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β ((πβπ)(,)(πβ(π + 1))) = (πΌβπ)) |
140 | 139 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β (0..^π) β§ (πΌβπ) = π‘) β ((πβπ)(,)(πβ(π + 1))) = (πΌβπ)) |
141 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β (0..^π) β§ (πΌβπ) = π‘) β (πΌβπ) = π‘) |
142 | 140, 141 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π β (0..^π) β§ (πΌβπ) = π‘) β ((πβπ)(,)(πβ(π + 1))) = π‘) |
143 | 142 | raleqdv 3326 |
. . . . . . . . . . . . 13
β’ ((π β (0..^π) β§ (πΌβπ) = π‘) β (βπ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ )) β€ π β βπ β π‘ (absβ(πΉβπ )) β€ π)) |
144 | 143 | rexbidv 3179 |
. . . . . . . . . . . 12
β’ ((π β (0..^π) β§ (πΌβπ) = π‘) β (βπ β β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ )) β€ π β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π)) |
145 | 144 | 3adant1 1131 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β (βπ β β βπ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ )) β€ π β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π)) |
146 | 137, 145 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π) |
147 | 146 | 3exp 1120 |
. . . . . . . . 9
β’ (π β (π β (0..^π) β ((πΌβπ) = π‘ β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π))) |
148 | 147 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β ran πΌ) β (π β (0..^π) β ((πΌβπ) = π‘ β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π))) |
149 | 148 | rexlimdv 3154 |
. . . . . . 7
β’ ((π β§ π‘ β ran πΌ) β (βπ β (0..^π)(πΌβπ) = π‘ β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π)) |
150 | 118, 149 | mpd 15 |
. . . . . 6
β’ ((π β§ π‘ β ran πΌ) β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π) |
151 | 150 | adantlr 714 |
. . . . 5
β’ (((π β§ π€ = βͺ ran πΌ) β§ π‘ β ran πΌ) β βπ β β βπ β π‘ (absβ(πΉβπ )) β€ π) |
152 | | eqimss 4040 |
. . . . . 6
β’ (π€ = βͺ
ran πΌ β π€ β βͺ ran πΌ) |
153 | 152 | adantl 483 |
. . . . 5
β’ ((π β§ π€ = βͺ ran πΌ) β π€ β βͺ ran
πΌ) |
154 | 106, 113,
151, 153 | ssfiunibd 44006 |
. . . 4
β’ ((π β§ π€ = βͺ ran πΌ) β βπ§ β β βπ β π€ (absβ(πΉβπ )) β€ π§) |
155 | 101, 105,
154 | syl2anc 585 |
. . 3
β’ (((π β§ π€ β {ran π, βͺ ran πΌ}) β§ Β¬ π€ = ran π) β βπ§ β β βπ β π€ (absβ(πΉβπ )) β€ π§) |
156 | 100, 155 | pm2.61dan 812 |
. 2
β’ ((π β§ π€ β {ran π, βͺ ran πΌ}) β βπ§ β β βπ β π€ (absβ(πΉβπ )) β€ π§) |
157 | 21 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β π β β) |
158 | 4 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β π:(0...π)βΆβ) |
159 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β (π΄[,]π΅)) β π‘ β (π΄[,]π΅)) |
160 | 25 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ = (πβ0)) |
161 | 26 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ = (πβπ)) |
162 | 160, 161 | oveq12d 7424 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄[,]π΅) = ((πβ0)[,](πβπ))) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β (π΄[,]π΅)) β (π΄[,]π΅) = ((πβ0)[,](πβπ))) |
164 | 159, 163 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β (π΄[,]π΅)) β π‘ β ((πβ0)[,](πβπ))) |
165 | 164 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β π‘ β ((πβ0)[,](πβπ))) |
166 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β Β¬ π‘ β ran π) |
167 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
168 | 167 | breq1d 5158 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ) < π‘ β (πβπ) < π‘)) |
169 | 168 | cbvrabv 3443 |
. . . . . . . . . . . . 13
β’ {π β (0..^π) β£ (πβπ) < π‘} = {π β (0..^π) β£ (πβπ) < π‘} |
170 | 169 | supeq1i 9439 |
. . . . . . . . . . . 12
β’
sup({π β
(0..^π) β£ (πβπ) < π‘}, β, < ) = sup({π β (0..^π) β£ (πβπ) < π‘}, β, < ) |
171 | 157, 158,
165, 166, 170 | fourierdlem25 44835 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β βπ β (0..^π)π‘ β ((πβπ)(,)(πβ(π + 1)))) |
172 | 138 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π β (0..^π) β (π‘ β (πΌβπ) β π‘ β ((πβπ)(,)(πβ(π + 1))))) |
173 | 172 | rexbiia 3093 |
. . . . . . . . . . 11
β’
(βπ β
(0..^π)π‘ β (πΌβπ) β βπ β (0..^π)π‘ β ((πβπ)(,)(πβ(π + 1)))) |
174 | 171, 173 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β βπ β (0..^π)π‘ β (πΌβπ)) |
175 | 48 | eqcomi 2742 |
. . . . . . . . . . 11
β’
(0..^π) = dom πΌ |
176 | 175 | rexeqi 3325 |
. . . . . . . . . 10
β’
(βπ β
(0..^π)π‘ β (πΌβπ) β βπ β dom πΌ π‘ β (πΌβπ)) |
177 | 174, 176 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β βπ β dom πΌ π‘ β (πΌβπ)) |
178 | | elunirn 7247 |
. . . . . . . . . 10
β’ (Fun
πΌ β (π‘ β βͺ ran πΌ β βπ β dom πΌ π‘ β (πΌβπ))) |
179 | 42, 178 | mp1i 13 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β (π‘ β βͺ ran
πΌ β βπ β dom πΌ π‘ β (πΌβπ))) |
180 | 177, 179 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ π‘ β (π΄[,]π΅)) β§ Β¬ π‘ β ran π) β π‘ β βͺ ran
πΌ) |
181 | 180 | ex 414 |
. . . . . . 7
β’ ((π β§ π‘ β (π΄[,]π΅)) β (Β¬ π‘ β ran π β π‘ β βͺ ran
πΌ)) |
182 | 181 | orrd 862 |
. . . . . 6
β’ ((π β§ π‘ β (π΄[,]π΅)) β (π‘ β ran π β¨ π‘ β βͺ ran
πΌ)) |
183 | | elun 4148 |
. . . . . 6
β’ (π‘ β (ran π βͺ βͺ ran
πΌ) β (π‘ β ran π β¨ π‘ β βͺ ran
πΌ)) |
184 | 182, 183 | sylibr 233 |
. . . . 5
β’ ((π β§ π‘ β (π΄[,]π΅)) β π‘ β (ran π βͺ βͺ ran
πΌ)) |
185 | 184 | ralrimiva 3147 |
. . . 4
β’ (π β βπ‘ β (π΄[,]π΅)π‘ β (ran π βͺ βͺ ran
πΌ)) |
186 | | dfss3 3970 |
. . . 4
β’ ((π΄[,]π΅) β (ran π βͺ βͺ ran
πΌ) β βπ‘ β (π΄[,]π΅)π‘ β (ran π βͺ βͺ ran
πΌ)) |
187 | 185, 186 | sylibr 233 |
. . 3
β’ (π β (π΄[,]π΅) β (ran π βͺ βͺ ran
πΌ)) |
188 | 187, 17 | sseqtrrd 4023 |
. 2
β’ (π β (π΄[,]π΅) β βͺ {ran
π, βͺ ran πΌ}) |
189 | 2, 79, 156, 188 | ssfiunibd 44006 |
1
β’ (π β βπ₯ β β βπ β (π΄[,]π΅)(absβ(πΉβπ )) β€ π₯) |