Metamath Proof Explorer


Theorem fourierdlem108

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any positive value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem108.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
fourierdlem108.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
fourierdlem108.t โŠข ๐‘‡ = ( ๐ต โˆ’ ๐ด )
fourierdlem108.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„+ )
fourierdlem108.p โŠข ๐‘ƒ = ( ๐‘š โˆˆ โ„• โ†ฆ { ๐‘ โˆˆ ( โ„ โ†‘m ( 0 ... ๐‘š ) ) โˆฃ ( ( ( ๐‘ โ€˜ 0 ) = ๐ด โˆง ( ๐‘ โ€˜ ๐‘š ) = ๐ต ) โˆง โˆ€ ๐‘– โˆˆ ( 0 ..^ ๐‘š ) ( ๐‘ โ€˜ ๐‘– ) < ( ๐‘ โ€˜ ( ๐‘– + 1 ) ) ) } )
fourierdlem108.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
fourierdlem108.q โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ( ๐‘ƒ โ€˜ ๐‘€ ) )
fourierdlem108.f โŠข ( ๐œ‘ โ†’ ๐น : โ„ โŸถ โ„‚ )
fourierdlem108.fper โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„ ) โ†’ ( ๐น โ€˜ ( ๐‘ฅ + ๐‘‡ ) ) = ( ๐น โ€˜ ๐‘ฅ ) )
fourierdlem108.fcn โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ( ๐น โ†พ ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โˆˆ ( ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) โ€“cnโ†’ โ„‚ ) )
fourierdlem108.r โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐‘… โˆˆ ( ( ๐น โ†พ ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘„ โ€˜ ๐‘– ) ) )
fourierdlem108.l โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐ฟ โˆˆ ( ( ๐น โ†พ ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) )
Assertion fourierdlem108 ( ๐œ‘ โ†’ โˆซ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ( ๐ต โˆ’ ๐‘‹ ) ) ( ๐น โ€˜ ๐‘ฅ ) d ๐‘ฅ = โˆซ ( ๐ด [,] ๐ต ) ( ๐น โ€˜ ๐‘ฅ ) d ๐‘ฅ )

Proof

Step Hyp Ref Expression
1 fourierdlem108.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2 fourierdlem108.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
3 fourierdlem108.t โŠข ๐‘‡ = ( ๐ต โˆ’ ๐ด )
4 fourierdlem108.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„+ )
5 fourierdlem108.p โŠข ๐‘ƒ = ( ๐‘š โˆˆ โ„• โ†ฆ { ๐‘ โˆˆ ( โ„ โ†‘m ( 0 ... ๐‘š ) ) โˆฃ ( ( ( ๐‘ โ€˜ 0 ) = ๐ด โˆง ( ๐‘ โ€˜ ๐‘š ) = ๐ต ) โˆง โˆ€ ๐‘– โˆˆ ( 0 ..^ ๐‘š ) ( ๐‘ โ€˜ ๐‘– ) < ( ๐‘ โ€˜ ( ๐‘– + 1 ) ) ) } )
6 fourierdlem108.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
7 fourierdlem108.q โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ( ๐‘ƒ โ€˜ ๐‘€ ) )
8 fourierdlem108.f โŠข ( ๐œ‘ โ†’ ๐น : โ„ โŸถ โ„‚ )
9 fourierdlem108.fper โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„ ) โ†’ ( ๐น โ€˜ ( ๐‘ฅ + ๐‘‡ ) ) = ( ๐น โ€˜ ๐‘ฅ ) )
10 fourierdlem108.fcn โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ( ๐น โ†พ ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โˆˆ ( ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) โ€“cnโ†’ โ„‚ ) )
11 fourierdlem108.r โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐‘… โˆˆ ( ( ๐น โ†พ ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘„ โ€˜ ๐‘– ) ) )
12 fourierdlem108.l โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐ฟ โˆˆ ( ( ๐น โ†พ ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) )
13 eqid โŠข ( ๐‘š โˆˆ โ„• โ†ฆ { ๐‘ โˆˆ ( โ„ โ†‘m ( 0 ... ๐‘š ) ) โˆฃ ( ( ( ๐‘ โ€˜ 0 ) = ( ๐ด โˆ’ ๐‘‹ ) โˆง ( ๐‘ โ€˜ ๐‘š ) = ๐ด ) โˆง โˆ€ ๐‘– โˆˆ ( 0 ..^ ๐‘š ) ( ๐‘ โ€˜ ๐‘– ) < ( ๐‘ โ€˜ ( ๐‘– + 1 ) ) ) } ) = ( ๐‘š โˆˆ โ„• โ†ฆ { ๐‘ โˆˆ ( โ„ โ†‘m ( 0 ... ๐‘š ) ) โˆฃ ( ( ( ๐‘ โ€˜ 0 ) = ( ๐ด โˆ’ ๐‘‹ ) โˆง ( ๐‘ โ€˜ ๐‘š ) = ๐ด ) โˆง โˆ€ ๐‘– โˆˆ ( 0 ..^ ๐‘š ) ( ๐‘ โ€˜ ๐‘– ) < ( ๐‘ โ€˜ ( ๐‘– + 1 ) ) ) } )
14 oveq1 โŠข ( ๐‘ค = ๐‘ฆ โ†’ ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) = ( ๐‘ฆ + ( ๐‘˜ ยท ๐‘‡ ) ) )
15 14 eleq1d โŠข ( ๐‘ค = ๐‘ฆ โ†’ ( ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ โ†” ( ๐‘ฆ + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ ) )
16 15 rexbidv โŠข ( ๐‘ค = ๐‘ฆ โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ โ†” โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ฆ + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ ) )
17 16 cbvrabv โŠข { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } = { ๐‘ฆ โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ฆ + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ }
18 17 uneq2i โŠข ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) = ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ฆ โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ฆ + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } )
19 oveq1 โŠข ( ๐‘™ = ๐‘˜ โ†’ ( ๐‘™ ยท ๐‘‡ ) = ( ๐‘˜ ยท ๐‘‡ ) )
20 19 oveq2d โŠข ( ๐‘™ = ๐‘˜ โ†’ ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) = ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) )
21 20 eleq1d โŠข ( ๐‘™ = ๐‘˜ โ†’ ( ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ โ†” ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ ) )
22 21 cbvrexvw โŠข ( โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ โ†” โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ )
23 22 rgenw โŠข โˆ€ ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) ( โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ โ†” โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ )
24 rabbi โŠข ( โˆ€ ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) ( โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ โ†” โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ ) โ†” { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } = { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } )
25 23 24 mpbi โŠข { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } = { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ }
26 25 uneq2i โŠข ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) = ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } )
27 26 fveq2i โŠข ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) = ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) )
28 27 oveq1i โŠข ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) = ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 )
29 isoeq5 โŠข ( ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) = ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) โ†’ ( ๐‘” Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โ†” ๐‘” Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) ) )
30 26 29 ax-mp โŠข ( ๐‘” Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โ†” ๐‘” Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) )
31 isoeq1 โŠข ( ๐‘” = ๐‘“ โ†’ ( ๐‘” Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โ†” ๐‘“ Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) ) )
32 30 31 bitrid โŠข ( ๐‘” = ๐‘“ โ†’ ( ๐‘” Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โ†” ๐‘“ Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) ) )
33 32 cbviotavw โŠข ( โ„ฉ ๐‘” ๐‘” Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) ) = ( โ„ฉ ๐‘“ ๐‘“ Isom < , < ( ( 0 ... ( ( โ™ฏ โ€˜ ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘™ โˆˆ โ„ค ( ๐‘ค + ( ๐‘™ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) โˆ’ 1 ) ) , ( { ( ๐ด โˆ’ ๐‘‹ ) , ๐ด } โˆช { ๐‘ค โˆˆ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ๐ด ) โˆฃ โˆƒ ๐‘˜ โˆˆ โ„ค ( ๐‘ค + ( ๐‘˜ ยท ๐‘‡ ) ) โˆˆ ran ๐‘„ } ) ) )
34 id โŠข ( ๐‘ค = ๐‘ฅ โ†’ ๐‘ค = ๐‘ฅ )
35 oveq2 โŠข ( ๐‘ค = ๐‘ฅ โ†’ ( ๐ต โˆ’ ๐‘ค ) = ( ๐ต โˆ’ ๐‘ฅ ) )
36 35 oveq1d โŠข ( ๐‘ค = ๐‘ฅ โ†’ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) = ( ( ๐ต โˆ’ ๐‘ฅ ) / ๐‘‡ ) )
37 36 fveq2d โŠข ( ๐‘ค = ๐‘ฅ โ†’ ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) = ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ฅ ) / ๐‘‡ ) ) )
38 37 oveq1d โŠข ( ๐‘ค = ๐‘ฅ โ†’ ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) = ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ฅ ) / ๐‘‡ ) ) ยท ๐‘‡ ) )
39 34 38 oveq12d โŠข ( ๐‘ค = ๐‘ฅ โ†’ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) = ( ๐‘ฅ + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ฅ ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) )
40 39 cbvmptv โŠข ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ ( ๐‘ฅ + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ฅ ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) )
41 eqeq1 โŠข ( ๐‘ค = ๐‘ฆ โ†’ ( ๐‘ค = ๐ต โ†” ๐‘ฆ = ๐ต ) )
42 id โŠข ( ๐‘ค = ๐‘ฆ โ†’ ๐‘ค = ๐‘ฆ )
43 41 42 ifbieq2d โŠข ( ๐‘ค = ๐‘ฆ โ†’ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) = if ( ๐‘ฆ = ๐ต , ๐ด , ๐‘ฆ ) )
44 43 cbvmptv โŠข ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) = ( ๐‘ฆ โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ฆ = ๐ต , ๐ด , ๐‘ฆ ) )
45 fveq2 โŠข ( ๐‘ง = ๐‘ฅ โ†’ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ง ) = ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) )
46 45 fveq2d โŠข ( ๐‘ง = ๐‘ฅ โ†’ ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ง ) ) = ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) )
47 46 breq2d โŠข ( ๐‘ง = ๐‘ฅ โ†’ ( ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ง ) ) โ†” ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) ) )
48 47 rabbidv โŠข ( ๐‘ง = ๐‘ฅ โ†’ { ๐‘— โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ง ) ) } = { ๐‘— โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) } )
49 fveq2 โŠข ( ๐‘— = ๐‘– โ†’ ( ๐‘„ โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) )
50 49 breq1d โŠข ( ๐‘— = ๐‘– โ†’ ( ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) โ†” ( ๐‘„ โ€˜ ๐‘– ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) ) )
51 50 cbvrabv โŠข { ๐‘— โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) } = { ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘– ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) }
52 48 51 eqtrdi โŠข ( ๐‘ง = ๐‘ฅ โ†’ { ๐‘— โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ง ) ) } = { ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘– ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) } )
53 52 supeq1d โŠข ( ๐‘ง = ๐‘ฅ โ†’ sup ( { ๐‘— โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘— ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ง ) ) } , โ„ , < ) = sup ( { ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) โˆฃ ( ๐‘„ โ€˜ ๐‘– ) โ‰ค ( ( ๐‘ค โˆˆ ( ๐ด (,] ๐ต ) โ†ฆ if ( ๐‘ค = ๐ต , ๐ด , ๐‘ค ) ) โ€˜ ( ( ๐‘ค โˆˆ โ„ โ†ฆ ( ๐‘ค + ( ( โŒŠ โ€˜ ( ( ๐ต โˆ’ ๐‘ค ) / ๐‘‡ ) ) ยท ๐‘‡ ) ) ) โ€˜ ๐‘ฅ ) ) } , โ„ , < ) )
54 53 cbvmptv โŠข ( ๐‘ง โˆˆ โ„ โ†ฆ 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 โŠข ( ๐œ‘ โ†’ โˆซ ( ( ๐ด โˆ’ ๐‘‹ ) [,] ( ๐ต โˆ’ ๐‘‹ ) ) ( ๐น โ€˜ ๐‘ฅ ) d ๐‘ฅ = โˆซ ( ๐ด [,] ๐ต ) ( ๐น โ€˜ ๐‘ฅ ) d ๐‘ฅ )