Metamath Proof Explorer


Theorem dvfsumabs

Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016)

Ref Expression
Hypotheses dvfsumabs.m โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) )
dvfsumabs.a โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
dvfsumabs.v โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ๐ต โˆˆ ๐‘‰ )
dvfsumabs.b โŠข ( ๐œ‘ โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐ต ) )
dvfsumabs.c โŠข ( ๐‘ฅ = ๐‘€ โ†’ ๐ด = ๐ถ )
dvfsumabs.d โŠข ( ๐‘ฅ = ๐‘ โ†’ ๐ด = ๐ท )
dvfsumabs.x โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘‹ โˆˆ โ„‚ )
dvfsumabs.y โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘Œ โˆˆ โ„ )
dvfsumabs.l โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) ) โ†’ ( abs โ€˜ ( ๐‘‹ โˆ’ ๐ต ) ) โ‰ค ๐‘Œ )
Assertion dvfsumabs ( ๐œ‘ โ†’ ( abs โ€˜ ( ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘‹ โˆ’ ( ๐ท โˆ’ ๐ถ ) ) ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘Œ )

Proof

Step Hyp Ref Expression
1 dvfsumabs.m โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) )
2 dvfsumabs.a โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
3 dvfsumabs.v โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ๐ต โˆˆ ๐‘‰ )
4 dvfsumabs.b โŠข ( ๐œ‘ โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐ต ) )
5 dvfsumabs.c โŠข ( ๐‘ฅ = ๐‘€ โ†’ ๐ด = ๐ถ )
6 dvfsumabs.d โŠข ( ๐‘ฅ = ๐‘ โ†’ ๐ด = ๐ท )
7 dvfsumabs.x โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘‹ โˆˆ โ„‚ )
8 dvfsumabs.y โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘Œ โˆˆ โ„ )
9 dvfsumabs.l โŠข ( ( ๐œ‘ โˆง ( ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) ) โ†’ ( abs โ€˜ ( ๐‘‹ โˆ’ ๐ต ) ) โ‰ค ๐‘Œ )
10 fzofi โŠข ( ๐‘€ ..^ ๐‘ ) โˆˆ Fin
11 10 a1i โŠข ( ๐œ‘ โ†’ ( ๐‘€ ..^ ๐‘ ) โˆˆ Fin )
12 eluzel2 โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) โ†’ ๐‘€ โˆˆ โ„ค )
13 1 12 syl โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค )
14 eluzelz โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) โ†’ ๐‘ โˆˆ โ„ค )
15 1 14 syl โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„ค )
16 fzval2 โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘€ ... ๐‘ ) = ( ( ๐‘€ [,] ๐‘ ) โˆฉ โ„ค ) )
17 13 15 16 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘€ ... ๐‘ ) = ( ( ๐‘€ [,] ๐‘ ) โˆฉ โ„ค ) )
18 inss1 โŠข ( ( ๐‘€ [,] ๐‘ ) โˆฉ โ„ค ) โŠ† ( ๐‘€ [,] ๐‘ )
19 17 18 eqsstrdi โŠข ( ๐œ‘ โ†’ ( ๐‘€ ... ๐‘ ) โŠ† ( ๐‘€ [,] ๐‘ ) )
20 19 sselda โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ( ๐‘€ ... ๐‘ ) ) โ†’ ๐‘ฆ โˆˆ ( ๐‘€ [,] ๐‘ ) )
21 cncff โŠข ( ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) : ( ๐‘€ [,] ๐‘ ) โŸถ โ„‚ )
22 2 21 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) : ( ๐‘€ [,] ๐‘ ) โŸถ โ„‚ )
23 eqid โŠข ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) = ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด )
24 23 fmpt โŠข ( โˆ€ ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ๐ด โˆˆ โ„‚ โ†” ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) : ( ๐‘€ [,] ๐‘ ) โŸถ โ„‚ )
25 22 24 sylibr โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ๐ด โˆˆ โ„‚ )
26 nfcsb1v โŠข โ„ฒ ๐‘ฅ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด
27 26 nfel1 โŠข โ„ฒ ๐‘ฅ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚
28 csbeq1a โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ๐ด = โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด )
29 28 eleq1d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐ด โˆˆ โ„‚ โ†” โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ ) )
30 27 29 rspc โŠข ( ๐‘ฆ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ๐ด โˆˆ โ„‚ โ†’ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ ) )
31 25 30 mpan9 โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ( ๐‘€ [,] ๐‘ ) ) โ†’ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ )
32 20 31 syldan โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ( ๐‘€ ... ๐‘ ) ) โ†’ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ )
33 32 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฆ โˆˆ ( ๐‘€ ... ๐‘ ) โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ )
34 fzofzp1 โŠข ( ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) โ†’ ( ๐‘˜ + 1 ) โˆˆ ( ๐‘€ ... ๐‘ ) )
35 csbeq1 โŠข ( ๐‘ฆ = ( ๐‘˜ + 1 ) โ†’ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด = โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด )
36 35 eleq1d โŠข ( ๐‘ฆ = ( ๐‘˜ + 1 ) โ†’ ( โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ โ†” โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ ) )
37 36 rspccva โŠข ( ( โˆ€ ๐‘ฆ โˆˆ ( ๐‘€ ... ๐‘ ) โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ โˆง ( ๐‘˜ + 1 ) โˆˆ ( ๐‘€ ... ๐‘ ) ) โ†’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ )
38 33 34 37 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ )
39 elfzofz โŠข ( ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) โ†’ ๐‘˜ โˆˆ ( ๐‘€ ... ๐‘ ) )
40 csbeq1 โŠข ( ๐‘ฆ = ๐‘˜ โ†’ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด = โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด )
41 40 eleq1d โŠข ( ๐‘ฆ = ๐‘˜ โ†’ ( โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ โ†” โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ ) )
42 41 rspccva โŠข ( ( โˆ€ ๐‘ฆ โˆˆ ( ๐‘€ ... ๐‘ ) โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ ( ๐‘€ ... ๐‘ ) ) โ†’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ )
43 33 39 42 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด โˆˆ โ„‚ )
44 38 43 subcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) โˆˆ โ„‚ )
45 11 7 44 fsumsub โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) = ( ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘‹ โˆ’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) )
46 vex โŠข ๐‘ฆ โˆˆ V
47 46 a1i โŠข ( ๐‘ฆ = ๐‘€ โ†’ ๐‘ฆ โˆˆ V )
48 eqeq2 โŠข ( ๐‘ฆ = ๐‘€ โ†’ ( ๐‘ฅ = ๐‘ฆ โ†” ๐‘ฅ = ๐‘€ ) )
49 48 biimpa โŠข ( ( ๐‘ฆ = ๐‘€ โˆง ๐‘ฅ = ๐‘ฆ ) โ†’ ๐‘ฅ = ๐‘€ )
50 49 5 syl โŠข ( ( ๐‘ฆ = ๐‘€ โˆง ๐‘ฅ = ๐‘ฆ ) โ†’ ๐ด = ๐ถ )
51 47 50 csbied โŠข ( ๐‘ฆ = ๐‘€ โ†’ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด = ๐ถ )
52 46 a1i โŠข ( ๐‘ฆ = ๐‘ โ†’ ๐‘ฆ โˆˆ V )
53 eqeq2 โŠข ( ๐‘ฆ = ๐‘ โ†’ ( ๐‘ฅ = ๐‘ฆ โ†” ๐‘ฅ = ๐‘ ) )
54 53 biimpa โŠข ( ( ๐‘ฆ = ๐‘ โˆง ๐‘ฅ = ๐‘ฆ ) โ†’ ๐‘ฅ = ๐‘ )
55 54 6 syl โŠข ( ( ๐‘ฆ = ๐‘ โˆง ๐‘ฅ = ๐‘ฆ ) โ†’ ๐ด = ๐ท )
56 52 55 csbied โŠข ( ๐‘ฆ = ๐‘ โ†’ โฆ‹ ๐‘ฆ / ๐‘ฅ โฆŒ ๐ด = ๐ท )
57 40 35 51 56 1 32 telfsumo2 โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) = ( ๐ท โˆ’ ๐ถ ) )
58 57 oveq2d โŠข ( ๐œ‘ โ†’ ( ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘‹ โˆ’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) = ( ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘‹ โˆ’ ( ๐ท โˆ’ ๐ถ ) ) )
59 45 58 eqtrd โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) = ( ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘‹ โˆ’ ( ๐ท โˆ’ ๐ถ ) ) )
60 59 fveq2d โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) = ( abs โ€˜ ( ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘‹ โˆ’ ( ๐ท โˆ’ ๐ถ ) ) ) )
61 7 44 subcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) โˆˆ โ„‚ )
62 11 61 fsumcl โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) โˆˆ โ„‚ )
63 62 abscld โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) โˆˆ โ„ )
64 61 abscld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( abs โ€˜ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) โˆˆ โ„ )
65 11 64 fsumrecl โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( abs โ€˜ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) โˆˆ โ„ )
66 11 8 fsumrecl โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘Œ โˆˆ โ„ )
67 11 61 fsumabs โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( abs โ€˜ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) )
68 elfzoelz โŠข ( ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) โ†’ ๐‘˜ โˆˆ โ„ค )
69 68 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘˜ โˆˆ โ„ค )
70 69 zred โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘˜ โˆˆ โ„ )
71 70 rexrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘˜ โˆˆ โ„* )
72 peano2re โŠข ( ๐‘˜ โˆˆ โ„ โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„ )
73 70 72 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„ )
74 73 rexrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„* )
75 70 lep1d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘˜ โ‰ค ( ๐‘˜ + 1 ) )
76 ubicc2 โŠข ( ( ๐‘˜ โˆˆ โ„* โˆง ( ๐‘˜ + 1 ) โˆˆ โ„* โˆง ๐‘˜ โ‰ค ( ๐‘˜ + 1 ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) )
77 71 74 75 76 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) )
78 lbicc2 โŠข ( ( ๐‘˜ โˆˆ โ„* โˆง ( ๐‘˜ + 1 ) โˆˆ โ„* โˆง ๐‘˜ โ‰ค ( ๐‘˜ + 1 ) ) โ†’ ๐‘˜ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) )
79 71 74 75 78 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘˜ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) )
80 13 zred โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„ )
81 80 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘€ โˆˆ โ„ )
82 15 zred โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„ )
83 82 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘ โˆˆ โ„ )
84 elfzole1 โŠข ( ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) โ†’ ๐‘€ โ‰ค ๐‘˜ )
85 84 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘€ โ‰ค ๐‘˜ )
86 34 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ ( ๐‘€ ... ๐‘ ) )
87 elfzle2 โŠข ( ( ๐‘˜ + 1 ) โˆˆ ( ๐‘€ ... ๐‘ ) โ†’ ( ๐‘˜ + 1 ) โ‰ค ๐‘ )
88 86 87 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ + 1 ) โ‰ค ๐‘ )
89 iccss โŠข ( ( ( ๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ ) โˆง ( ๐‘€ โ‰ค ๐‘˜ โˆง ( ๐‘˜ + 1 ) โ‰ค ๐‘ ) ) โ†’ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ [,] ๐‘ ) )
90 81 83 85 88 89 syl22anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ [,] ๐‘ ) )
91 90 resmptd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ†พ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) = ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) )
92 eqid โŠข ( TopOpen โ€˜ โ„‚fld ) = ( TopOpen โ€˜ โ„‚fld )
93 92 subcn โŠข โˆ’ โˆˆ ( ( ( TopOpen โ€˜ โ„‚fld ) ร—t ( TopOpen โ€˜ โ„‚fld ) ) Cn ( TopOpen โ€˜ โ„‚fld ) )
94 93 a1i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ โˆ’ โˆˆ ( ( ( TopOpen โ€˜ โ„‚fld ) ร—t ( TopOpen โ€˜ โ„‚fld ) ) Cn ( TopOpen โ€˜ โ„‚fld ) ) )
95 iccssre โŠข ( ( ๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ ) โ†’ ( ๐‘€ [,] ๐‘ ) โŠ† โ„ )
96 80 82 95 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘€ [,] ๐‘ ) โŠ† โ„ )
97 96 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘€ [,] ๐‘ ) โŠ† โ„ )
98 ax-resscn โŠข โ„ โŠ† โ„‚
99 97 98 sstrdi โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘€ [,] ๐‘ ) โŠ† โ„‚ )
100 ssid โŠข โ„‚ โŠ† โ„‚
101 100 a1i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ โ„‚ โŠ† โ„‚ )
102 cncfmptc โŠข ( ( ๐‘‹ โˆˆ โ„‚ โˆง ( ๐‘€ [,] ๐‘ ) โŠ† โ„‚ โˆง โ„‚ โŠ† โ„‚ ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐‘‹ ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
103 7 99 101 102 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐‘‹ ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
104 cncfmptid โŠข ( ( ( ๐‘€ [,] ๐‘ ) โŠ† โ„‚ โˆง โ„‚ โŠ† โ„‚ ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐‘ฅ ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
105 99 100 104 sylancl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐‘ฅ ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
106 103 105 mulcncf โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ( ๐‘‹ ยท ๐‘ฅ ) ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
107 2 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ๐ด ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
108 92 94 106 107 cncfmpt2f โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) )
109 rescncf โŠข ( ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ [,] ๐‘ ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โˆˆ ( ( ๐‘€ [,] ๐‘ ) โ€“cnโ†’ โ„‚ ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ†พ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) โˆˆ ( ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ€“cnโ†’ โ„‚ ) ) )
110 90 108 109 sylc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ†พ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) โˆˆ ( ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ€“cnโ†’ โ„‚ ) )
111 91 110 eqeltrrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โˆˆ ( ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ€“cnโ†’ โ„‚ ) )
112 98 a1i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ โ„ โŠ† โ„‚ )
113 90 97 sstrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โŠ† โ„ )
114 90 sselda โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) โ†’ ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) )
115 7 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ) โ†’ ๐‘‹ โˆˆ โ„‚ )
116 99 sselda โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
117 115 116 mulcld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ) โ†’ ( ๐‘‹ ยท ๐‘ฅ ) โˆˆ โ„‚ )
118 25 r19.21bi โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ) โ†’ ๐ด โˆˆ โ„‚ )
119 118 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ) โ†’ ๐ด โˆˆ โ„‚ )
120 117 119 subcld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) ) โ†’ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) โˆˆ โ„‚ )
121 114 120 syldan โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) โ†’ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) โˆˆ โ„‚ )
122 92 tgioo2 โŠข ( topGen โ€˜ ran (,) ) = ( ( TopOpen โ€˜ โ„‚fld ) โ†พt โ„ )
123 iccntr โŠข ( ( ๐‘˜ โˆˆ โ„ โˆง ( ๐‘˜ + 1 ) โˆˆ โ„ ) โ†’ ( ( int โ€˜ ( topGen โ€˜ ran (,) ) ) โ€˜ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) = ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) )
124 70 73 123 syl2anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( int โ€˜ ( topGen โ€˜ ran (,) ) ) โ€˜ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) = ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) )
125 112 113 121 122 92 124 dvmptntr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) = ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) )
126 reelprrecn โŠข โ„ โˆˆ { โ„ , โ„‚ }
127 126 a1i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ โ„ โˆˆ { โ„ , โ„‚ } )
128 ioossicc โŠข ( ๐‘€ (,) ๐‘ ) โŠ† ( ๐‘€ [,] ๐‘ )
129 128 sseli โŠข ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†’ ๐‘ฅ โˆˆ ( ๐‘€ [,] ๐‘ ) )
130 129 120 sylan2 โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) โˆˆ โ„‚ )
131 ovex โŠข ( ๐‘‹ โˆ’ ๐ต ) โˆˆ V
132 131 a1i โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ( ๐‘‹ โˆ’ ๐ต ) โˆˆ V )
133 129 117 sylan2 โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ( ๐‘‹ ยท ๐‘ฅ ) โˆˆ โ„‚ )
134 7 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ๐‘‹ โˆˆ โ„‚ )
135 128 99 sstrid โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘€ (,) ๐‘ ) โŠ† โ„‚ )
136 135 sselda โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
137 1cnd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ 1 โˆˆ โ„‚ )
138 112 sselda โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ โ„ ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
139 1cnd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ โ„ ) โ†’ 1 โˆˆ โ„‚ )
140 127 dvmptid โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ โ„ โ†ฆ ๐‘ฅ ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ 1 ) )
141 128 97 sstrid โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘€ (,) ๐‘ ) โŠ† โ„ )
142 iooretop โŠข ( ๐‘€ (,) ๐‘ ) โˆˆ ( topGen โ€˜ ran (,) )
143 142 a1i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘€ (,) ๐‘ ) โˆˆ ( topGen โ€˜ ran (,) ) )
144 127 138 139 140 141 122 92 143 dvmptres โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐‘ฅ ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ 1 ) )
145 127 136 137 144 7 dvmptcmul โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ( ๐‘‹ ยท ๐‘ฅ ) ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ( ๐‘‹ ยท 1 ) ) )
146 7 mulid1d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘‹ ยท 1 ) = ๐‘‹ )
147 146 mpteq2dv โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ( ๐‘‹ ยท 1 ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐‘‹ ) )
148 145 147 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ( ๐‘‹ ยท ๐‘ฅ ) ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐‘‹ ) )
149 129 119 sylan2 โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ๐ด โˆˆ โ„‚ )
150 3 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) ) โ†’ ๐ต โˆˆ ๐‘‰ )
151 4 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐ด ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ๐ต ) )
152 127 133 134 148 149 150 151 dvmptsub โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) = ( ๐‘ฅ โˆˆ ( ๐‘€ (,) ๐‘ ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) )
153 81 rexrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘€ โˆˆ โ„* )
154 iooss1 โŠข ( ( ๐‘€ โˆˆ โ„* โˆง ๐‘€ โ‰ค ๐‘˜ ) โ†’ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ (,) ( ๐‘˜ + 1 ) ) )
155 153 85 154 syl2anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ (,) ( ๐‘˜ + 1 ) ) )
156 83 rexrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘ โˆˆ โ„* )
157 iooss2 โŠข ( ( ๐‘ โˆˆ โ„* โˆง ( ๐‘˜ + 1 ) โ‰ค ๐‘ ) โ†’ ( ๐‘€ (,) ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ (,) ๐‘ ) )
158 156 88 157 syl2anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘€ (,) ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ (,) ๐‘ ) )
159 155 158 sstrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โŠ† ( ๐‘€ (,) ๐‘ ) )
160 iooretop โŠข ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โˆˆ ( topGen โ€˜ ran (,) )
161 160 a1i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โˆˆ ( topGen โ€˜ ran (,) ) )
162 127 130 132 152 159 122 92 161 dvmptres โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) = ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) )
163 125 162 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) = ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) )
164 163 dmeqd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ dom ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) = dom ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) )
165 eqid โŠข ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) = ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) )
166 131 165 dmmpti โŠข dom ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) = ( ๐‘˜ (,) ( ๐‘˜ + 1 ) )
167 164 166 eqtrdi โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ dom ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) = ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) )
168 163 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) = ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) )
169 168 fveq1d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) โ€˜ ๐‘ฅ ) )
170 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) )
171 165 fvmpt2 โŠข ( ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โˆง ( ๐‘‹ โˆ’ ๐ต ) โˆˆ V ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) โ€˜ ๐‘ฅ ) = ( ๐‘‹ โˆ’ ๐ต ) )
172 170 131 171 sylancl โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†ฆ ( ๐‘‹ โˆ’ ๐ต ) ) โ€˜ ๐‘ฅ ) = ( ๐‘‹ โˆ’ ๐ต ) )
173 169 172 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) = ( ๐‘‹ โˆ’ ๐ต ) )
174 173 fveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) ) = ( abs โ€˜ ( ๐‘‹ โˆ’ ๐ต ) ) )
175 9 anassrs โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( abs โ€˜ ( ๐‘‹ โˆ’ ๐ต ) ) โ‰ค ๐‘Œ )
176 174 175 eqbrtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) ) โ‰ค ๐‘Œ )
177 176 ralrimiva โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) ) โ‰ค ๐‘Œ )
178 nfcv โŠข โ„ฒ ๐‘ฅ abs
179 nfcv โŠข โ„ฒ ๐‘ฅ โ„
180 nfcv โŠข โ„ฒ ๐‘ฅ D
181 nfmpt1 โŠข โ„ฒ ๐‘ฅ ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) )
182 179 180 181 nfov โŠข โ„ฒ ๐‘ฅ ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) )
183 nfcv โŠข โ„ฒ ๐‘ฅ ๐‘ฆ
184 182 183 nffv โŠข โ„ฒ ๐‘ฅ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฆ )
185 178 184 nffv โŠข โ„ฒ ๐‘ฅ ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฆ ) )
186 nfcv โŠข โ„ฒ ๐‘ฅ โ‰ค
187 nfcv โŠข โ„ฒ ๐‘ฅ ๐‘Œ
188 185 186 187 nfbr โŠข โ„ฒ ๐‘ฅ ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฆ ) ) โ‰ค ๐‘Œ
189 2fveq3 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) ) = ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฆ ) ) )
190 189 breq1d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) ) โ‰ค ๐‘Œ โ†” ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฆ ) ) โ‰ค ๐‘Œ ) )
191 188 190 rspc โŠข ( ๐‘ฆ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฅ ) ) โ‰ค ๐‘Œ โ†’ ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฆ ) ) โ‰ค ๐‘Œ ) )
192 177 191 mpan9 โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ๐‘ฆ โˆˆ ( ๐‘˜ (,) ( ๐‘˜ + 1 ) ) ) โ†’ ( abs โ€˜ ( ( โ„ D ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) ) โ€˜ ๐‘ฆ ) ) โ‰ค ๐‘Œ )
193 70 73 111 167 8 192 dvlip โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โˆง ( ( ๐‘˜ + 1 ) โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โˆง ๐‘˜ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) ) โ†’ ( abs โ€˜ ( ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) โˆ’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) ) ) โ‰ค ( ๐‘Œ ยท ( abs โ€˜ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) ) )
194 193 ex โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ( ๐‘˜ + 1 ) โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โˆง ๐‘˜ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) ) โ†’ ( abs โ€˜ ( ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) โˆ’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) ) ) โ‰ค ( ๐‘Œ ยท ( abs โ€˜ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) ) ) )
195 77 79 194 mp2and โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( abs โ€˜ ( ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) โˆ’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) ) ) โ‰ค ( ๐‘Œ ยท ( abs โ€˜ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) ) )
196 ovex โŠข ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด ) โˆˆ V
197 nfcv โŠข โ„ฒ ๐‘ฅ ( ๐‘˜ + 1 )
198 nfcv โŠข โ„ฒ ๐‘ฅ ( ๐‘‹ ยท ( ๐‘˜ + 1 ) )
199 nfcv โŠข โ„ฒ ๐‘ฅ โˆ’
200 nfcsb1v โŠข โ„ฒ ๐‘ฅ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด
201 198 199 200 nfov โŠข โ„ฒ ๐‘ฅ ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด )
202 oveq2 โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ( ๐‘‹ ยท ๐‘ฅ ) = ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) )
203 csbeq1a โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ๐ด = โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด )
204 202 203 oveq12d โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) = ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด ) )
205 eqid โŠข ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) = ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) )
206 197 201 204 205 fvmptf โŠข ( ( ( ๐‘˜ + 1 ) โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โˆง ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด ) โˆˆ V ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) = ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด ) )
207 77 196 206 sylancl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) = ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด ) )
208 70 recnd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘˜ โˆˆ โ„‚ )
209 7 208 mulcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘‹ ยท ๐‘˜ ) โˆˆ โ„‚ )
210 209 43 subcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) โˆˆ โ„‚ )
211 nfcv โŠข โ„ฒ ๐‘ฅ ๐‘˜
212 nfcv โŠข โ„ฒ ๐‘ฅ ( ๐‘‹ ยท ๐‘˜ )
213 nfcsb1v โŠข โ„ฒ ๐‘ฅ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด
214 212 199 213 nfov โŠข โ„ฒ ๐‘ฅ ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด )
215 oveq2 โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ๐‘‹ ยท ๐‘ฅ ) = ( ๐‘‹ ยท ๐‘˜ ) )
216 csbeq1a โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ๐ด = โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด )
217 215 216 oveq12d โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) = ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) )
218 211 214 217 205 fvmptf โŠข ( ( ๐‘˜ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โˆง ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) โˆˆ โ„‚ ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) = ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) )
219 79 210 218 syl2anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) = ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) )
220 207 219 oveq12d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) โˆ’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) ) = ( ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด ) โˆ’ ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) )
221 peano2cn โŠข ( ๐‘˜ โˆˆ โ„‚ โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„‚ )
222 208 221 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„‚ )
223 7 222 mulcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆˆ โ„‚ )
224 223 209 38 43 sub4d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ ( ๐‘‹ ยท ๐‘˜ ) ) โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) = ( ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด ) โˆ’ ( ( ๐‘‹ ยท ๐‘˜ ) โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) )
225 1cnd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ 1 โˆˆ โ„‚ )
226 208 225 pncan2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) = 1 )
227 226 oveq2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘‹ ยท ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) = ( ๐‘‹ ยท 1 ) )
228 7 222 208 subdid โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘‹ ยท ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) = ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ ( ๐‘‹ ยท ๐‘˜ ) ) )
229 227 228 146 3eqtr3d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ ( ๐‘‹ ยท ๐‘˜ ) ) = ๐‘‹ )
230 229 oveq1d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ( ( ๐‘‹ ยท ( ๐‘˜ + 1 ) ) โˆ’ ( ๐‘‹ ยท ๐‘˜ ) ) โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) = ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) )
231 220 224 230 3eqtr2rd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) = ( ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) โˆ’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) ) )
232 231 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( abs โ€˜ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) = ( abs โ€˜ ( ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ( ๐‘˜ + 1 ) ) โˆ’ ( ( ๐‘ฅ โˆˆ ( ๐‘˜ [,] ( ๐‘˜ + 1 ) ) โ†ฆ ( ( ๐‘‹ ยท ๐‘ฅ ) โˆ’ ๐ด ) ) โ€˜ ๐‘˜ ) ) ) )
233 226 fveq2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( abs โ€˜ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) = ( abs โ€˜ 1 ) )
234 abs1 โŠข ( abs โ€˜ 1 ) = 1
235 233 234 eqtrdi โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( abs โ€˜ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) = 1 )
236 235 oveq2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘Œ ยท ( abs โ€˜ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) ) = ( ๐‘Œ ยท 1 ) )
237 8 recnd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘Œ โˆˆ โ„‚ )
238 237 mulid1d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( ๐‘Œ ยท 1 ) = ๐‘Œ )
239 236 238 eqtr2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ๐‘Œ = ( ๐‘Œ ยท ( abs โ€˜ ( ( ๐‘˜ + 1 ) โˆ’ ๐‘˜ ) ) ) )
240 195 232 239 3brtr4d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ) โ†’ ( abs โ€˜ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) โ‰ค ๐‘Œ )
241 11 64 8 240 fsumle โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( abs โ€˜ ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘Œ )
242 63 65 66 67 241 letrd โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ( ๐‘‹ โˆ’ ( โฆ‹ ( ๐‘˜ + 1 ) / ๐‘ฅ โฆŒ ๐ด โˆ’ โฆ‹ ๐‘˜ / ๐‘ฅ โฆŒ ๐ด ) ) ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘Œ )
243 60 242 eqbrtrrd โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ( ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘‹ โˆ’ ( ๐ท โˆ’ ๐ถ ) ) ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( ๐‘€ ..^ ๐‘ ) ๐‘Œ )