MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvfsumlem4 Structured version   Visualization version   GIF version

Theorem dvfsumlem4 25416
Description: Lemma for dvfsumrlim 25418. (Contributed by Mario Carneiro, 18-May-2016.)
Hypotheses
Ref Expression
dvfsum.s ๐‘† = (๐‘‡(,)+โˆž)
dvfsum.z ๐‘ = (โ„คโ‰ฅโ€˜๐‘€)
dvfsum.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
dvfsum.d (๐œ‘ โ†’ ๐ท โˆˆ โ„)
dvfsum.md (๐œ‘ โ†’ ๐‘€ โ‰ค (๐ท + 1))
dvfsum.t (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„)
dvfsum.a ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘†) โ†’ ๐ด โˆˆ โ„)
dvfsum.b1 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘†) โ†’ ๐ต โˆˆ ๐‘‰)
dvfsum.b2 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ ๐ต โˆˆ โ„)
dvfsum.b3 (๐œ‘ โ†’ (โ„ D (๐‘ฅ โˆˆ ๐‘† โ†ฆ ๐ด)) = (๐‘ฅ โˆˆ ๐‘† โ†ฆ ๐ต))
dvfsum.c (๐‘ฅ = ๐‘˜ โ†’ ๐ต = ๐ถ)
dvfsum.u (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„*)
dvfsum.l ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐‘˜ โˆˆ ๐‘†) โˆง (๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘ˆ)) โ†’ ๐ถ โ‰ค ๐ต)
dvfsumlem4.g ๐บ = (๐‘ฅ โˆˆ ๐‘† โ†ฆ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด))
dvfsumlem4.0 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค ๐ต)
dvfsumlem4.1 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐‘†)
dvfsumlem4.2 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐‘†)
dvfsumlem4.3 (๐œ‘ โ†’ ๐ท โ‰ค ๐‘‹)
dvfsumlem4.4 (๐œ‘ โ†’ ๐‘‹ โ‰ค ๐‘Œ)
dvfsumlem4.5 (๐œ‘ โ†’ ๐‘Œ โ‰ค ๐‘ˆ)
Assertion
Ref Expression
dvfsumlem4 (๐œ‘ โ†’ (absโ€˜((๐บโ€˜๐‘Œ) โˆ’ (๐บโ€˜๐‘‹))) โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
Distinct variable groups:   ๐ต,๐‘˜   ๐‘ฅ,๐ถ   ๐‘ฅ,๐‘˜,๐ท   ๐œ‘,๐‘˜,๐‘ฅ   ๐‘†,๐‘˜,๐‘ฅ   ๐‘˜,๐‘€,๐‘ฅ   ๐‘ฅ,๐‘‡   ๐‘˜,๐‘Œ,๐‘ฅ   ๐‘ฅ,๐‘   ๐‘ˆ,๐‘˜,๐‘ฅ   ๐‘˜,๐‘‹,๐‘ฅ
Allowed substitution hints:   ๐ด(๐‘ฅ,๐‘˜)   ๐ต(๐‘ฅ)   ๐ถ(๐‘˜)   ๐‘‡(๐‘˜)   ๐บ(๐‘ฅ,๐‘˜)   ๐‘‰(๐‘ฅ,๐‘˜)   ๐‘(๐‘˜)

Proof of Theorem dvfsumlem4
Dummy variable ๐‘š is distinct from all other variables.
StepHypRef Expression
1 dvfsumlem4.2 . . . . 5 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐‘†)
2 fzfid 13887 . . . . . . 7 (๐œ‘ โ†’ (๐‘€...(โŒŠโ€˜๐‘Œ)) โˆˆ Fin)
3 dvfsum.b2 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ ๐ต โˆˆ โ„)
43ralrimiva 3140 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐‘ ๐ต โˆˆ โ„)
5 elfzuz 13446 . . . . . . . . 9 (๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ)) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
6 dvfsum.z . . . . . . . . 9 ๐‘ = (โ„คโ‰ฅโ€˜๐‘€)
75, 6eleqtrrdi 2845 . . . . . . . 8 (๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ)) โ†’ ๐‘˜ โˆˆ ๐‘)
8 dvfsum.c . . . . . . . . . 10 (๐‘ฅ = ๐‘˜ โ†’ ๐ต = ๐ถ)
98eleq1d 2819 . . . . . . . . 9 (๐‘ฅ = ๐‘˜ โ†’ (๐ต โˆˆ โ„ โ†” ๐ถ โˆˆ โ„))
109rspccva 3582 . . . . . . . 8 ((โˆ€๐‘ฅ โˆˆ ๐‘ ๐ต โˆˆ โ„ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ ๐ถ โˆˆ โ„)
114, 7, 10syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))) โ†’ ๐ถ โˆˆ โ„)
122, 11fsumrecl 15627 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆˆ โ„)
13 dvfsum.a . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘†) โ†’ ๐ด โˆˆ โ„)
1413ralrimiva 3140 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐‘† ๐ด โˆˆ โ„)
15 nfcsb1v 3884 . . . . . . . . 9 โ„ฒ๐‘ฅโฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด
1615nfel1 2920 . . . . . . . 8 โ„ฒ๐‘ฅโฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด โˆˆ โ„
17 csbeq1a 3873 . . . . . . . . 9 (๐‘ฅ = ๐‘Œ โ†’ ๐ด = โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)
1817eleq1d 2819 . . . . . . . 8 (๐‘ฅ = ๐‘Œ โ†’ (๐ด โˆˆ โ„ โ†” โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด โˆˆ โ„))
1916, 18rspc 3571 . . . . . . 7 (๐‘Œ โˆˆ ๐‘† โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘† ๐ด โˆˆ โ„ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด โˆˆ โ„))
201, 14, 19sylc 65 . . . . . 6 (๐œ‘ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด โˆˆ โ„)
2112, 20resubcld 11591 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆˆ โ„)
22 nfcv 2904 . . . . . 6 โ„ฒ๐‘ฅ๐‘Œ
23 nfcv 2904 . . . . . . 7 โ„ฒ๐‘ฅฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ
24 nfcv 2904 . . . . . . 7 โ„ฒ๐‘ฅ โˆ’
2523, 24, 15nfov 7391 . . . . . 6 โ„ฒ๐‘ฅ(ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)
26 fveq2 6846 . . . . . . . . 9 (๐‘ฅ = ๐‘Œ โ†’ (โŒŠโ€˜๐‘ฅ) = (โŒŠโ€˜๐‘Œ))
2726oveq2d 7377 . . . . . . . 8 (๐‘ฅ = ๐‘Œ โ†’ (๐‘€...(โŒŠโ€˜๐‘ฅ)) = (๐‘€...(โŒŠโ€˜๐‘Œ)))
2827sumeq1d 15594 . . . . . . 7 (๐‘ฅ = ๐‘Œ โ†’ ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ = ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ)
2928, 17oveq12d 7379 . . . . . 6 (๐‘ฅ = ๐‘Œ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด) = (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
30 dvfsumlem4.g . . . . . 6 ๐บ = (๐‘ฅ โˆˆ ๐‘† โ†ฆ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด))
3122, 25, 29, 30fvmptf 6973 . . . . 5 ((๐‘Œ โˆˆ ๐‘† โˆง (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆˆ โ„) โ†’ (๐บโ€˜๐‘Œ) = (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
321, 21, 31syl2anc 585 . . . 4 (๐œ‘ โ†’ (๐บโ€˜๐‘Œ) = (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
33 dvfsumlem4.1 . . . . 5 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐‘†)
34 fzfid 13887 . . . . . . 7 (๐œ‘ โ†’ (๐‘€...(โŒŠโ€˜๐‘‹)) โˆˆ Fin)
35 elfzuz 13446 . . . . . . . . 9 (๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹)) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
3635, 6eleqtrrdi 2845 . . . . . . . 8 (๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹)) โ†’ ๐‘˜ โˆˆ ๐‘)
374, 36, 10syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))) โ†’ ๐ถ โˆˆ โ„)
3834, 37fsumrecl 15627 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆˆ โ„)
39 nfcsb1v 3884 . . . . . . . . 9 โ„ฒ๐‘ฅโฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด
4039nfel1 2920 . . . . . . . 8 โ„ฒ๐‘ฅโฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โˆˆ โ„
41 csbeq1a 3873 . . . . . . . . 9 (๐‘ฅ = ๐‘‹ โ†’ ๐ด = โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)
4241eleq1d 2819 . . . . . . . 8 (๐‘ฅ = ๐‘‹ โ†’ (๐ด โˆˆ โ„ โ†” โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โˆˆ โ„))
4340, 42rspc 3571 . . . . . . 7 (๐‘‹ โˆˆ ๐‘† โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘† ๐ด โˆˆ โ„ โ†’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โˆˆ โ„))
4433, 14, 43sylc 65 . . . . . 6 (๐œ‘ โ†’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด โˆˆ โ„)
4538, 44resubcld 11591 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โˆˆ โ„)
46 nfcv 2904 . . . . . 6 โ„ฒ๐‘ฅ๐‘‹
47 nfcv 2904 . . . . . . 7 โ„ฒ๐‘ฅฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ
4847, 24, 39nfov 7391 . . . . . 6 โ„ฒ๐‘ฅ(ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)
49 fveq2 6846 . . . . . . . . 9 (๐‘ฅ = ๐‘‹ โ†’ (โŒŠโ€˜๐‘ฅ) = (โŒŠโ€˜๐‘‹))
5049oveq2d 7377 . . . . . . . 8 (๐‘ฅ = ๐‘‹ โ†’ (๐‘€...(โŒŠโ€˜๐‘ฅ)) = (๐‘€...(โŒŠโ€˜๐‘‹)))
5150sumeq1d 15594 . . . . . . 7 (๐‘ฅ = ๐‘‹ โ†’ ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ = ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ)
5251, 41oveq12d 7379 . . . . . 6 (๐‘ฅ = ๐‘‹ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด) = (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))
5346, 48, 52, 30fvmptf 6973 . . . . 5 ((๐‘‹ โˆˆ ๐‘† โˆง (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โˆˆ โ„) โ†’ (๐บโ€˜๐‘‹) = (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))
5433, 45, 53syl2anc 585 . . . 4 (๐œ‘ โ†’ (๐บโ€˜๐‘‹) = (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))
5532, 54oveq12d 7379 . . 3 (๐œ‘ โ†’ ((๐บโ€˜๐‘Œ) โˆ’ (๐บโ€˜๐‘‹)) = ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
5655fveq2d 6850 . 2 (๐œ‘ โ†’ (absโ€˜((๐บโ€˜๐‘Œ) โˆ’ (๐บโ€˜๐‘‹))) = (absโ€˜((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))))
57 dvfsum.s . . . . . . . . . . 11 ๐‘† = (๐‘‡(,)+โˆž)
58 ioossre 13334 . . . . . . . . . . 11 (๐‘‡(,)+โˆž) โŠ† โ„
5957, 58eqsstri 3982 . . . . . . . . . 10 ๐‘† โŠ† โ„
6059a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘† โŠ† โ„)
61 dvfsum.b1 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘†) โ†’ ๐ต โˆˆ ๐‘‰)
62 dvfsum.b3 . . . . . . . . 9 (๐œ‘ โ†’ (โ„ D (๐‘ฅ โˆˆ ๐‘† โ†ฆ ๐ด)) = (๐‘ฅ โˆˆ ๐‘† โ†ฆ ๐ต))
6360, 13, 61, 62dvmptrecl 25411 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘†) โ†’ ๐ต โˆˆ โ„)
6463ralrimiva 3140 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐‘† ๐ต โˆˆ โ„)
65 nfv 1918 . . . . . . . 8 โ„ฒ๐‘š ๐ต โˆˆ โ„
66 nfcsb1v 3884 . . . . . . . . 9 โ„ฒ๐‘ฅโฆ‹๐‘š / ๐‘ฅโฆŒ๐ต
6766nfel1 2920 . . . . . . . 8 โ„ฒ๐‘ฅโฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„
68 csbeq1a 3873 . . . . . . . . 9 (๐‘ฅ = ๐‘š โ†’ ๐ต = โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต)
6968eleq1d 2819 . . . . . . . 8 (๐‘ฅ = ๐‘š โ†’ (๐ต โˆˆ โ„ โ†” โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„))
7065, 67, 69cbvralw 3288 . . . . . . 7 (โˆ€๐‘ฅ โˆˆ ๐‘† ๐ต โˆˆ โ„ โ†” โˆ€๐‘š โˆˆ ๐‘† โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„)
7164, 70sylib 217 . . . . . 6 (๐œ‘ โ†’ โˆ€๐‘š โˆˆ ๐‘† โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„)
72 csbeq1 3862 . . . . . . . 8 (๐‘š = ๐‘‹ โ†’ โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต = โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
7372eleq1d 2819 . . . . . . 7 (๐‘š = ๐‘‹ โ†’ (โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„ โ†” โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต โˆˆ โ„))
7473rspcv 3579 . . . . . 6 (๐‘‹ โˆˆ ๐‘† โ†’ (โˆ€๐‘š โˆˆ ๐‘† โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„ โ†’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต โˆˆ โ„))
7533, 71, 74sylc 65 . . . . 5 (๐œ‘ โ†’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต โˆˆ โ„)
7645, 75resubcld 11591 . . . 4 (๐œ‘ โ†’ ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โˆˆ โ„)
7759, 33sselid 3946 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
78 reflcl 13710 . . . . . . . . 9 (๐‘‹ โˆˆ โ„ โ†’ (โŒŠโ€˜๐‘‹) โˆˆ โ„)
7977, 78syl 17 . . . . . . . 8 (๐œ‘ โ†’ (โŒŠโ€˜๐‘‹) โˆˆ โ„)
8077, 79resubcld 11591 . . . . . . 7 (๐œ‘ โ†’ (๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) โˆˆ โ„)
8180, 75remulcld 11193 . . . . . 6 (๐œ‘ โ†’ ((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โˆˆ โ„)
8281, 45readdcld 11192 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆˆ โ„)
8382, 75resubcld 11591 . . . 4 (๐œ‘ โ†’ ((((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โˆˆ โ„)
84 fracge0 13718 . . . . . . . 8 (๐‘‹ โˆˆ โ„ โ†’ 0 โ‰ค (๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)))
8577, 84syl 17 . . . . . . 7 (๐œ‘ โ†’ 0 โ‰ค (๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)))
86 dvfsumlem4.3 . . . . . . . . 9 (๐œ‘ โ†’ ๐ท โ‰ค ๐‘‹)
8777rexrd 11213 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„*)
8859, 1sselid 3946 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
8988rexrd 11213 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„*)
90 dvfsum.u . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„*)
91 dvfsumlem4.4 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‹ โ‰ค ๐‘Œ)
92 dvfsumlem4.5 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โ‰ค ๐‘ˆ)
9387, 89, 90, 91, 92xrletrd 13090 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ โ‰ค ๐‘ˆ)
9433, 86, 933jca 1129 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ))
95 simpr1 1195 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ)) โ†’ ๐‘‹ โˆˆ ๐‘†)
96 nfv 1918 . . . . . . . . . . 11 โ„ฒ๐‘ฅ(๐œ‘ โˆง (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ))
97 nfcv 2904 . . . . . . . . . . . 12 โ„ฒ๐‘ฅ0
98 nfcv 2904 . . . . . . . . . . . 12 โ„ฒ๐‘ฅ โ‰ค
99 nfcsb1v 3884 . . . . . . . . . . . 12 โ„ฒ๐‘ฅโฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต
10097, 98, 99nfbr 5156 . . . . . . . . . . 11 โ„ฒ๐‘ฅ0 โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต
10196, 100nfim 1900 . . . . . . . . . 10 โ„ฒ๐‘ฅ((๐œ‘ โˆง (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
102 eleq1 2822 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ โˆˆ ๐‘† โ†” ๐‘‹ โˆˆ ๐‘†))
103 breq2 5113 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘‹ โ†’ (๐ท โ‰ค ๐‘ฅ โ†” ๐ท โ‰ค ๐‘‹))
104 breq1 5112 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ โ‰ค ๐‘ˆ โ†” ๐‘‹ โ‰ค ๐‘ˆ))
105102, 103, 1043anbi123d 1437 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘‹ โ†’ ((๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ) โ†” (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ)))
106105anbi2d 630 . . . . . . . . . . 11 (๐‘ฅ = ๐‘‹ โ†’ ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ)) โ†” (๐œ‘ โˆง (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ))))
107 csbeq1a 3873 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘‹ โ†’ ๐ต = โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
108107breq2d 5121 . . . . . . . . . . 11 (๐‘ฅ = ๐‘‹ โ†’ (0 โ‰ค ๐ต โ†” 0 โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
109106, 108imbi12d 345 . . . . . . . . . 10 (๐‘ฅ = ๐‘‹ โ†’ (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค ๐ต) โ†” ((๐œ‘ โˆง (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)))
110 dvfsumlem4.0 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค ๐ต)
111101, 109, 110vtoclg1f 3526 . . . . . . . . 9 (๐‘‹ โˆˆ ๐‘† โ†’ ((๐œ‘ โˆง (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
11295, 111mpcom 38 . . . . . . . 8 ((๐œ‘ โˆง (๐‘‹ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘‹ โˆง ๐‘‹ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
11394, 112mpdan 686 . . . . . . 7 (๐œ‘ โ†’ 0 โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
11480, 75, 85, 113mulge0d 11740 . . . . . 6 (๐œ‘ โ†’ 0 โ‰ค ((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
11545, 81addge02d 11752 . . . . . 6 (๐œ‘ โ†’ (0 โ‰ค ((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ†” (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โ‰ค (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))))
116114, 115mpbid 231 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โ‰ค (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
11745, 82, 75, 116lesub1dd 11779 . . . 4 (๐œ‘ โ†’ ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค ((((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
118 reflcl 13710 . . . . . . . . . 10 (๐‘Œ โˆˆ โ„ โ†’ (โŒŠโ€˜๐‘Œ) โˆˆ โ„)
11988, 118syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (โŒŠโ€˜๐‘Œ) โˆˆ โ„)
12088, 119resubcld 11591 . . . . . . . 8 (๐œ‘ โ†’ (๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) โˆˆ โ„)
121 csbeq1 3862 . . . . . . . . . . 11 (๐‘š = ๐‘Œ โ†’ โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต = โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
122121eleq1d 2819 . . . . . . . . . 10 (๐‘š = ๐‘Œ โ†’ (โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„ โ†” โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆˆ โ„))
123122rspcv 3579 . . . . . . . . 9 (๐‘Œ โˆˆ ๐‘† โ†’ (โˆ€๐‘š โˆˆ ๐‘† โฆ‹๐‘š / ๐‘ฅโฆŒ๐ต โˆˆ โ„ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆˆ โ„))
1241, 71, 123sylc 65 . . . . . . . 8 (๐œ‘ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆˆ โ„)
125120, 124remulcld 11193 . . . . . . 7 (๐œ‘ โ†’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โˆˆ โ„)
126125, 21readdcld 11192 . . . . . 6 (๐œ‘ โ†’ (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆˆ โ„)
127126, 124resubcld 11591 . . . . 5 (๐œ‘ โ†’ ((((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โˆˆ โ„)
128 dvfsum.m . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
129 dvfsum.d . . . . . . . 8 (๐œ‘ โ†’ ๐ท โˆˆ โ„)
130 dvfsum.md . . . . . . . 8 (๐œ‘ โ†’ ๐‘€ โ‰ค (๐ท + 1))
131 dvfsum.t . . . . . . . 8 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„)
132 dvfsum.l . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐‘˜ โˆˆ ๐‘†) โˆง (๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘ˆ)) โ†’ ๐ถ โ‰ค ๐ต)
133 eqid 2733 . . . . . . . 8 (๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด))) = (๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))
13457, 6, 128, 129, 130, 131, 13, 61, 3, 62, 8, 90, 132, 133, 33, 1, 86, 91, 92dvfsumlem3 25415 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘Œ) โ‰ค ((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘‹) โˆง (((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘‹) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค (((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘Œ) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)))
135134simprd 497 . . . . . 6 (๐œ‘ โ†’ (((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘‹) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค (((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘Œ) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
136 nfcv 2904 . . . . . . . . . . 11 โ„ฒ๐‘ฅ(๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹))
137 nfcv 2904 . . . . . . . . . . 11 โ„ฒ๐‘ฅ ยท
138136, 137, 99nfov 7391 . . . . . . . . . 10 โ„ฒ๐‘ฅ((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
139 nfcv 2904 . . . . . . . . . 10 โ„ฒ๐‘ฅ +
140138, 139, 48nfov 7391 . . . . . . . . 9 โ„ฒ๐‘ฅ(((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))
141 id 22 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘‹ โ†’ ๐‘ฅ = ๐‘‹)
142141, 49oveq12d 7379 . . . . . . . . . . 11 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) = (๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)))
143142, 107oveq12d 7379 . . . . . . . . . 10 (๐‘ฅ = ๐‘‹ โ†’ ((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) = ((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
144143, 52oveq12d 7379 . . . . . . . . 9 (๐‘ฅ = ๐‘‹ โ†’ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)) = (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
14546, 140, 144, 133fvmptf 6973 . . . . . . . 8 ((๐‘‹ โˆˆ ๐‘† โˆง (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆˆ โ„) โ†’ ((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘‹) = (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
14633, 82, 145syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘‹) = (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
147146oveq1d 7376 . . . . . 6 (๐œ‘ โ†’ (((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘‹) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) = ((((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
148 nfcv 2904 . . . . . . . . . . 11 โ„ฒ๐‘ฅ(๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ))
149 nfcsb1v 3884 . . . . . . . . . . 11 โ„ฒ๐‘ฅโฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต
150148, 137, 149nfov 7391 . . . . . . . . . 10 โ„ฒ๐‘ฅ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
151150, 139, 25nfov 7391 . . . . . . . . 9 โ„ฒ๐‘ฅ(((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
152 id 22 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘Œ โ†’ ๐‘ฅ = ๐‘Œ)
153152, 26oveq12d 7379 . . . . . . . . . . 11 (๐‘ฅ = ๐‘Œ โ†’ (๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) = (๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)))
154 csbeq1a 3873 . . . . . . . . . . 11 (๐‘ฅ = ๐‘Œ โ†’ ๐ต = โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
155153, 154oveq12d 7379 . . . . . . . . . 10 (๐‘ฅ = ๐‘Œ โ†’ ((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) = ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
156155, 29oveq12d 7379 . . . . . . . . 9 (๐‘ฅ = ๐‘Œ โ†’ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)) = (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)))
15722, 151, 156, 133fvmptf 6973 . . . . . . . 8 ((๐‘Œ โˆˆ ๐‘† โˆง (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆˆ โ„) โ†’ ((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘Œ) = (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)))
1581, 126, 157syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘Œ) = (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)))
159158oveq1d 7376 . . . . . 6 (๐œ‘ โ†’ (((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘Œ) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) = ((((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
160135, 147, 1593brtr3d 5140 . . . . 5 (๐œ‘ โ†’ ((((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค ((((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
16121recnd 11191 . . . . . . . 8 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆˆ โ„‚)
162124recnd 11191 . . . . . . . 8 (๐œ‘ โ†’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆˆ โ„‚)
163125recnd 11191 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โˆˆ โ„‚)
164161, 162, 163subsub3d 11550 . . . . . . 7 (๐œ‘ โ†’ ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))) = (((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) + ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
165161, 163addcomd 11365 . . . . . . . 8 (๐œ‘ โ†’ ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) + ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)) = (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)))
166165oveq1d 7376 . . . . . . 7 (๐œ‘ โ†’ (((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) + ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) = ((((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
167164, 166eqtrd 2773 . . . . . 6 (๐œ‘ โ†’ ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))) = ((((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
168 1red 11164 . . . . . . . . . 10 (๐œ‘ โ†’ 1 โˆˆ โ„)
169129, 77, 88, 86, 91letrd 11320 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ท โ‰ค ๐‘Œ)
1701, 169, 923jca 1129 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ))
171 simpr1 1195 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ)) โ†’ ๐‘Œ โˆˆ ๐‘†)
172 nfv 1918 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅ(๐œ‘ โˆง (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ))
17397, 98, 149nfbr 5156 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅ0 โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต
174172, 173nfim 1900 . . . . . . . . . . . . 13 โ„ฒ๐‘ฅ((๐œ‘ โˆง (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
175 eleq1 2822 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘Œ โ†’ (๐‘ฅ โˆˆ ๐‘† โ†” ๐‘Œ โˆˆ ๐‘†))
176 breq2 5113 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘Œ โ†’ (๐ท โ‰ค ๐‘ฅ โ†” ๐ท โ‰ค ๐‘Œ))
177 breq1 5112 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘Œ โ†’ (๐‘ฅ โ‰ค ๐‘ˆ โ†” ๐‘Œ โ‰ค ๐‘ˆ))
178175, 176, 1773anbi123d 1437 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘Œ โ†’ ((๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ) โ†” (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ)))
179178anbi2d 630 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘Œ โ†’ ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ)) โ†” (๐œ‘ โˆง (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ))))
180154breq2d 5121 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘Œ โ†’ (0 โ‰ค ๐ต โ†” 0 โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
181179, 180imbi12d 345 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘Œ โ†’ (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค ๐ต) โ†” ((๐œ‘ โˆง (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)))
182174, 181, 110vtoclg1f 3526 . . . . . . . . . . . 12 (๐‘Œ โˆˆ ๐‘† โ†’ ((๐œ‘ โˆง (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
183171, 182mpcom 38 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Œ โˆˆ ๐‘† โˆง ๐ท โ‰ค ๐‘Œ โˆง ๐‘Œ โ‰ค ๐‘ˆ)) โ†’ 0 โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
184170, 183mpdan 686 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
185 fracle1 13717 . . . . . . . . . . 11 (๐‘Œ โˆˆ โ„ โ†’ (๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) โ‰ค 1)
18688, 185syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) โ‰ค 1)
187120, 168, 124, 184, 186lemul1ad 12102 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โ‰ค (1 ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
188162mullidd 11181 . . . . . . . . 9 (๐œ‘ โ†’ (1 ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) = โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
189187, 188breqtrd 5135 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)
190124, 125subge0d 11753 . . . . . . . 8 (๐œ‘ โ†’ (0 โ‰ค (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)) โ†” ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โ‰ค โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
191189, 190mpbird 257 . . . . . . 7 (๐œ‘ โ†’ 0 โ‰ค (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)))
192124, 125resubcld 11591 . . . . . . . 8 (๐œ‘ โ†’ (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)) โˆˆ โ„)
19321, 192subge02d 11755 . . . . . . 7 (๐œ‘ โ†’ (0 โ‰ค (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต)) โ†” ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))) โ‰ค (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)))
194191, 193mpbid 231 . . . . . 6 (๐œ‘ โ†’ ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต โˆ’ ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))) โ‰ค (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
195167, 194eqbrtrrd 5133 . . . . 5 (๐œ‘ โ†’ ((((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โ‰ค (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
19683, 127, 21, 160, 195letrd 11320 . . . 4 (๐œ‘ โ†’ ((((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
19776, 83, 21, 117, 196letrd 11320 . . 3 (๐œ‘ โ†’ ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))
19875, 45readdcld 11192 . . . . 5 (๐œ‘ โ†’ (โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โˆˆ โ„)
199 fracge0 13718 . . . . . . . . 9 (๐‘Œ โˆˆ โ„ โ†’ 0 โ‰ค (๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)))
20088, 199syl 17 . . . . . . . 8 (๐œ‘ โ†’ 0 โ‰ค (๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)))
201120, 124, 200, 184mulge0d 11740 . . . . . . 7 (๐œ‘ โ†’ 0 โ‰ค ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต))
20221, 125addge02d 11752 . . . . . . 7 (๐œ‘ โ†’ (0 โ‰ค ((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) โ†” (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โ‰ค (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด))))
203201, 202mpbid 231 . . . . . 6 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โ‰ค (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)))
204134simpld 496 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘Œ) โ‰ค ((๐‘ฅ โˆˆ ๐‘† โ†ฆ (((๐‘ฅ โˆ’ (โŒŠโ€˜๐‘ฅ)) ยท ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘ฅ))๐ถ โˆ’ ๐ด)))โ€˜๐‘‹))
205204, 158, 1463brtr3d 5140 . . . . . 6 (๐œ‘ โ†’ (((๐‘Œ โˆ’ (โŒŠโ€˜๐‘Œ)) ยท โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด)) โ‰ค (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
20621, 126, 82, 203, 205letrd 11320 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โ‰ค (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
207 fracle1 13717 . . . . . . . . 9 (๐‘‹ โˆˆ โ„ โ†’ (๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) โ‰ค 1)
20877, 207syl 17 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) โ‰ค 1)
20980, 168, 75, 113, 208lemul1ad 12102 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค (1 ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
21075recnd 11191 . . . . . . . 8 (๐œ‘ โ†’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต โˆˆ โ„‚)
211210mullidd 11181 . . . . . . 7 (๐œ‘ โ†’ (1 ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) = โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
212209, 211breqtrd 5135 . . . . . 6 (๐œ‘ โ†’ ((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
21381, 75, 45, 212leadd1dd 11777 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ โˆ’ (โŒŠโ€˜๐‘‹)) ยท โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) โ‰ค (โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
21421, 82, 198, 206, 213letrd 11320 . . . 4 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โ‰ค (โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)))
21545recnd 11191 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โˆˆ โ„‚)
216210, 215addcomd 11365 . . . 4 (๐œ‘ โ†’ (โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต + (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด)) = ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) + โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
217214, 216breqtrd 5135 . . 3 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โ‰ค ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) + โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))
21821, 45, 75absdifled 15328 . . 3 (๐œ‘ โ†’ ((absโ€˜((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))) โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต โ†” (((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต) โ‰ค (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆง (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โ‰ค ((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด) + โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต))))
219197, 217, 218mpbir2and 712 . 2 (๐œ‘ โ†’ (absโ€˜((ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘Œ))๐ถ โˆ’ โฆ‹๐‘Œ / ๐‘ฅโฆŒ๐ด) โˆ’ (ฮฃ๐‘˜ โˆˆ (๐‘€...(โŒŠโ€˜๐‘‹))๐ถ โˆ’ โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ด))) โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
22056, 219eqbrtrd 5131 1 (๐œ‘ โ†’ (absโ€˜((๐บโ€˜๐‘Œ) โˆ’ (๐บโ€˜๐‘‹))) โ‰ค โฆ‹๐‘‹ / ๐‘ฅโฆŒ๐ต)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3061  โฆ‹csb 3859   โŠ† wss 3914   class class class wbr 5109   โ†ฆ cmpt 5192  โ€˜cfv 6500  (class class class)co 7361  โ„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   ยท cmul 11064  +โˆžcpnf 11194  โ„*cxr 11196   โ‰ค cle 11198   โˆ’ cmin 11393  โ„คcz 12507  โ„คโ‰ฅcuz 12771  (,)cioo 13273  ...cfz 13433  โŒŠcfl 13704  abscabs 15128  ฮฃcsu 15579   D cdv 25250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137  ax-addf 11138  ax-mulf 11139
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-om 7807  df-1st 7925  df-2nd 7926  df-supp 8097  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-er 8654  df-map 8773  df-pm 8774  df-ixp 8842  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fsupp 9312  df-fi 9355  df-sup 9386  df-inf 9387  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228  df-7 12229  df-8 12230  df-9 12231  df-n0 12422  df-z 12508  df-dec 12627  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-ioo 13277  df-ico 13279  df-icc 13280  df-fz 13434  df-fzo 13577  df-fl 13706  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-clim 15379  df-sum 15580  df-struct 17027  df-sets 17044  df-slot 17062  df-ndx 17074  df-base 17092  df-ress 17121  df-plusg 17154  df-mulr 17155  df-starv 17156  df-sca 17157  df-vsca 17158  df-ip 17159  df-tset 17160  df-ple 17161  df-ds 17163  df-unif 17164  df-hom 17165  df-cco 17166  df-rest 17312  df-topn 17313  df-0g 17331  df-gsum 17332  df-topgen 17333  df-pt 17334  df-prds 17337  df-xrs 17392  df-qtop 17397  df-imas 17398  df-xps 17400  df-mre 17474  df-mrc 17475  df-acs 17477  df-mgm 18505  df-sgrp 18554  df-mnd 18565  df-submnd 18610  df-mulg 18881  df-cntz 19105  df-cmn 19572  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-fbas 20816  df-fg 20817  df-cnfld 20820  df-top 22266  df-topon 22283  df-topsp 22305  df-bases 22319  df-cld 22393  df-ntr 22394  df-cls 22395  df-nei 22472  df-lp 22510  df-perf 22511  df-cn 22601  df-cnp 22602  df-haus 22689  df-cmp 22761  df-tx 22936  df-hmeo 23129  df-fil 23220  df-fm 23312  df-flim 23313  df-flf 23314  df-xms 23696  df-ms 23697  df-tms 23698  df-cncf 24264  df-limc 25253  df-dv 25254
This theorem is referenced by:  dvfsumrlim  25418  dvfsumrlim2  25419  logexprlim  26596
  Copyright terms: Public domain W3C validator