Step | Hyp | Ref
| Expression |
1 | | ssrab2 4038 |
. . . 4
โข {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ (0..^๐) |
2 | | ltso 11240 |
. . . . . 6
โข < Or
โ |
3 | 2 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ < Or
โ) |
4 | | fzfi 13883 |
. . . . . . 7
โข
(0...๐) โ
Fin |
5 | | fzossfz 13597 |
. . . . . . . 8
โข
(0..^๐) โ
(0...๐) |
6 | 1, 5 | sstri 3954 |
. . . . . . 7
โข {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ (0...๐) |
7 | | ssfi 9120 |
. . . . . . 7
โข
(((0...๐) โ Fin
โง {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ (0...๐)) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ Fin) |
8 | 4, 6, 7 | mp2an 691 |
. . . . . 6
โข {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ Fin |
9 | 8 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ Fin) |
10 | | 0zd 12516 |
. . . . . . . . 9
โข (๐ โ 0 โ
โค) |
11 | | fourierdlem37.m |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
12 | 11 | nnzd 12531 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
13 | 11 | nngt0d 12207 |
. . . . . . . . 9
โข (๐ โ 0 < ๐) |
14 | | fzolb 13584 |
. . . . . . . . 9
โข (0 โ
(0..^๐) โ (0 โ
โค โง ๐ โ
โค โง 0 < ๐)) |
15 | 10, 12, 13, 14 | syl3anbrc 1344 |
. . . . . . . 8
โข (๐ โ 0 โ (0..^๐)) |
16 | 15 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ 0 โ (0..^๐)) |
17 | | fourierdlem37.q |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ (๐โ๐)) |
18 | | fourierdlem37.p |
. . . . . . . . . . . . . . . . . 18
โข ๐ = (๐ โ โ โฆ {๐ โ (โ โm
(0...๐)) โฃ (((๐โ0) = ๐ด โง (๐โ๐) = ๐ต) โง โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1)))}) |
19 | 18 | fourierdlem2 44436 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ โ (๐โ๐) โ (๐ โ (โ โm
(0...๐)) โง (((๐โ0) = ๐ด โง (๐โ๐) = ๐ต) โง โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1)))))) |
20 | 11, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โ (๐โ๐) โ (๐ โ (โ โm
(0...๐)) โง (((๐โ0) = ๐ด โง (๐โ๐) = ๐ต) โง โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1)))))) |
21 | 17, 20 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ (โ โm
(0...๐)) โง (((๐โ0) = ๐ด โง (๐โ๐) = ๐ต) โง โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1))))) |
22 | 21 | simprd 497 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐โ0) = ๐ด โง (๐โ๐) = ๐ต) โง โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1)))) |
23 | 22 | simplld 767 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โ0) = ๐ด) |
24 | 18, 11, 17 | fourierdlem11 44445 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต)) |
25 | 24 | simp1d 1143 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ โ) |
26 | 23, 25 | eqeltrd 2834 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ0) โ โ) |
27 | 26, 23 | eqled 11263 |
. . . . . . . . . . 11
โข (๐ โ (๐โ0) โค ๐ด) |
28 | 27 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง (๐ธโ๐ฅ) = ๐ต) โ (๐โ0) โค ๐ด) |
29 | | iftrue 4493 |
. . . . . . . . . . . 12
โข ((๐ธโ๐ฅ) = ๐ต โ if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ)) = ๐ด) |
30 | 29 | eqcomd 2739 |
. . . . . . . . . . 11
โข ((๐ธโ๐ฅ) = ๐ต โ ๐ด = if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
31 | 30 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง (๐ธโ๐ฅ) = ๐ต) โ ๐ด = if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
32 | 28, 31 | breqtrd 5132 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง (๐ธโ๐ฅ) = ๐ต) โ (๐โ0) โค if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
33 | 26 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ) โ (๐โ0) โ โ) |
34 | 25 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ โ) |
35 | 34 | rexrd 11210 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ
โ*) |
36 | 24 | simp2d 1144 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โ โ) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ โ) โ ๐ต โ โ) |
38 | | iocssre 13350 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ*
โง ๐ต โ โ)
โ (๐ด(,]๐ต) โ
โ) |
39 | 35, 37, 38 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ (๐ด(,]๐ต) โ โ) |
40 | 24 | simp3d 1145 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด < ๐ต) |
41 | | fourierdlem37.t |
. . . . . . . . . . . . . . 15
โข ๐ = (๐ต โ ๐ด) |
42 | | fourierdlem37.e |
. . . . . . . . . . . . . . 15
โข ๐ธ = (๐ฅ โ โ โฆ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐))) |
43 | 25, 36, 40, 41, 42 | fourierdlem4 44438 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ธ:โโถ(๐ด(,]๐ต)) |
44 | 43 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ (๐ธโ๐ฅ) โ (๐ด(,]๐ต)) |
45 | 39, 44 | sseldd 3946 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ) โ (๐ธโ๐ฅ) โ โ) |
46 | 23 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ (๐โ0) = ๐ด) |
47 | | elioc2 13333 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ*
โง ๐ต โ โ)
โ ((๐ธโ๐ฅ) โ (๐ด(,]๐ต) โ ((๐ธโ๐ฅ) โ โ โง ๐ด < (๐ธโ๐ฅ) โง (๐ธโ๐ฅ) โค ๐ต))) |
48 | 35, 37, 47 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ โ) โ ((๐ธโ๐ฅ) โ (๐ด(,]๐ต) โ ((๐ธโ๐ฅ) โ โ โง ๐ด < (๐ธโ๐ฅ) โง (๐ธโ๐ฅ) โค ๐ต))) |
49 | 44, 48 | mpbid 231 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ โ) โ ((๐ธโ๐ฅ) โ โ โง ๐ด < (๐ธโ๐ฅ) โง (๐ธโ๐ฅ) โค ๐ต)) |
50 | 49 | simp2d 1144 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ ๐ด < (๐ธโ๐ฅ)) |
51 | 46, 50 | eqbrtrd 5128 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ) โ (๐โ0) < (๐ธโ๐ฅ)) |
52 | 33, 45, 51 | ltled 11308 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ) โ (๐โ0) โค (๐ธโ๐ฅ)) |
53 | 52 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ยฌ (๐ธโ๐ฅ) = ๐ต) โ (๐โ0) โค (๐ธโ๐ฅ)) |
54 | | iffalse 4496 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ธโ๐ฅ) = ๐ต โ if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ)) = (๐ธโ๐ฅ)) |
55 | 54 | eqcomd 2739 |
. . . . . . . . . . 11
โข (ยฌ
(๐ธโ๐ฅ) = ๐ต โ (๐ธโ๐ฅ) = if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
56 | 55 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ยฌ (๐ธโ๐ฅ) = ๐ต) โ (๐ธโ๐ฅ) = if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
57 | 53, 56 | breqtrd 5132 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ยฌ (๐ธโ๐ฅ) = ๐ต) โ (๐โ0) โค if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
58 | 32, 57 | pm2.61dan 812 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ (๐โ0) โค if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
59 | | fourierdlem37.l |
. . . . . . . . . 10
โข ๐ฟ = (๐ฆ โ (๐ด(,]๐ต) โฆ if(๐ฆ = ๐ต, ๐ด, ๐ฆ)) |
60 | 59 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ) โ ๐ฟ = (๐ฆ โ (๐ด(,]๐ต) โฆ if(๐ฆ = ๐ต, ๐ด, ๐ฆ))) |
61 | | eqeq1 2737 |
. . . . . . . . . . 11
โข (๐ฆ = (๐ธโ๐ฅ) โ (๐ฆ = ๐ต โ (๐ธโ๐ฅ) = ๐ต)) |
62 | | id 22 |
. . . . . . . . . . 11
โข (๐ฆ = (๐ธโ๐ฅ) โ ๐ฆ = (๐ธโ๐ฅ)) |
63 | 61, 62 | ifbieq2d 4513 |
. . . . . . . . . 10
โข (๐ฆ = (๐ธโ๐ฅ) โ if(๐ฆ = ๐ต, ๐ด, ๐ฆ) = if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
64 | 63 | adantl 483 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ฆ = (๐ธโ๐ฅ)) โ if(๐ฆ = ๐ต, ๐ด, ๐ฆ) = if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
65 | 34, 45 | ifcld 4533 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ) โ if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ)) โ โ) |
66 | 60, 64, 44, 65 | fvmptd 6956 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ (๐ฟโ(๐ธโ๐ฅ)) = if((๐ธโ๐ฅ) = ๐ต, ๐ด, (๐ธโ๐ฅ))) |
67 | 58, 66 | breqtrrd 5134 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ (๐โ0) โค (๐ฟโ(๐ธโ๐ฅ))) |
68 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ = 0 โ (๐โ๐) = (๐โ0)) |
69 | 68 | breq1d 5116 |
. . . . . . . 8
โข (๐ = 0 โ ((๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ)) โ (๐โ0) โค (๐ฟโ(๐ธโ๐ฅ)))) |
70 | 69 | elrab 3646 |
. . . . . . 7
โข (0 โ
{๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ (0 โ (0..^๐) โง (๐โ0) โค (๐ฟโ(๐ธโ๐ฅ)))) |
71 | 16, 67, 70 | sylanbrc 584 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ 0 โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}) |
72 | 71 | ne0d 4296 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ โ
) |
73 | | fzssz 13449 |
. . . . . . . . 9
โข
(0...๐) โ
โค |
74 | 5, 73 | sstri 3954 |
. . . . . . . 8
โข
(0..^๐) โ
โค |
75 | | zssre 12511 |
. . . . . . . 8
โข โค
โ โ |
76 | 74, 75 | sstri 3954 |
. . . . . . 7
โข
(0..^๐) โ
โ |
77 | 1, 76 | sstri 3954 |
. . . . . 6
โข {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ โ |
78 | 77 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ โ) |
79 | | fisupcl 9410 |
. . . . 5
โข (( <
Or โ โง ({๐ โ
(0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ Fin โง {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ โ
โง {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))} โ โ)) โ sup({๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}, โ, < ) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}) |
80 | 3, 9, 72, 78, 79 | syl13anc 1373 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ sup({๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}, โ, < ) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}) |
81 | 1, 80 | sselid 3943 |
. . 3
โข ((๐ โง ๐ฅ โ โ) โ sup({๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}, โ, < ) โ (0..^๐)) |
82 | | fourierdlem37.i |
. . 3
โข ๐ผ = (๐ฅ โ โ โฆ sup({๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}, โ, < )) |
83 | 81, 82 | fmptd 7063 |
. 2
โข (๐ โ ๐ผ:โโถ(0..^๐)) |
84 | 80 | ex 414 |
. 2
โข (๐ โ (๐ฅ โ โ โ sup({๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}, โ, < ) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))})) |
85 | 83, 84 | jca 513 |
1
โข (๐ โ (๐ผ:โโถ(0..^๐) โง (๐ฅ โ โ โ sup({๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}, โ, < ) โ {๐ โ (0..^๐) โฃ (๐โ๐) โค (๐ฟโ(๐ธโ๐ฅ))}))) |