Step | Hyp | Ref
| Expression |
1 | | prfi 9319 |
. . . 4
β’ {(ran
π β© dom πΉ), βͺ
ran πΌ} β
Fin |
2 | 1 | a1i 11 |
. . 3
β’ (π β {(ran π β© dom πΉ), βͺ ran πΌ} β Fin) |
3 | | fourierdlem71.f |
. . . . . . 7
β’ (π β πΉ:dom πΉβΆβ) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β πΉ:dom πΉβΆβ) |
5 | | simpl 484 |
. . . . . . 7
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β π) |
6 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β π₯ β βͺ {(ran π β© dom πΉ), βͺ ran πΌ}) |
7 | | fourierdlem71.q |
. . . . . . . . . . . 12
β’ (π β π:(0...π)βΆβ) |
8 | | ovex 7439 |
. . . . . . . . . . . . 13
β’
(0...π) β
V |
9 | 8 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (0...π) β V) |
10 | 7, 9 | fexd 7226 |
. . . . . . . . . . 11
β’ (π β π β V) |
11 | | rnexg 7892 |
. . . . . . . . . . 11
β’ (π β V β ran π β V) |
12 | | inex1g 5319 |
. . . . . . . . . . 11
β’ (ran
π β V β (ran
π β© dom πΉ) β V) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . 10
β’ (π β (ran π β© dom πΉ) β V) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β (ran π β© dom πΉ) β V) |
15 | | fourierdlem71.i |
. . . . . . . . . . . . . 14
β’ πΌ = (π β (0..^π) β¦ ((πβπ)(,)(πβ(π + 1)))) |
16 | | ovex 7439 |
. . . . . . . . . . . . . . 15
β’
(0..^π) β
V |
17 | 16 | mptex 7222 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β¦ ((πβπ)(,)(πβ(π + 1)))) β V |
18 | 15, 17 | eqeltri 2830 |
. . . . . . . . . . . . 13
β’ πΌ β V |
19 | 18 | rnex 7900 |
. . . . . . . . . . . 12
β’ ran πΌ β V |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
β’ (π β ran πΌ β V) |
21 | 20 | uniexd 7729 |
. . . . . . . . . 10
β’ (π β βͺ ran πΌ β V) |
22 | 21 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β βͺ ran πΌ β V) |
23 | | uniprg 4925 |
. . . . . . . . 9
β’ (((ran
π β© dom πΉ) β V β§ βͺ ran πΌ β V) β βͺ {(ran π β© dom πΉ), βͺ ran πΌ} = ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
24 | 14, 22, 23 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β βͺ {(ran π β© dom πΉ), βͺ ran πΌ} = ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
25 | 6, 24 | eleqtrd 2836 |
. . . . . . 7
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
26 | | elinel2 4196 |
. . . . . . . . 9
β’ (π₯ β (ran π β© dom πΉ) β π₯ β dom πΉ) |
27 | 26 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) β§ π₯ β (ran π β© dom πΉ)) β π₯ β dom πΉ) |
28 | | simpll 766 |
. . . . . . . . 9
β’ (((π β§ π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) β§ Β¬ π₯ β (ran π β© dom πΉ)) β π) |
29 | | elunnel1 4149 |
. . . . . . . . . 10
β’ ((π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ) β§ Β¬ π₯ β (ran π β© dom πΉ)) β π₯ β βͺ ran
πΌ) |
30 | 29 | adantll 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) β§ Β¬ π₯ β (ran π β© dom πΉ)) β π₯ β βͺ ran
πΌ) |
31 | 15 | funmpt2 6585 |
. . . . . . . . . . . . 13
β’ Fun πΌ |
32 | | elunirn 7247 |
. . . . . . . . . . . . 13
β’ (Fun
πΌ β (π₯ β βͺ ran πΌ β βπ β dom πΌ π₯ β (πΌβπ))) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (π₯ β βͺ ran πΌ β βπ β dom πΌ π₯ β (πΌβπ)) |
34 | 33 | biimpi 215 |
. . . . . . . . . . 11
β’ (π₯ β βͺ ran πΌ β βπ β dom πΌ π₯ β (πΌβπ)) |
35 | 34 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β βͺ ran
πΌ) β βπ β dom πΌ π₯ β (πΌβπ)) |
36 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom πΌ β π β dom πΌ) |
37 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβπ)(,)(πβ(π + 1))) β V |
38 | 37, 15 | dmmpti 6692 |
. . . . . . . . . . . . . . . . . . 19
β’ dom πΌ = (0..^π) |
39 | 36, 38 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom πΌ β π β (0..^π)) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom πΌ) β π β (0..^π)) |
41 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom πΌ) β ((πβπ)(,)(πβ(π + 1))) β V) |
42 | 15 | fvmpt2 7007 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0..^π) β§ ((πβπ)(,)(πβ(π + 1))) β V) β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
43 | 40, 41, 42 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β dom πΌ) β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
44 | | fourierdlem71.fcn |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
45 | | cncff 24401 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
46 | | fdm 6724 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
47 | 44, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
48 | 39, 47 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom πΌ) β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
49 | | ssdmres 6003 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ)(,)(πβ(π + 1))) β dom πΉ β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
50 | 48, 49 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β dom πΌ) β ((πβπ)(,)(πβ(π + 1))) β dom πΉ) |
51 | 43, 50 | eqsstrd 4020 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β dom πΌ) β (πΌβπ) β dom πΉ) |
52 | 51 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom πΌ β§ π₯ β (πΌβπ)) β (πΌβπ) β dom πΉ) |
53 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom πΌ β§ π₯ β (πΌβπ)) β π₯ β (πΌβπ)) |
54 | 52, 53 | sseldd 3983 |
. . . . . . . . . . . . 13
β’ ((π β§ π β dom πΌ β§ π₯ β (πΌβπ)) β π₯ β dom πΉ) |
55 | 54 | 3exp 1120 |
. . . . . . . . . . . 12
β’ (π β (π β dom πΌ β (π₯ β (πΌβπ) β π₯ β dom πΉ))) |
56 | 55 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β βͺ ran
πΌ) β (π β dom πΌ β (π₯ β (πΌβπ) β π₯ β dom πΉ))) |
57 | 56 | rexlimdv 3154 |
. . . . . . . . . 10
β’ ((π β§ π₯ β βͺ ran
πΌ) β (βπ β dom πΌ π₯ β (πΌβπ) β π₯ β dom πΉ)) |
58 | 35, 57 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π₯ β βͺ ran
πΌ) β π₯ β dom πΉ) |
59 | 28, 30, 58 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) β§ Β¬ π₯ β (ran π β© dom πΉ)) β π₯ β dom πΉ) |
60 | 27, 59 | pm2.61dan 812 |
. . . . . . 7
β’ ((π β§ π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) β π₯ β dom πΉ) |
61 | 5, 25, 60 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β π₯ β dom πΉ) |
62 | 4, 61 | ffvelcdmd 7085 |
. . . . 5
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β (πΉβπ₯) β β) |
63 | 62 | recnd 11239 |
. . . 4
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β (πΉβπ₯) β β) |
64 | 63 | abscld 15380 |
. . 3
β’ ((π β§ π₯ β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) β
(absβ(πΉβπ₯)) β
β) |
65 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π€ = (ran π β© dom πΉ)) β π€ = (ran π β© dom πΉ)) |
66 | | fzfid 13935 |
. . . . . . . . . 10
β’ (π β (0...π) β Fin) |
67 | | rnffi 43857 |
. . . . . . . . . 10
β’ ((π:(0...π)βΆβ β§ (0...π) β Fin) β ran π β Fin) |
68 | 7, 66, 67 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ran π β Fin) |
69 | | infi 9265 |
. . . . . . . . 9
β’ (ran
π β Fin β (ran
π β© dom πΉ) β Fin) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
β’ (π β (ran π β© dom πΉ) β Fin) |
71 | 70 | adantr 482 |
. . . . . . 7
β’ ((π β§ π€ = (ran π β© dom πΉ)) β (ran π β© dom πΉ) β Fin) |
72 | 65, 71 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π€ = (ran π β© dom πΉ)) β π€ β Fin) |
73 | | simpll 766 |
. . . . . . . 8
β’ (((π β§ π€ = (ran π β© dom πΉ)) β§ π₯ β π€) β π) |
74 | | simpr 486 |
. . . . . . . . . 10
β’ ((π€ = (ran π β© dom πΉ) β§ π₯ β π€) β π₯ β π€) |
75 | | simpl 484 |
. . . . . . . . . 10
β’ ((π€ = (ran π β© dom πΉ) β§ π₯ β π€) β π€ = (ran π β© dom πΉ)) |
76 | 74, 75 | eleqtrd 2836 |
. . . . . . . . 9
β’ ((π€ = (ran π β© dom πΉ) β§ π₯ β π€) β π₯ β (ran π β© dom πΉ)) |
77 | 76 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π€ = (ran π β© dom πΉ)) β§ π₯ β π€) β π₯ β (ran π β© dom πΉ)) |
78 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (ran π β© dom πΉ)) β πΉ:dom πΉβΆβ) |
79 | 26 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (ran π β© dom πΉ)) β π₯ β dom πΉ) |
80 | 78, 79 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (ran π β© dom πΉ)) β (πΉβπ₯) β β) |
81 | 80 | recnd 11239 |
. . . . . . . . 9
β’ ((π β§ π₯ β (ran π β© dom πΉ)) β (πΉβπ₯) β β) |
82 | 81 | abscld 15380 |
. . . . . . . 8
β’ ((π β§ π₯ β (ran π β© dom πΉ)) β (absβ(πΉβπ₯)) β β) |
83 | 73, 77, 82 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π€ = (ran π β© dom πΉ)) β§ π₯ β π€) β (absβ(πΉβπ₯)) β β) |
84 | 83 | ralrimiva 3147 |
. . . . . 6
β’ ((π β§ π€ = (ran π β© dom πΉ)) β βπ₯ β π€ (absβ(πΉβπ₯)) β β) |
85 | | fimaxre3 12157 |
. . . . . 6
β’ ((π€ β Fin β§ βπ₯ β π€ (absβ(πΉβπ₯)) β β) β βπ¦ β β βπ₯ β π€ (absβ(πΉβπ₯)) β€ π¦) |
86 | 72, 84, 85 | syl2anc 585 |
. . . . 5
β’ ((π β§ π€ = (ran π β© dom πΉ)) β βπ¦ β β βπ₯ β π€ (absβ(πΉβπ₯)) β€ π¦) |
87 | 86 | adantlr 714 |
. . . 4
β’ (((π β§ π€ β {(ran π β© dom πΉ), βͺ ran πΌ}) β§ π€ = (ran π β© dom πΉ)) β βπ¦ β β βπ₯ β π€ (absβ(πΉβπ₯)) β€ π¦) |
88 | | simpll 766 |
. . . . 5
β’ (((π β§ π€ β {(ran π β© dom πΉ), βͺ ran πΌ}) β§ Β¬ π€ = (ran π β© dom πΉ)) β π) |
89 | | neqne 2949 |
. . . . . . 7
β’ (Β¬
π€ = (ran π β© dom πΉ) β π€ β (ran π β© dom πΉ)) |
90 | | elprn1 44336 |
. . . . . . 7
β’ ((π€ β {(ran π β© dom πΉ), βͺ ran πΌ} β§ π€ β (ran π β© dom πΉ)) β π€ = βͺ ran πΌ) |
91 | 89, 90 | sylan2 594 |
. . . . . 6
β’ ((π€ β {(ran π β© dom πΉ), βͺ ran πΌ} β§ Β¬ π€ = (ran π β© dom πΉ)) β π€ = βͺ ran πΌ) |
92 | 91 | adantll 713 |
. . . . 5
β’ (((π β§ π€ β {(ran π β© dom πΉ), βͺ ran πΌ}) β§ Β¬ π€ = (ran π β© dom πΉ)) β π€ = βͺ ran πΌ) |
93 | | fzofi 13936 |
. . . . . . . 8
β’
(0..^π) β
Fin |
94 | 15 | rnmptfi 43853 |
. . . . . . . 8
β’
((0..^π) β Fin
β ran πΌ β
Fin) |
95 | 93, 94 | ax-mp 5 |
. . . . . . 7
β’ ran πΌ β Fin |
96 | 95 | a1i 11 |
. . . . . 6
β’ ((π β§ π€ = βͺ ran πΌ) β ran πΌ β Fin) |
97 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β βͺ ran
πΌ) β πΉ:dom πΉβΆβ) |
98 | 97, 58 | ffvelcdmd 7085 |
. . . . . . . . 9
β’ ((π β§ π₯ β βͺ ran
πΌ) β (πΉβπ₯) β β) |
99 | 98 | recnd 11239 |
. . . . . . . 8
β’ ((π β§ π₯ β βͺ ran
πΌ) β (πΉβπ₯) β β) |
100 | 99 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π€ = βͺ ran πΌ) β§ π₯ β βͺ ran
πΌ) β (πΉβπ₯) β β) |
101 | 100 | abscld 15380 |
. . . . . 6
β’ (((π β§ π€ = βͺ ran πΌ) β§ π₯ β βͺ ran
πΌ) β (absβ(πΉβπ₯)) β β) |
102 | 37, 15 | fnmpti 6691 |
. . . . . . . . . . 11
β’ πΌ Fn (0..^π) |
103 | | fvelrnb 6950 |
. . . . . . . . . . 11
β’ (πΌ Fn (0..^π) β (π‘ β ran πΌ β βπ β (0..^π)(πΌβπ) = π‘)) |
104 | 102, 103 | ax-mp 5 |
. . . . . . . . . 10
β’ (π‘ β ran πΌ β βπ β (0..^π)(πΌβπ) = π‘) |
105 | 104 | biimpi 215 |
. . . . . . . . 9
β’ (π‘ β ran πΌ β βπ β (0..^π)(πΌβπ) = π‘) |
106 | 105 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π‘ β ran πΌ) β βπ β (0..^π)(πΌβπ) = π‘) |
107 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
108 | | elfzofz 13645 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β π β (0...π)) |
109 | 108 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
110 | 107, 109 | ffvelcdmd 7085 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
111 | | fzofzp1 13726 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β (π + 1) β (0...π)) |
112 | 111 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
113 | 107, 112 | ffvelcdmd 7085 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
114 | | fourierdlem71.l |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
115 | | fourierdlem71.r |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
116 | 110, 113,
44, 114, 115 | cncfioobd 44600 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π) |
117 | 116 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π) |
118 | | fvres 6908 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯) = (πΉβπ₯)) |
119 | 118 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β (absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) = (absβ(πΉβπ₯))) |
120 | 119 | breq1d 5158 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β ((absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π β (absβ(πΉβπ₯)) β€ π)) |
121 | 120 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β ((absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π β (absβ(πΉβπ₯)) β€ π)) |
122 | 121 | ralbidva 3176 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ₯)) β€ π)) |
123 | 122 | rexbidv 3179 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π β βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ₯)) β€ π)) |
124 | 123 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β (βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π β βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ₯)) β€ π)) |
125 | 37, 42 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
126 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌβπ) = π‘ β (πΌβπ) = π‘) |
127 | 125, 126 | sylan9req 2794 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0..^π) β§ (πΌβπ) = π‘) β ((πβπ)(,)(πβ(π + 1))) = π‘) |
128 | 127 | 3adant1 1131 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β ((πβπ)(,)(πβ(π + 1))) = π‘) |
129 | 128 | raleqdv 3326 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β (βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ₯)) β€ π β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π)) |
130 | 129 | rexbidv 3179 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β (βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ₯)) β€ π β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π)) |
131 | 124, 130 | bitrd 279 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β (βπ β β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(absβ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ₯)) β€ π β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π)) |
132 | 117, 131 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π) β§ (πΌβπ) = π‘) β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π) |
133 | 132 | 3exp 1120 |
. . . . . . . . . 10
β’ (π β (π β (0..^π) β ((πΌβπ) = π‘ β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π))) |
134 | 133 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β ran πΌ) β (π β (0..^π) β ((πΌβπ) = π‘ β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π))) |
135 | 134 | rexlimdv 3154 |
. . . . . . . 8
β’ ((π β§ π‘ β ran πΌ) β (βπ β (0..^π)(πΌβπ) = π‘ β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π)) |
136 | 106, 135 | mpd 15 |
. . . . . . 7
β’ ((π β§ π‘ β ran πΌ) β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π) |
137 | 136 | adantlr 714 |
. . . . . 6
β’ (((π β§ π€ = βͺ ran πΌ) β§ π‘ β ran πΌ) β βπ β β βπ₯ β π‘ (absβ(πΉβπ₯)) β€ π) |
138 | | eqimss 4040 |
. . . . . . 7
β’ (π€ = βͺ
ran πΌ β π€ β βͺ ran πΌ) |
139 | 138 | adantl 483 |
. . . . . 6
β’ ((π β§ π€ = βͺ ran πΌ) β π€ β βͺ ran
πΌ) |
140 | 96, 101, 137, 139 | ssfiunibd 44006 |
. . . . 5
β’ ((π β§ π€ = βͺ ran πΌ) β βπ¦ β β βπ₯ β π€ (absβ(πΉβπ₯)) β€ π¦) |
141 | 88, 92, 140 | syl2anc 585 |
. . . 4
β’ (((π β§ π€ β {(ran π β© dom πΉ), βͺ ran πΌ}) β§ Β¬ π€ = (ran π β© dom πΉ)) β βπ¦ β β βπ₯ β π€ (absβ(πΉβπ₯)) β€ π¦) |
142 | 87, 141 | pm2.61dan 812 |
. . 3
β’ ((π β§ π€ β {(ran π β© dom πΉ), βͺ ran πΌ}) β βπ¦ β β βπ₯ β π€ (absβ(πΉβπ₯)) β€ π¦) |
143 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ π₯ β ran π) β π₯ β ran π) |
144 | | elinel2 4196 |
. . . . . . . . . 10
β’ (π₯ β ((π΄[,]π΅) β© dom πΉ) β π₯ β dom πΉ) |
145 | 144 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ π₯ β ran π) β π₯ β dom πΉ) |
146 | 143, 145 | elind 4194 |
. . . . . . . 8
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ π₯ β ran π) β π₯ β (ran π β© dom πΉ)) |
147 | | elun1 4176 |
. . . . . . . 8
β’ (π₯ β (ran π β© dom πΉ) β π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
148 | 146, 147 | syl 17 |
. . . . . . 7
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ π₯ β ran π) β π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
149 | | fourierdlem71.7 |
. . . . . . . . . . . 12
β’ (π β π β β) |
150 | 149 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β π β β) |
151 | 7 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β π:(0...π)βΆβ) |
152 | | elinel1 4195 |
. . . . . . . . . . . . . 14
β’ (π₯ β ((π΄[,]π΅) β© dom πΉ) β π₯ β (π΄[,]π΅)) |
153 | 152 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β π₯ β (π΄[,]π΅)) |
154 | | fourierdlem71.q0 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ0) = π΄) |
155 | 154 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ = (πβ0)) |
156 | 155 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β π΄ = (πβ0)) |
157 | | fourierdlem71.10 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβπ) = π΅) |
158 | 157 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ = (πβπ)) |
159 | 158 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β π΅ = (πβπ)) |
160 | 156, 159 | oveq12d 7424 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β (π΄[,]π΅) = ((πβ0)[,](πβπ))) |
161 | 153, 160 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β π₯ β ((πβ0)[,](πβπ))) |
162 | 161 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β π₯ β ((πβ0)[,](πβπ))) |
163 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β Β¬ π₯ β ran π) |
164 | | fveq2 6889 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
165 | 164 | breq1d 5158 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ) < π₯ β (πβπ) < π₯)) |
166 | 165 | cbvrabv 3443 |
. . . . . . . . . . . 12
β’ {π β (0..^π) β£ (πβπ) < π₯} = {π β (0..^π) β£ (πβπ) < π₯} |
167 | 166 | supeq1i 9439 |
. . . . . . . . . . 11
β’
sup({π β
(0..^π) β£ (πβπ) < π₯}, β, < ) = sup({π β (0..^π) β£ (πβπ) < π₯}, β, < ) |
168 | 150, 151,
162, 163, 167 | fourierdlem25 44835 |
. . . . . . . . . 10
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β βπ β (0..^π)π₯ β ((πβπ)(,)(πβ(π + 1)))) |
169 | 39 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom πΌ β§ π₯ β (πΌβπ))) β π β (0..^π)) |
170 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom πΌ β§ π₯ β (πΌβπ))) β π₯ β (πΌβπ)) |
171 | 169, 125 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom πΌ β§ π₯ β (πΌβπ))) β (πΌβπ) = ((πβπ)(,)(πβ(π + 1)))) |
172 | 170, 171 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom πΌ β§ π₯ β (πΌβπ))) β π₯ β ((πβπ)(,)(πβ(π + 1)))) |
173 | 169, 172 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom πΌ β§ π₯ β (πΌβπ))) β (π β (0..^π) β§ π₯ β ((πβπ)(,)(πβ(π + 1))))) |
174 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β π β (0..^π)) |
175 | 174, 38 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β π β dom πΌ) |
176 | 175 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (0..^π) β§ π₯ β ((πβπ)(,)(πβ(π + 1))))) β π β dom πΌ) |
177 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (0..^π) β§ π₯ β ((πβπ)(,)(πβ(π + 1))))) β π₯ β ((πβπ)(,)(πβ(π + 1)))) |
178 | 125 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β ((πβπ)(,)(πβ(π + 1))) = (πΌβπ)) |
179 | 178 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (0..^π) β§ π₯ β ((πβπ)(,)(πβ(π + 1))))) β ((πβπ)(,)(πβ(π + 1))) = (πΌβπ)) |
180 | 177, 179 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (0..^π) β§ π₯ β ((πβπ)(,)(πβ(π + 1))))) β π₯ β (πΌβπ)) |
181 | 176, 180 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (0..^π) β§ π₯ β ((πβπ)(,)(πβ(π + 1))))) β (π β dom πΌ β§ π₯ β (πΌβπ))) |
182 | 173, 181 | impbida 800 |
. . . . . . . . . . . 12
β’ (π β ((π β dom πΌ β§ π₯ β (πΌβπ)) β (π β (0..^π) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))))) |
183 | 182 | rexbidv2 3175 |
. . . . . . . . . . 11
β’ (π β (βπ β dom πΌ π₯ β (πΌβπ) β βπ β (0..^π)π₯ β ((πβπ)(,)(πβ(π + 1))))) |
184 | 183 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β (βπ β dom πΌ π₯ β (πΌβπ) β βπ β (0..^π)π₯ β ((πβπ)(,)(πβ(π + 1))))) |
185 | 168, 184 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β βπ β dom πΌ π₯ β (πΌβπ)) |
186 | 185, 33 | sylibr 233 |
. . . . . . . 8
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β π₯ β βͺ ran
πΌ) |
187 | | elun2 4177 |
. . . . . . . 8
β’ (π₯ β βͺ ran πΌ β π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
188 | 186, 187 | syl 17 |
. . . . . . 7
β’ (((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β§ Β¬ π₯ β ran π) β π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
189 | 148, 188 | pm2.61dan 812 |
. . . . . 6
β’ ((π β§ π₯ β ((π΄[,]π΅) β© dom πΉ)) β π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
190 | 189 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ₯ β ((π΄[,]π΅) β© dom πΉ)π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
191 | | dfss3 3970 |
. . . . 5
β’ (((π΄[,]π΅) β© dom πΉ) β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ) β βπ₯ β ((π΄[,]π΅) β© dom πΉ)π₯ β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
192 | 190, 191 | sylibr 233 |
. . . 4
β’ (π β ((π΄[,]π΅) β© dom πΉ) β ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
193 | 13, 21, 23 | syl2anc 585 |
. . . 4
β’ (π β βͺ {(ran π β© dom πΉ), βͺ ran πΌ} = ((ran π β© dom πΉ) βͺ βͺ ran
πΌ)) |
194 | 192, 193 | sseqtrrd 4023 |
. . 3
β’ (π β ((π΄[,]π΅) β© dom πΉ) β βͺ {(ran
π β© dom πΉ), βͺ
ran πΌ}) |
195 | 2, 64, 142, 194 | ssfiunibd 44006 |
. 2
β’ (π β βπ¦ β β βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) |
196 | | nfv 1918 |
. . . . . 6
β’
β²π₯π |
197 | | nfra1 3282 |
. . . . . 6
β’
β²π₯βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦ |
198 | 196, 197 | nfan 1903 |
. . . . 5
β’
β²π₯(π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) |
199 | | fourierdlem71.dmf |
. . . . . . . . . . . . 13
β’ (π β dom πΉ β β) |
200 | 199 | sselda 3982 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β dom πΉ) β π₯ β β) |
201 | | fourierdlem71.b |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β β) |
202 | 201 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β dom πΉ) β π΅ β β) |
203 | 202, 200 | resubcld 11639 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β dom πΉ) β (π΅ β π₯) β β) |
204 | | fourierdlem71.t |
. . . . . . . . . . . . . . . . . . 19
β’ π = (π΅ β π΄) |
205 | | fourierdlem71.a |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β β) |
206 | 201, 205 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π΅ β π΄) β β) |
207 | 204, 206 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
208 | 207 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β dom πΉ) β π β β) |
209 | | fourierdlem71.altb |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΄ < π΅) |
210 | 205, 201 | posdifd 11798 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
211 | 209, 210 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 0 < (π΅ β π΄)) |
212 | 211, 204 | breqtrrdi 5190 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 < π) |
213 | 212 | gt0ne0d 11775 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β 0) |
214 | 213 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β dom πΉ) β π β 0) |
215 | 203, 208,
214 | redivcld 12039 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β dom πΉ) β ((π΅ β π₯) / π) β β) |
216 | 215 | flcld 13760 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β dom πΉ) β (ββ((π΅ β π₯) / π)) β β€) |
217 | 216 | zred 12663 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β dom πΉ) β (ββ((π΅ β π₯) / π)) β β) |
218 | 217, 208 | remulcld 11241 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β dom πΉ) β ((ββ((π΅ β π₯) / π)) Β· π) β β) |
219 | 200, 218 | readdcld 11240 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β dom πΉ) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) β β) |
220 | | fourierdlem71.e |
. . . . . . . . . . . . 13
β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
221 | 220 | fvmpt2 7007 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) β β) β (πΈβπ₯) = (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
222 | 200, 219,
221 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β dom πΉ) β (πΈβπ₯) = (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
223 | 222 | fveq2d 6893 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom πΉ) β (πΉβ(πΈβπ₯)) = (πΉβ(π₯ + ((ββ((π΅ β π₯) / π)) Β· π)))) |
224 | | fvex 6902 |
. . . . . . . . . . . 12
β’
(ββ((π΅
β π₯) / π)) β V |
225 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ (π = (ββ((π΅ β π₯) / π)) β (π β β€ β (ββ((π΅ β π₯) / π)) β β€)) |
226 | 225 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = (ββ((π΅ β π₯) / π)) β (((π β§ π₯ β dom πΉ) β§ π β β€) β ((π β§ π₯ β dom πΉ) β§ (ββ((π΅ β π₯) / π)) β β€))) |
227 | | oveq1 7413 |
. . . . . . . . . . . . . . . 16
β’ (π = (ββ((π΅ β π₯) / π)) β (π Β· π) = ((ββ((π΅ β π₯) / π)) Β· π)) |
228 | 227 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
β’ (π = (ββ((π΅ β π₯) / π)) β (π₯ + (π Β· π)) = (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
229 | 228 | fveq2d 6893 |
. . . . . . . . . . . . . 14
β’ (π = (ββ((π΅ β π₯) / π)) β (πΉβ(π₯ + (π Β· π))) = (πΉβ(π₯ + ((ββ((π΅ β π₯) / π)) Β· π)))) |
230 | 229 | eqeq1d 2735 |
. . . . . . . . . . . . 13
β’ (π = (ββ((π΅ β π₯) / π)) β ((πΉβ(π₯ + (π Β· π))) = (πΉβπ₯) β (πΉβ(π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) = (πΉβπ₯))) |
231 | 226, 230 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = (ββ((π΅ β π₯) / π)) β ((((π β§ π₯ β dom πΉ) β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) β (((π β§ π₯ β dom πΉ) β§ (ββ((π΅ β π₯) / π)) β β€) β (πΉβ(π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) = (πΉβπ₯)))) |
232 | | fourierdlem71.fxpt |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β dom πΉ) β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) |
233 | 224, 231,
232 | vtocl 3550 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β dom πΉ) β§ (ββ((π΅ β π₯) / π)) β β€) β (πΉβ(π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) = (πΉβπ₯)) |
234 | 216, 233 | mpdan 686 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom πΉ) β (πΉβ(π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) = (πΉβπ₯)) |
235 | 223, 234 | eqtr2d 2774 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΉ) β (πΉβπ₯) = (πΉβ(πΈβπ₯))) |
236 | 235 | fveq2d 6893 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΉ) β (absβ(πΉβπ₯)) = (absβ(πΉβ(πΈβπ₯)))) |
237 | 236 | adantlr 714 |
. . . . . . 7
β’ (((π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) β§ π₯ β dom πΉ) β (absβ(πΉβπ₯)) = (absβ(πΉβ(πΈβπ₯)))) |
238 | | fveq2 6889 |
. . . . . . . . . . . . 13
β’ (π₯ = π€ β (πΉβπ₯) = (πΉβπ€)) |
239 | 238 | fveq2d 6893 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (absβ(πΉβπ₯)) = (absβ(πΉβπ€))) |
240 | 239 | breq1d 5158 |
. . . . . . . . . . 11
β’ (π₯ = π€ β ((absβ(πΉβπ₯)) β€ π¦ β (absβ(πΉβπ€)) β€ π¦)) |
241 | 240 | cbvralvw 3235 |
. . . . . . . . . 10
β’
(βπ₯ β
((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦ β βπ€ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ€)) β€ π¦) |
242 | 241 | biimpi 215 |
. . . . . . . . 9
β’
(βπ₯ β
((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦ β βπ€ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ€)) β€ π¦) |
243 | 242 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) β§ π₯ β dom πΉ) β βπ€ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ€)) β€ π¦) |
244 | | iocssicc 13411 |
. . . . . . . . . . 11
β’ (π΄(,]π΅) β (π΄[,]π΅) |
245 | 205 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β dom πΉ) β π΄ β β) |
246 | 209 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β dom πΉ) β π΄ < π΅) |
247 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β π₯ = π¦) |
248 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β (π΅ β π₯) = (π΅ β π¦)) |
249 | 248 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β ((π΅ β π₯) / π) = ((π΅ β π¦) / π)) |
250 | 249 | fveq2d 6893 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (ββ((π΅ β π₯) / π)) = (ββ((π΅ β π¦) / π))) |
251 | 250 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β ((ββ((π΅ β π₯) / π)) Β· π) = ((ββ((π΅ β π¦) / π)) Β· π)) |
252 | 247, 251 | oveq12d 7424 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = (π¦ + ((ββ((π΅ β π¦) / π)) Β· π))) |
253 | 252 | cbvmptv 5261 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) = (π¦ β β β¦ (π¦ + ((ββ((π΅ β π¦) / π)) Β· π))) |
254 | 220, 253 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ πΈ = (π¦ β β β¦ (π¦ + ((ββ((π΅ β π¦) / π)) Β· π))) |
255 | 245, 202,
246, 204, 254 | fourierdlem4 44814 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β dom πΉ) β πΈ:ββΆ(π΄(,]π΅)) |
256 | 255, 200 | ffvelcdmd 7085 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β dom πΉ) β (πΈβπ₯) β (π΄(,]π΅)) |
257 | 244, 256 | sselid 3980 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom πΉ) β (πΈβπ₯) β (π΄[,]π΅)) |
258 | 228 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = (ββ((π΅ β π₯) / π)) β ((π₯ + (π Β· π)) β dom πΉ β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) β dom πΉ)) |
259 | 226, 258 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = (ββ((π΅ β π₯) / π)) β ((((π β§ π₯ β dom πΉ) β§ π β β€) β (π₯ + (π Β· π)) β dom πΉ) β (((π β§ π₯ β dom πΉ) β§ (ββ((π΅ β π₯) / π)) β β€) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) β dom πΉ))) |
260 | | fourierdlem71.xpt |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β dom πΉ) β§ π β β€) β (π₯ + (π Β· π)) β dom πΉ) |
261 | 224, 259,
260 | vtocl 3550 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β dom πΉ) β§ (ββ((π΅ β π₯) / π)) β β€) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) β dom πΉ) |
262 | 216, 261 | mpdan 686 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β dom πΉ) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) β dom πΉ) |
263 | 222, 262 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom πΉ) β (πΈβπ₯) β dom πΉ) |
264 | 257, 263 | elind 4194 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΉ) β (πΈβπ₯) β ((π΄[,]π΅) β© dom πΉ)) |
265 | 264 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) β§ π₯ β dom πΉ) β (πΈβπ₯) β ((π΄[,]π΅) β© dom πΉ)) |
266 | | fveq2 6889 |
. . . . . . . . . . 11
β’ (π€ = (πΈβπ₯) β (πΉβπ€) = (πΉβ(πΈβπ₯))) |
267 | 266 | fveq2d 6893 |
. . . . . . . . . 10
β’ (π€ = (πΈβπ₯) β (absβ(πΉβπ€)) = (absβ(πΉβ(πΈβπ₯)))) |
268 | 267 | breq1d 5158 |
. . . . . . . . 9
β’ (π€ = (πΈβπ₯) β ((absβ(πΉβπ€)) β€ π¦ β (absβ(πΉβ(πΈβπ₯))) β€ π¦)) |
269 | 268 | rspccva 3612 |
. . . . . . . 8
β’
((βπ€ β
((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ€)) β€ π¦ β§ (πΈβπ₯) β ((π΄[,]π΅) β© dom πΉ)) β (absβ(πΉβ(πΈβπ₯))) β€ π¦) |
270 | 243, 265,
269 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) β§ π₯ β dom πΉ) β (absβ(πΉβ(πΈβπ₯))) β€ π¦) |
271 | 237, 270 | eqbrtrd 5170 |
. . . . . 6
β’ (((π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) β§ π₯ β dom πΉ) β (absβ(πΉβπ₯)) β€ π¦) |
272 | 271 | ex 414 |
. . . . 5
β’ ((π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) β (π₯ β dom πΉ β (absβ(πΉβπ₯)) β€ π¦)) |
273 | 198, 272 | ralrimi 3255 |
. . . 4
β’ ((π β§ βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦) β βπ₯ β dom πΉ(absβ(πΉβπ₯)) β€ π¦) |
274 | 273 | ex 414 |
. . 3
β’ (π β (βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦ β βπ₯ β dom πΉ(absβ(πΉβπ₯)) β€ π¦)) |
275 | 274 | reximdv 3171 |
. 2
β’ (π β (βπ¦ β β βπ₯ β ((π΄[,]π΅) β© dom πΉ)(absβ(πΉβπ₯)) β€ π¦ β βπ¦ β β βπ₯ β dom πΉ(absβ(πΉβπ₯)) β€ π¦)) |
276 | 195, 275 | mpd 15 |
1
β’ (π β βπ¦ β β βπ₯ β dom πΉ(absβ(πΉβπ₯)) β€ π¦) |