Metamath Proof Explorer

Theorem fourierdlem86

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem86.f โŠข ( ๐œ‘ โ†’ ๐น : โ„ โŸถ โ„ )
fourierdlem86.xre โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„ )
fourierdlem86.p โŠข ๐‘ƒ = ( ๐‘š โˆˆ โ„• โ†ฆ { ๐‘ โˆˆ ( โ„ โ†‘m ( 0 ... ๐‘š ) ) โˆฃ ( ( ( ๐‘ โ€˜ 0 ) = ( - ฯ€ + ๐‘‹ ) โˆง ( ๐‘ โ€˜ ๐‘š ) = ( ฯ€ + ๐‘‹ ) ) โˆง โˆ€ ๐‘– โˆˆ ( 0 ..^ ๐‘š ) ( ๐‘ โ€˜ ๐‘– ) < ( ๐‘ โ€˜ ( ๐‘– + 1 ) ) ) } )
fourierdlem86.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
fourierdlem86.v โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ ( ๐‘ƒ โ€˜ ๐‘€ ) )
fourierdlem86.fcn โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ( ๐น โ†พ ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) ) โˆˆ ( ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) โ€“cnโ†’ โ„‚ ) )
fourierdlem86.r โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐‘… โˆˆ ( ( ๐น โ†พ ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘‰ โ€˜ ๐‘– ) ) )
fourierdlem86.l โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐ฟ โˆˆ ( ( ๐น โ†พ ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) )
fourierdlem86.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
fourierdlem86.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
fourierdlem86.altb โŠข ( ๐œ‘ โ†’ ๐ด < ๐ต )
fourierdlem86.ab โŠข ( ๐œ‘ โ†’ ( ๐ด [,] ๐ต ) โŠ† ( - ฯ€ [,] ฯ€ ) )
fourierdlem86.n0 โŠข ( ๐œ‘ โ†’ ยฌ 0 โˆˆ ( ๐ด [,] ๐ต ) )
fourierdlem86.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„ )
fourierdlem86.o โŠข ๐‘‚ = ( ๐‘  โˆˆ ( ๐ด [,] ๐ต ) โ†ฆ ( ( ( ( ๐น โ€˜ ( ๐‘‹ + ๐‘  ) ) โˆ’ ๐ถ ) / ๐‘  ) ยท ( ๐‘  / ( 2 ยท ( sin โ€˜ ( ๐‘  / 2 ) ) ) ) ) )
fourierdlem86.q โŠข ๐‘„ = ( ๐‘– โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ( ๐‘‰ โ€˜ ๐‘– ) โˆ’ ๐‘‹ ) )
fourierdlem86.t โŠข ๐‘‡ = ( { ๐ด , ๐ต } โˆช ( ran ๐‘„ โˆฉ ( ๐ด (,) ๐ต ) ) )
fourierdlem86.n โŠข ๐‘ = ( ( โ™ฏ โ€˜ ๐‘‡ ) โˆ’ 1 )
fourierdlem86.s โŠข ๐‘† = ( โ„ฉ ๐‘“ ๐‘“ Isom < , < ( ( 0 ... ๐‘ ) , ๐‘‡ ) )
fourierdlem86.d โŠข ๐ท = ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) )
fourierdlem86.e โŠข ๐ธ = ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) )
fourierdlem86.u โŠข ๐‘ˆ = ( โ„ฉ ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) )
Assertion fourierdlem86 ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ๐ท โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ๐ธ โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem86.f โŠข ( ๐œ‘ โ†’ ๐น : โ„ โŸถ โ„ )
2 fourierdlem86.xre โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„ )
3 fourierdlem86.p โŠข ๐‘ƒ = ( ๐‘š โˆˆ โ„• โ†ฆ { ๐‘ โˆˆ ( โ„ โ†‘m ( 0 ... ๐‘š ) ) โˆฃ ( ( ( ๐‘ โ€˜ 0 ) = ( - ฯ€ + ๐‘‹ ) โˆง ( ๐‘ โ€˜ ๐‘š ) = ( ฯ€ + ๐‘‹ ) ) โˆง โˆ€ ๐‘– โˆˆ ( 0 ..^ ๐‘š ) ( ๐‘ โ€˜ ๐‘– ) < ( ๐‘ โ€˜ ( ๐‘– + 1 ) ) ) } )
4 fourierdlem86.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
5 fourierdlem86.v โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ ( ๐‘ƒ โ€˜ ๐‘€ ) )
6 fourierdlem86.fcn โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ( ๐น โ†พ ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) ) โˆˆ ( ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) โ€“cnโ†’ โ„‚ ) )
7 fourierdlem86.r โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐‘… โˆˆ ( ( ๐น โ†พ ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘‰ โ€˜ ๐‘– ) ) )
8 fourierdlem86.l โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†’ ๐ฟ โˆˆ ( ( ๐น โ†พ ( ( ๐‘‰ โ€˜ ๐‘– ) (,) ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) ) limโ„‚ ( ๐‘‰ โ€˜ ( ๐‘– + 1 ) ) ) )
9 fourierdlem86.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
10 fourierdlem86.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
11 fourierdlem86.altb โŠข ( ๐œ‘ โ†’ ๐ด < ๐ต )
12 fourierdlem86.ab โŠข ( ๐œ‘ โ†’ ( ๐ด [,] ๐ต ) โŠ† ( - ฯ€ [,] ฯ€ ) )
13 fourierdlem86.n0 โŠข ( ๐œ‘ โ†’ ยฌ 0 โˆˆ ( ๐ด [,] ๐ต ) )
14 fourierdlem86.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„ )
15 fourierdlem86.o โŠข ๐‘‚ = ( ๐‘  โˆˆ ( ๐ด [,] ๐ต ) โ†ฆ ( ( ( ( ๐น โ€˜ ( ๐‘‹ + ๐‘  ) ) โˆ’ ๐ถ ) / ๐‘  ) ยท ( ๐‘  / ( 2 ยท ( sin โ€˜ ( ๐‘  / 2 ) ) ) ) ) )
16 fourierdlem86.q โŠข ๐‘„ = ( ๐‘– โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ( ๐‘‰ โ€˜ ๐‘– ) โˆ’ ๐‘‹ ) )
17 fourierdlem86.t โŠข ๐‘‡ = ( { ๐ด , ๐ต } โˆช ( ran ๐‘„ โˆฉ ( ๐ด (,) ๐ต ) ) )
18 fourierdlem86.n โŠข ๐‘ = ( ( โ™ฏ โ€˜ ๐‘‡ ) โˆ’ 1 )
19 fourierdlem86.s โŠข ๐‘† = ( โ„ฉ ๐‘“ ๐‘“ Isom < , < ( ( 0 ... ๐‘ ) , ๐‘‡ ) )
20 fourierdlem86.d โŠข ๐ท = ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) )
21 fourierdlem86.e โŠข ๐ธ = ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) )
22 fourierdlem86.u โŠข ๐‘ˆ = ( โ„ฉ ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) )
23 2 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐‘‹ โˆˆ โ„ )
24 4 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐‘€ โˆˆ โ„• )
25 5 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐‘‰ โˆˆ ( ๐‘ƒ โ€˜ ๐‘€ ) )
26 9 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐ด โˆˆ โ„ )
27 10 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐ต โˆˆ โ„ )
28 11 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐ด < ๐ต )
29 12 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ๐ด [,] ๐ต ) โŠ† ( - ฯ€ [,] ฯ€ ) )
30 simpr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐‘— โˆˆ ( 0 ..^ ๐‘ ) )
31 biid โŠข ( ( ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โˆง ๐‘ฆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ฆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ฆ + 1 ) ) ) ) โ†” ( ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โˆง ๐‘ฆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ฆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ฆ + 1 ) ) ) ) )
32 23 3 24 25 26 27 28 29 16 17 18 19 30 22 31 fourierdlem50 โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) ) )
33 32 simpld โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) )
34 id โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) )
35 32 simprd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) )
36 34 33 35 jca31 โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) ) )
37 nfv โŠข โ„ฒ ๐‘– ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) )
38 nfv โŠข โ„ฒ ๐‘– ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) )
39 nfcsb1v โŠข โ„ฒ ๐‘– โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ
40 nfcv โŠข โ„ฒ ๐‘– ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) )
41 38 39 40 nfif โŠข โ„ฒ ๐‘– if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) )
42 nfcv โŠข โ„ฒ ๐‘– โˆ’
43 nfcv โŠข โ„ฒ ๐‘– ๐ถ
44 41 42 43 nfov โŠข โ„ฒ ๐‘– ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ )
45 nfcv โŠข โ„ฒ ๐‘– /
46 nfcv โŠข โ„ฒ ๐‘– ( ๐‘† โ€˜ ( ๐‘— + 1 ) )
47 44 45 46 nfov โŠข โ„ฒ ๐‘– ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) )
48 nfcv โŠข โ„ฒ ๐‘– ยท
49 nfcv โŠข โ„ฒ ๐‘– ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) )
50 47 48 49 nfov โŠข โ„ฒ ๐‘– ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) )
51 50 nfel1 โŠข โ„ฒ ๐‘– ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) )
52 nfv โŠข โ„ฒ ๐‘– ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ )
53 nfcsb1v โŠข โ„ฒ ๐‘– โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘…
54 nfcv โŠข โ„ฒ ๐‘– ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) )
55 52 53 54 nfif โŠข โ„ฒ ๐‘– if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) )
56 55 42 43 nfov โŠข โ„ฒ ๐‘– ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ )
57 nfcv โŠข โ„ฒ ๐‘– ( ๐‘† โ€˜ ๐‘— )
58 56 45 57 nfov โŠข โ„ฒ ๐‘– ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) )
59 nfcv โŠข โ„ฒ ๐‘– ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) )
60 58 48 59 nfov โŠข โ„ฒ ๐‘– ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) )
61 60 nfel1 โŠข โ„ฒ ๐‘– ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) )
62 51 61 nfan โŠข โ„ฒ ๐‘– ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) )
63 nfv โŠข โ„ฒ ๐‘– ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ )
64 62 63 nfan โŠข โ„ฒ ๐‘– ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) )
65 37 64 nfim โŠข โ„ฒ ๐‘– ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) ) โ†’ ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) )
66 eleq1 โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) โ†” ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) )
67 66 anbi2d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โ†” ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) ) )
68 fveq2 โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ๐‘„ โ€˜ ๐‘– ) = ( ๐‘„ โ€˜ ๐‘ˆ ) )
69 oveq1 โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ๐‘– + 1 ) = ( ๐‘ˆ + 1 ) )
70 69 fveq2d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) )
71 68 70 oveq12d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) = ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) )
72 71 sseq2d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) โ†” ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) ) )
73 67 72 anbi12d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โ†” ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) ) ) )
74 70 eqeq2d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) โ†” ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) )
75 csbeq1a โŠข ( ๐‘– = ๐‘ˆ โ†’ ๐ฟ = โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ )
76 74 75 ifbieq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) = if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) )
77 76 oveq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) = ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) )
78 77 oveq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) = ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) )
79 78 oveq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) = ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) )
80 79 eleq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ†” ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) )
81 68 eqeq2d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) โ†” ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) ) )
82 csbeq1a โŠข ( ๐‘– = ๐‘ˆ โ†’ ๐‘… = โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… )
83 81 82 ifbieq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) = if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) )
84 83 oveq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) = ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) )
85 84 oveq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) = ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) )
86 85 oveq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) = ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) )
87 86 eleq1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) โ†” ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) )
88 80 87 anbi12d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โ†” ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) ) )
89 88 anbi1d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) โ†” ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) ) )
90 73 89 imbi12d โŠข ( ๐‘– = ๐‘ˆ โ†’ ( ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โ†’ ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) ) โ†” ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) ) โ†’ ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) ) ) )
91 eqid โŠข ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) = ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) )
92 eqid โŠข ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) = ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) )
93 biid โŠข ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โ†” ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) )
94 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 91 92 93 fourierdlem76 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘– โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘– ) (,) ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) ) ) โ†’ ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘– + 1 ) ) , ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘– ) , ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) )
95 65 90 94 vtoclg1f โŠข ( ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) โ†’ ( ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โˆง ๐‘ˆ โˆˆ ( 0 ..^ ๐‘€ ) ) โˆง ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โŠ† ( ( ๐‘„ โ€˜ ๐‘ˆ ) (,) ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) ) ) โ†’ ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) ) )
96 33 36 95 sylc โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) )
97 96 simpld โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) )
98 97 simpld โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ( if ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) = ( ๐‘„ โ€˜ ( ๐‘ˆ + 1 ) ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐ฟ , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ยท ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) )
99 20 98 eqeltrid โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐ท โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) )
100 97 simprd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ( if ( ( ๐‘† โ€˜ ๐‘— ) = ( ๐‘„ โ€˜ ๐‘ˆ ) , โฆ‹ ๐‘ˆ / ๐‘– โฆŒ ๐‘… , ( ๐น โ€˜ ( ๐‘‹ + ( ๐‘† โ€˜ ๐‘— ) ) ) ) โˆ’ ๐ถ ) / ( ๐‘† โ€˜ ๐‘— ) ) ยท ( ( ๐‘† โ€˜ ๐‘— ) / ( 2 ยท ( sin โ€˜ ( ( ๐‘† โ€˜ ๐‘— ) / 2 ) ) ) ) ) โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) )
101 21 100 eqeltrid โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ๐ธ โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) )
102 96 simprd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) )
103 99 101 102 jca31 โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ( 0 ..^ ๐‘ ) ) โ†’ ( ( ๐ท โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โˆง ๐ธ โˆˆ ( ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) limโ„‚ ( ๐‘† โ€˜ ๐‘— ) ) ) โˆง ( ๐‘‚ โ†พ ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) ) โˆˆ ( ( ( ๐‘† โ€˜ ๐‘— ) (,) ( ๐‘† โ€˜ ( ๐‘— + 1 ) ) ) โ€“cnโ†’ โ„‚ ) ) )