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

Theorem mertenslem1 15827
Description: Lemma for mertens 15829. (Contributed by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
mertens.1 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘—) = ๐ด)
mertens.2 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐พโ€˜๐‘—) = (absโ€˜๐ด))
mertens.3 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ๐ด โˆˆ โ„‚)
mertens.4 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) = ๐ต)
mertens.5 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐ต โˆˆ โ„‚)
mertens.6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ปโ€˜๐‘˜) = ฮฃ๐‘— โˆˆ (0...๐‘˜)(๐ด ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))))
mertens.7 (๐œ‘ โ†’ seq0( + , ๐พ) โˆˆ dom โ‡ )
mertens.8 (๐œ‘ โ†’ seq0( + , ๐บ) โˆˆ dom โ‡ )
mertens.9 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
mertens.10 ๐‘‡ = {๐‘ง โˆฃ โˆƒ๐‘› โˆˆ (0...(๐‘  โˆ’ 1))๐‘ง = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜))}
mertens.11 (๐œ“ โ†” (๐‘  โˆˆ โ„• โˆง โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘ )(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
mertens.12 (๐œ‘ โ†’ (๐œ“ โˆง (๐‘ก โˆˆ โ„•0 โˆง โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ก)(๐พโ€˜๐‘š) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)))))
mertens.13 (๐œ‘ โ†’ (0 โ‰ค sup(๐‘‡, โ„, < ) โˆง (๐‘‡ โІ โ„ โˆง ๐‘‡ โ‰  โˆ… โˆง โˆƒ๐‘ง โˆˆ โ„ โˆ€๐‘ค โˆˆ ๐‘‡ ๐‘ค โ‰ค ๐‘ง)))
Assertion
Ref Expression
mertenslem1 (๐œ‘ โ†’ โˆƒ๐‘ฆ โˆˆ โ„•0 โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฆ)(absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ)
Distinct variable groups:   ๐‘—,๐‘š,๐‘›,๐‘ ,๐‘ก,๐‘ฆ,๐‘ง,๐ต   ๐‘—,๐‘˜,๐บ,๐‘š,๐‘›,๐‘ ,๐‘ฆ,๐‘ง   ๐œ‘,๐‘—,๐‘˜,๐‘š,๐‘ฆ,๐‘ง   ๐‘ก,๐‘˜,๐ด,๐‘š,๐‘›,๐‘ ,๐‘ฆ   ๐‘—,๐ธ,๐‘˜,๐‘š,๐‘›,๐‘ ,๐‘ก,๐‘ฆ,๐‘ง   ๐‘—,๐พ,๐‘˜,๐‘š,๐‘›,๐‘ ,๐‘ก,๐‘ฆ,๐‘ง   ๐‘—,๐น,๐‘š,๐‘›,๐‘ฆ   ๐œ“,๐‘—,๐‘˜,๐‘š,๐‘›,๐‘ก,๐‘ฆ,๐‘ง   ๐‘ค,๐‘—,๐‘‡,๐‘˜,๐‘š,๐‘›,๐‘ก,๐‘ฆ,๐‘ง   ๐‘˜,๐ป,๐‘š,๐‘ฆ
Allowed substitution hints:   ๐œ‘(๐‘ค,๐‘ก,๐‘›,๐‘ )   ๐œ“(๐‘ค,๐‘ )   ๐ด(๐‘ง,๐‘ค,๐‘—)   ๐ต(๐‘ค,๐‘˜)   ๐‘‡(๐‘ )   ๐ธ(๐‘ค)   ๐น(๐‘ง,๐‘ค,๐‘ก,๐‘˜,๐‘ )   ๐บ(๐‘ค,๐‘ก)   ๐ป(๐‘ง,๐‘ค,๐‘ก,๐‘—,๐‘›,๐‘ )   ๐พ(๐‘ค)

Proof of Theorem mertenslem1
StepHypRef Expression
1 mertens.12 . . . . . . 7 (๐œ‘ โ†’ (๐œ“ โˆง (๐‘ก โˆˆ โ„•0 โˆง โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ก)(๐พโ€˜๐‘š) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)))))
21simpld 494 . . . . . 6 (๐œ‘ โ†’ ๐œ“)
3 mertens.11 . . . . . 6 (๐œ“ โ†” (๐‘  โˆˆ โ„• โˆง โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘ )(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
42, 3sylib 217 . . . . 5 (๐œ‘ โ†’ (๐‘  โˆˆ โ„• โˆง โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘ )(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
54simpld 494 . . . 4 (๐œ‘ โ†’ ๐‘  โˆˆ โ„•)
65nnnn0d 12529 . . 3 (๐œ‘ โ†’ ๐‘  โˆˆ โ„•0)
71simprd 495 . . . 4 (๐œ‘ โ†’ (๐‘ก โˆˆ โ„•0 โˆง โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ก)(๐พโ€˜๐‘š) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1))))
87simpld 494 . . 3 (๐œ‘ โ†’ ๐‘ก โˆˆ โ„•0)
96, 8nn0addcld 12533 . 2 (๐œ‘ โ†’ (๐‘  + ๐‘ก) โˆˆ โ„•0)
10 fzfid 13935 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (0...๐‘š) โˆˆ Fin)
11 simpl 482 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐œ‘)
12 elfznn0 13591 . . . . . . . 8 (๐‘— โˆˆ (0...๐‘š) โ†’ ๐‘— โˆˆ โ„•0)
13 mertens.3 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ๐ด โˆˆ โ„‚)
1411, 12, 13syl2an 595 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ ๐ด โˆˆ โ„‚)
15 eqid 2724 . . . . . . . 8 (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1)) = (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))
16 fznn0sub 13530 . . . . . . . . . . 11 (๐‘— โˆˆ (0...๐‘š) โ†’ (๐‘š โˆ’ ๐‘—) โˆˆ โ„•0)
1716adantl 481 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ (๐‘š โˆ’ ๐‘—) โˆˆ โ„•0)
18 peano2nn0 12509 . . . . . . . . . 10 ((๐‘š โˆ’ ๐‘—) โˆˆ โ„•0 โ†’ ((๐‘š โˆ’ ๐‘—) + 1) โˆˆ โ„•0)
1917, 18syl 17 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ ((๐‘š โˆ’ ๐‘—) + 1) โˆˆ โ„•0)
2019nn0zd 12581 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ ((๐‘š โˆ’ ๐‘—) + 1) โˆˆ โ„ค)
21 simplll 772 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐œ‘)
22 eluznn0 12898 . . . . . . . . . 10 ((((๐‘š โˆ’ ๐‘—) + 1) โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐‘˜ โˆˆ โ„•0)
2319, 22sylan 579 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐‘˜ โˆˆ โ„•0)
24 mertens.4 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) = ๐ต)
2521, 23, 24syl2anc 583 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ (๐บโ€˜๐‘˜) = ๐ต)
26 mertens.5 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐ต โˆˆ โ„‚)
2721, 23, 26syl2anc 583 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐ต โˆˆ โ„‚)
28 mertens.8 . . . . . . . . . 10 (๐œ‘ โ†’ seq0( + , ๐บ) โˆˆ dom โ‡ )
2928ad2antrr 723 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ seq0( + , ๐บ) โˆˆ dom โ‡ )
30 nn0uz 12861 . . . . . . . . . 10 โ„•0 = (โ„คโ‰ฅโ€˜0)
31 simpll 764 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ ๐œ‘)
3224, 26eqeltrd 2825 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) โˆˆ โ„‚)
3331, 32sylan 579 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) โˆˆ โ„‚)
3430, 19, 33iserex 15600 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ (seq0( + , ๐บ) โˆˆ dom โ‡ โ†” seq((๐‘š โˆ’ ๐‘—) + 1)( + , ๐บ) โˆˆ dom โ‡ ))
3529, 34mpbid 231 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ seq((๐‘š โˆ’ ๐‘—) + 1)( + , ๐บ) โˆˆ dom โ‡ )
3615, 20, 25, 27, 35isumcl 15704 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต โˆˆ โ„‚)
3714, 36mulcld 11231 . . . . . 6 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ (๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„‚)
3810, 37fsumcl 15676 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„‚)
3938abscld 15380 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
4037abscld 15380 . . . . 5 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ (absโ€˜(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
4110, 40fsumrecl 15677 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘š)(absโ€˜(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
42 mertens.9 . . . . . 6 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
4342rpred 13013 . . . . 5 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
4443adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐ธ โˆˆ โ„)
4510, 37fsumabs 15744 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ฮฃ๐‘— โˆˆ (0...๐‘š)(absโ€˜(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)))
46 fzfid 13935 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (0...(๐‘š โˆ’ ๐‘ )) โˆˆ Fin)
476adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘  โˆˆ โ„•0)
4847nn0ge0d 12532 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ 0 โ‰ค ๐‘ )
49 eluzelz 12829 . . . . . . . . . . . . . . 15 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก)) โ†’ ๐‘š โˆˆ โ„ค)
5049adantl 481 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘š โˆˆ โ„ค)
5150zred 12663 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘š โˆˆ โ„)
5247nn0red 12530 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘  โˆˆ โ„)
5351, 52subge02d 11803 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (0 โ‰ค ๐‘  โ†” (๐‘š โˆ’ ๐‘ ) โ‰ค ๐‘š))
5448, 53mpbid 231 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) โ‰ค ๐‘š)
5547, 30eleqtrdi 2835 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘  โˆˆ (โ„คโ‰ฅโ€˜0))
565nnzd 12582 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘  โˆˆ โ„ค)
57 uzid 12834 . . . . . . . . . . . . . . . . . 18 (๐‘  โˆˆ โ„ค โ†’ ๐‘  โˆˆ (โ„คโ‰ฅโ€˜๐‘ ))
5856, 57syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘  โˆˆ (โ„คโ‰ฅโ€˜๐‘ ))
59 uzaddcl 12885 . . . . . . . . . . . . . . . . 17 ((๐‘  โˆˆ (โ„คโ‰ฅโ€˜๐‘ ) โˆง ๐‘ก โˆˆ โ„•0) โ†’ (๐‘  + ๐‘ก) โˆˆ (โ„คโ‰ฅโ€˜๐‘ ))
6058, 8, 59syl2anc 583 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘  + ๐‘ก) โˆˆ (โ„คโ‰ฅโ€˜๐‘ ))
61 eqid 2724 . . . . . . . . . . . . . . . . 17 (โ„คโ‰ฅโ€˜๐‘ ) = (โ„คโ‰ฅโ€˜๐‘ )
6261uztrn2 12838 . . . . . . . . . . . . . . . 16 (((๐‘  + ๐‘ก) โˆˆ (โ„คโ‰ฅโ€˜๐‘ ) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ ))
6360, 62sylan 579 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ ))
64 elfzuzb 13492 . . . . . . . . . . . . . . 15 (๐‘  โˆˆ (0...๐‘š) โ†” (๐‘  โˆˆ (โ„คโ‰ฅโ€˜0) โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ )))
6555, 63, 64sylanbrc 582 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘  โˆˆ (0...๐‘š))
66 fznn0sub2 13605 . . . . . . . . . . . . . 14 (๐‘  โˆˆ (0...๐‘š) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ (0...๐‘š))
6765, 66syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ (0...๐‘š))
68 elfzelz 13498 . . . . . . . . . . . . 13 ((๐‘š โˆ’ ๐‘ ) โˆˆ (0...๐‘š) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ โ„ค)
6967, 68syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ โ„ค)
70 eluz 12833 . . . . . . . . . . . 12 (((๐‘š โˆ’ ๐‘ ) โˆˆ โ„ค โˆง ๐‘š โˆˆ โ„ค) โ†’ (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘š โˆ’ ๐‘ )) โ†” (๐‘š โˆ’ ๐‘ ) โ‰ค ๐‘š))
7169, 50, 70syl2anc 583 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘š โˆ’ ๐‘ )) โ†” (๐‘š โˆ’ ๐‘ ) โ‰ค ๐‘š))
7254, 71mpbird 257 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘š โˆ’ ๐‘ )))
73 fzss2 13538 . . . . . . . . . 10 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘š โˆ’ ๐‘ )) โ†’ (0...(๐‘š โˆ’ ๐‘ )) โІ (0...๐‘š))
7472, 73syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (0...(๐‘š โˆ’ ๐‘ )) โІ (0...๐‘š))
7574sselda 3974 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘— โˆˆ (0...๐‘š))
7613abscld 15380 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„)
7711, 12, 76syl2an 595 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ (absโ€˜๐ด) โˆˆ โ„)
7836abscld 15380 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„)
7977, 78remulcld 11241 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
8075, 79syldan 590 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
8146, 80fsumrecl 15677 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
82 fzfid 13935 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š) โˆˆ Fin)
83 elfznn0 13591 . . . . . . . . . . . . 13 ((๐‘š โˆ’ ๐‘ ) โˆˆ (0...๐‘š) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ โ„•0)
8467, 83syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ โ„•0)
85 peano2nn0 12509 . . . . . . . . . . . 12 ((๐‘š โˆ’ ๐‘ ) โˆˆ โ„•0 โ†’ ((๐‘š โˆ’ ๐‘ ) + 1) โˆˆ โ„•0)
8684, 85syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐‘š โˆ’ ๐‘ ) + 1) โˆˆ โ„•0)
8786, 30eleqtrdi 2835 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐‘š โˆ’ ๐‘ ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0))
88 fzss1 13537 . . . . . . . . . 10 (((๐‘š โˆ’ ๐‘ ) + 1) โˆˆ (โ„คโ‰ฅโ€˜0) โ†’ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š) โІ (0...๐‘š))
8987, 88syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š) โІ (0...๐‘š))
9089sselda 3974 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ๐‘— โˆˆ (0...๐‘š))
9190, 79syldan 590 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
9282, 91fsumrecl 15677 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„)
9342rphalfcld 13025 . . . . . . . 8 (๐œ‘ โ†’ (๐ธ / 2) โˆˆ โ„+)
9493rpred 13013 . . . . . . 7 (๐œ‘ โ†’ (๐ธ / 2) โˆˆ โ„)
9594adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐ธ / 2) โˆˆ โ„)
96 elfznn0 13591 . . . . . . . . . . 11 (๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ )) โ†’ ๐‘— โˆˆ โ„•0)
9711, 96, 76syl2an 595 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (absโ€˜๐ด) โˆˆ โ„)
9846, 97fsumrecl 15677 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) โˆˆ โ„)
9998, 95remulcld 11241 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) โˆˆ โ„)
100 0zd 12567 . . . . . . . . . . 11 (๐œ‘ โ†’ 0 โˆˆ โ„ค)
101 eqidd 2725 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐พโ€˜๐‘—) = (๐พโ€˜๐‘—))
102 mertens.2 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐พโ€˜๐‘—) = (absโ€˜๐ด))
103102, 76eqeltrd 2825 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐พโ€˜๐‘—) โˆˆ โ„)
104 mertens.7 . . . . . . . . . . 11 (๐œ‘ โ†’ seq0( + , ๐พ) โˆˆ dom โ‡ )
10530, 100, 101, 103, 104isumrecl 15708 . . . . . . . . . 10 (๐œ‘ โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) โˆˆ โ„)
10613absge0d 15388 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ 0 โ‰ค (absโ€˜๐ด))
107106, 102breqtrrd 5166 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ 0 โ‰ค (๐พโ€˜๐‘—))
10830, 100, 101, 103, 104, 107isumge0 15709 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โ‰ค ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—))
109105, 108ge0p1rpd 13043 . . . . . . . . 9 (๐œ‘ โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„+)
110109adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„+)
11199, 110rerpdivcld 13044 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) โˆˆ โ„)
11293, 109rpdivcld 13030 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) โˆˆ โ„+)
113112rpred 13013 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) โˆˆ โ„)
114113ad2antrr 723 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) โˆˆ โ„)
11597, 114remulcld 11241 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))) โˆˆ โ„)
11675, 20syldan 590 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((๐‘š โˆ’ ๐‘—) + 1) โˆˆ โ„ค)
117 simplll 772 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐œ‘)
11875, 19syldan 590 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((๐‘š โˆ’ ๐‘—) + 1) โˆˆ โ„•0)
119118, 22sylan 579 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐‘˜ โˆˆ โ„•0)
120117, 119, 24syl2anc 583 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ (๐บโ€˜๐‘˜) = ๐ต)
121117, 119, 26syl2anc 583 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐ต โˆˆ โ„‚)
12275, 35syldan 590 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ seq((๐‘š โˆ’ ๐‘—) + 1)( + , ๐บ) โˆˆ dom โ‡ )
12315, 116, 120, 121, 122isumcl 15704 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต โˆˆ โ„‚)
124123abscld 15380 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„)
12576, 106jca 511 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด) โˆˆ โ„ โˆง 0 โ‰ค (absโ€˜๐ด)))
12611, 96, 125syl2an 595 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((absโ€˜๐ด) โˆˆ โ„ โˆง 0 โ‰ค (absโ€˜๐ด)))
127120sumeq2dv 15646 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜) = ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)
128127fveq2d 6885 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜)) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต))
129 fvoveq1 7424 . . . . . . . . . . . . . . . 16 (๐‘› = (๐‘š โˆ’ ๐‘—) โ†’ (โ„คโ‰ฅโ€˜(๐‘› + 1)) = (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1)))
130129sumeq1d 15644 . . . . . . . . . . . . . . 15 (๐‘› = (๐‘š โˆ’ ๐‘—) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜) = ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜))
131130fveq2d 6885 . . . . . . . . . . . . . 14 (๐‘› = (๐‘š โˆ’ ๐‘—) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜)))
132131breq1d 5148 . . . . . . . . . . . . 13 (๐‘› = (๐‘š โˆ’ ๐‘—) โ†’ ((absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) โ†” (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
1334simprd 495 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘ )(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
134133ad2antrr 723 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘ )(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
135 elfzelz 13498 . . . . . . . . . . . . . . . . 17 (๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ )) โ†’ ๐‘— โˆˆ โ„ค)
136135adantl 481 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘— โˆˆ โ„ค)
137136zred 12663 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘— โˆˆ โ„)
13849ad2antlr 724 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘š โˆˆ โ„ค)
139138zred 12663 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘š โˆˆ โ„)
14056ad2antrr 723 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘  โˆˆ โ„ค)
141140zred 12663 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘  โˆˆ โ„)
142 elfzle2 13502 . . . . . . . . . . . . . . . 16 (๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ )) โ†’ ๐‘— โ‰ค (๐‘š โˆ’ ๐‘ ))
143142adantl 481 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘— โ‰ค (๐‘š โˆ’ ๐‘ ))
144137, 139, 141, 143lesubd 11815 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ๐‘  โ‰ค (๐‘š โˆ’ ๐‘—))
145138, 136zsubcld 12668 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (๐‘š โˆ’ ๐‘—) โˆˆ โ„ค)
146 eluz 12833 . . . . . . . . . . . . . . 15 ((๐‘  โˆˆ โ„ค โˆง (๐‘š โˆ’ ๐‘—) โˆˆ โ„ค) โ†’ ((๐‘š โˆ’ ๐‘—) โˆˆ (โ„คโ‰ฅโ€˜๐‘ ) โ†” ๐‘  โ‰ค (๐‘š โˆ’ ๐‘—)))
147140, 145, 146syl2anc 583 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((๐‘š โˆ’ ๐‘—) โˆˆ (โ„คโ‰ฅโ€˜๐‘ ) โ†” ๐‘  โ‰ค (๐‘š โˆ’ ๐‘—)))
148144, 147mpbird 257 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (๐‘š โˆ’ ๐‘—) โˆˆ (โ„คโ‰ฅโ€˜๐‘ ))
149132, 134, 148rspcdva 3605 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜)) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
150128, 149eqbrtrrd 5162 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) < ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
151124, 114, 150ltled 11359 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ‰ค ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
152 lemul2a 12066 . . . . . . . . . 10 ((((absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„ โˆง ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) โˆˆ โ„ โˆง ((absโ€˜๐ด) โˆˆ โ„ โˆง 0 โ‰ค (absโ€˜๐ด))) โˆง (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ‰ค ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
153124, 114, 126, 151, 152syl31anc 1370 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
15446, 80, 115, 153fsumle 15742 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
15598recnd 11239 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) โˆˆ โ„‚)
15693rpcnd 13015 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ธ / 2) โˆˆ โ„‚)
157156adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐ธ / 2) โˆˆ โ„‚)
158 peano2re 11384 . . . . . . . . . . . . 13 (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) โˆˆ โ„ โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„)
159105, 158syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„)
160159recnd 11239 . . . . . . . . . . 11 (๐œ‘ โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„‚)
161160adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„‚)
162109rpne0d 13018 . . . . . . . . . . 11 (๐œ‘ โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โ‰  0)
163162adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โ‰  0)
164155, 157, 161, 163divassd 12022 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) = (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
165 fveq2 6881 . . . . . . . . . . . . . . . . 17 (๐‘› = ๐‘— โ†’ (๐พโ€˜๐‘›) = (๐พโ€˜๐‘—))
166165cbvsumv 15639 . . . . . . . . . . . . . . . 16 ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) = ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—)
167166oveq1i 7411 . . . . . . . . . . . . . . 15 (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1) = (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)
168167oveq2i 7412 . . . . . . . . . . . . . 14 ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1)) = ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))
169168, 112eqeltrid 2829 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1)) โˆˆ โ„+)
170169rpcnd 13015 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1)) โˆˆ โ„‚)
171170adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1)) โˆˆ โ„‚)
17276recnd 11239 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
17311, 96, 172syl2an 595 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
17446, 171, 173fsummulc1 15728 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1))) = ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1))))
175168oveq2i 7412 . . . . . . . . . 10 (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1))) = (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
176168oveq2i 7412 . . . . . . . . . . . 12 ((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1))) = ((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
177176a1i 11 . . . . . . . . . . 11 (๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ )) โ†’ ((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1))) = ((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
178177sumeq2i 15642 . . . . . . . . . 10 ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘› โˆˆ โ„•0 (๐พโ€˜๐‘›) + 1))) = ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
179174, 175, 1783eqtr3g 2787 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))) = ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
180164, 179eqtrd 2764 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) = ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท ((๐ธ / 2) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))))
181154, 180breqtrrd 5166 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
182105adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) โˆˆ โ„)
183159adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„)
184 0zd 12567 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ 0 โˆˆ โ„ค)
185 fz0ssnn0 13593 . . . . . . . . . . . . 13 (0...(๐‘š โˆ’ ๐‘ )) โІ โ„•0
186185a1i 11 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (0...(๐‘š โˆ’ ๐‘ )) โІ โ„•0)
187102adantlr 712 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐พโ€˜๐‘—) = (absโ€˜๐ด))
18876adantlr 712 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„)
189106adantlr 712 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ โ„•0) โ†’ 0 โ‰ค (absโ€˜๐ด))
190104adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ seq0( + , ๐พ) โˆˆ dom โ‡ )
19130, 184, 46, 186, 187, 188, 189, 190isumless 15788 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) โ‰ค ฮฃ๐‘— โˆˆ โ„•0 (absโ€˜๐ด))
192102sumeq2dv 15646 . . . . . . . . . . . 12 (๐œ‘ โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) = ฮฃ๐‘— โˆˆ โ„•0 (absโ€˜๐ด))
193192adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) = ฮฃ๐‘— โˆˆ โ„•0 (absโ€˜๐ด))
194191, 193breqtrrd 5166 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) โ‰ค ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—))
195105ltp1d 12141 . . . . . . . . . . 11 (๐œ‘ โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))
196195adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))
19798, 182, 183, 194, 196lelttrd 11369 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))
19893rpregt0d 13019 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ธ / 2) โˆˆ โ„ โˆง 0 < (๐ธ / 2)))
199198adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐ธ / 2) โˆˆ โ„ โˆง 0 < (๐ธ / 2)))
200 ltmul1 12061 . . . . . . . . . 10 ((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) โˆˆ โ„ โˆง (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„ โˆง ((๐ธ / 2) โˆˆ โ„ โˆง 0 < (๐ธ / 2))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โ†” (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) < ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) ยท (๐ธ / 2))))
20198, 183, 199, 200syl3anc 1368 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โ†” (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) < ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) ยท (๐ธ / 2))))
202197, 201mpbid 231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) < ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) ยท (๐ธ / 2)))
203109rpregt0d 13019 . . . . . . . . . 10 (๐œ‘ โ†’ ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„ โˆง 0 < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
204203adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„ โˆง 0 < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)))
205 ltdivmul 12086 . . . . . . . . 9 (((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) โˆˆ โ„ โˆง (๐ธ / 2) โˆˆ โ„ โˆง ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) โˆˆ โ„ โˆง 0 < (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1))) โ†’ (((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) < (๐ธ / 2) โ†” (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) < ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) ยท (๐ธ / 2))))
20699, 95, 204, 205syl3anc 1368 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) < (๐ธ / 2) โ†” (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) < ((ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1) ยท (๐ธ / 2))))
207202, 206mpbird 257 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))(absโ€˜๐ด) ยท (๐ธ / 2)) / (ฮฃ๐‘— โˆˆ โ„•0 (๐พโ€˜๐‘—) + 1)) < (๐ธ / 2))
20881, 111, 95, 181, 207lelttrd 11369 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < (๐ธ / 2))
209 mertens.13 . . . . . . . . . . . 12 (๐œ‘ โ†’ (0 โ‰ค sup(๐‘‡, โ„, < ) โˆง (๐‘‡ โІ โ„ โˆง ๐‘‡ โ‰  โˆ… โˆง โˆƒ๐‘ง โˆˆ โ„ โˆ€๐‘ค โˆˆ ๐‘‡ ๐‘ค โ‰ค ๐‘ง)))
210209simprd 495 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‡ โІ โ„ โˆง ๐‘‡ โ‰  โˆ… โˆง โˆƒ๐‘ง โˆˆ โ„ โˆ€๐‘ค โˆˆ ๐‘‡ ๐‘ค โ‰ค ๐‘ง))
211 suprcl 12171 . . . . . . . . . . 11 ((๐‘‡ โІ โ„ โˆง ๐‘‡ โ‰  โˆ… โˆง โˆƒ๐‘ง โˆˆ โ„ โˆ€๐‘ค โˆˆ ๐‘‡ ๐‘ค โ‰ค ๐‘ง) โ†’ sup(๐‘‡, โ„, < ) โˆˆ โ„)
212210, 211syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ sup(๐‘‡, โ„, < ) โˆˆ โ„)
21394, 212remulcld 11241 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) โˆˆ โ„)
214209simpld 494 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โ‰ค sup(๐‘‡, โ„, < ))
215212, 214ge0p1rpd 13043 . . . . . . . . 9 (๐œ‘ โ†’ (sup(๐‘‡, โ„, < ) + 1) โˆˆ โ„+)
216213, 215rerpdivcld 13044 . . . . . . . 8 (๐œ‘ โ†’ (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)) โˆˆ โ„)
217216adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)) โˆˆ โ„)
2185nnrpd 13011 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘  โˆˆ โ„+)
21993, 218rpdivcld 13030 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ธ / 2) / ๐‘ ) โˆˆ โ„+)
220219, 215rpdivcld 13030 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โˆˆ โ„+)
221220rpred 13013 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โˆˆ โ„)
222221, 212remulcld 11241 . . . . . . . . . 10 (๐œ‘ โ†’ ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) โˆˆ โ„)
223222ad2antrr 723 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) โˆˆ โ„)
224 simpll 764 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ๐œ‘)
22590, 12syl 17 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ๐‘— โˆˆ โ„•0)
226224, 225, 76syl2anc 583 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (absโ€˜๐ด) โˆˆ โ„)
227221ad2antrr 723 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โˆˆ โ„)
228224, 225, 102syl2anc 583 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐พโ€˜๐‘—) = (absโ€˜๐ด))
229 fveq2 6881 . . . . . . . . . . . . . 14 (๐‘š = ๐‘— โ†’ (๐พโ€˜๐‘š) = (๐พโ€˜๐‘—))
230229breq1d 5148 . . . . . . . . . . . . 13 (๐‘š = ๐‘— โ†’ ((๐พโ€˜๐‘š) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โ†” (๐พโ€˜๐‘—) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1))))
2317simprd 495 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ก)(๐พโ€˜๐‘š) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)))
232231ad2antrr 723 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ก)(๐พโ€˜๐‘š) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)))
233 elfzuz 13494 . . . . . . . . . . . . . 14 (๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘ ) + 1)))
234 eluzle 12832 . . . . . . . . . . . . . . . . . 18 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก)) โ†’ (๐‘  + ๐‘ก) โ‰ค ๐‘š)
235234adantl 481 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘  + ๐‘ก) โ‰ค ๐‘š)
2368nn0zd 12581 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐‘ก โˆˆ โ„ค)
237236adantr 480 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘ก โˆˆ โ„ค)
238237zred 12663 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘ก โˆˆ โ„)
23952, 238, 51leaddsub2d 11813 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐‘  + ๐‘ก) โ‰ค ๐‘š โ†” ๐‘ก โ‰ค (๐‘š โˆ’ ๐‘ )))
240235, 239mpbid 231 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘ก โ‰ค (๐‘š โˆ’ ๐‘ ))
241 eluz 12833 . . . . . . . . . . . . . . . . 17 ((๐‘ก โˆˆ โ„ค โˆง (๐‘š โˆ’ ๐‘ ) โˆˆ โ„ค) โ†’ ((๐‘š โˆ’ ๐‘ ) โˆˆ (โ„คโ‰ฅโ€˜๐‘ก) โ†” ๐‘ก โ‰ค (๐‘š โˆ’ ๐‘ )))
242237, 69, 241syl2anc 583 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐‘š โˆ’ ๐‘ ) โˆˆ (โ„คโ‰ฅโ€˜๐‘ก) โ†” ๐‘ก โ‰ค (๐‘š โˆ’ ๐‘ )))
243240, 242mpbird 257 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ (โ„คโ‰ฅโ€˜๐‘ก))
244 peano2uz 12882 . . . . . . . . . . . . . . 15 ((๐‘š โˆ’ ๐‘ ) โˆˆ (โ„คโ‰ฅโ€˜๐‘ก) โ†’ ((๐‘š โˆ’ ๐‘ ) + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘ก))
245243, 244syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐‘š โˆ’ ๐‘ ) + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘ก))
246 uztrn 12837 . . . . . . . . . . . . . 14 ((๐‘— โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘ ) + 1)) โˆง ((๐‘š โˆ’ ๐‘ ) + 1) โˆˆ (โ„คโ‰ฅโ€˜๐‘ก)) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘ก))
247233, 245, 246syl2anr 596 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘ก))
248230, 232, 247rspcdva 3605 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐พโ€˜๐‘—) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)))
249228, 248eqbrtrrd 5162 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (absโ€˜๐ด) < (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)))
250226, 227, 249ltled 11359 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (absโ€˜๐ด) โ‰ค (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)))
251210ad2antrr 723 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘‡ โІ โ„ โˆง ๐‘‡ โ‰  โˆ… โˆง โˆƒ๐‘ง โˆˆ โ„ โˆ€๐‘ค โˆˆ ๐‘‡ ๐‘ค โ‰ค ๐‘ง))
25251adantr 480 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ๐‘š โˆˆ โ„)
253 peano2zm 12602 . . . . . . . . . . . . . . . . . 18 (๐‘  โˆˆ โ„ค โ†’ (๐‘  โˆ’ 1) โˆˆ โ„ค)
25456, 253syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐‘  โˆ’ 1) โˆˆ โ„ค)
255254zred 12663 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘  โˆ’ 1) โˆˆ โ„)
256255ad2antrr 723 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘  โˆ’ 1) โˆˆ โ„)
257225nn0red 12530 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ๐‘— โˆˆ โ„)
25850zcnd 12664 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘š โˆˆ โ„‚)
25952recnd 11239 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘  โˆˆ โ„‚)
260 1cnd 11206 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ 1 โˆˆ โ„‚)
261258, 259, 260subsubd 11596 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ (๐‘  โˆ’ 1)) = ((๐‘š โˆ’ ๐‘ ) + 1))
262261adantr 480 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘š โˆ’ (๐‘  โˆ’ 1)) = ((๐‘š โˆ’ ๐‘ ) + 1))
263 elfzle1 13501 . . . . . . . . . . . . . . . . 17 (๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š) โ†’ ((๐‘š โˆ’ ๐‘ ) + 1) โ‰ค ๐‘—)
264263adantl 481 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((๐‘š โˆ’ ๐‘ ) + 1) โ‰ค ๐‘—)
265262, 264eqbrtrd 5160 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘š โˆ’ (๐‘  โˆ’ 1)) โ‰ค ๐‘—)
266252, 256, 257, 265subled 11814 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘š โˆ’ ๐‘—) โ‰ค (๐‘  โˆ’ 1))
26790, 16syl 17 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘š โˆ’ ๐‘—) โˆˆ โ„•0)
268267, 30eleqtrdi 2835 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘š โˆ’ ๐‘—) โˆˆ (โ„คโ‰ฅโ€˜0))
269254ad2antrr 723 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘  โˆ’ 1) โˆˆ โ„ค)
270 elfz5 13490 . . . . . . . . . . . . . . 15 (((๐‘š โˆ’ ๐‘—) โˆˆ (โ„คโ‰ฅโ€˜0) โˆง (๐‘  โˆ’ 1) โˆˆ โ„ค) โ†’ ((๐‘š โˆ’ ๐‘—) โˆˆ (0...(๐‘  โˆ’ 1)) โ†” (๐‘š โˆ’ ๐‘—) โ‰ค (๐‘  โˆ’ 1)))
271268, 269, 270syl2anc 583 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((๐‘š โˆ’ ๐‘—) โˆˆ (0...(๐‘  โˆ’ 1)) โ†” (๐‘š โˆ’ ๐‘—) โ‰ค (๐‘  โˆ’ 1)))
272266, 271mpbird 257 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (๐‘š โˆ’ ๐‘—) โˆˆ (0...(๐‘  โˆ’ 1)))
273 simplll 772 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐œ‘)
27490, 19syldan 590 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((๐‘š โˆ’ ๐‘—) + 1) โˆˆ โ„•0)
275274, 22sylan 579 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ ๐‘˜ โˆˆ โ„•0)
276273, 275, 24syl2anc 583 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))) โ†’ (๐บโ€˜๐‘˜) = ๐ต)
277276sumeq2dv 15646 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜) = ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)
278277eqcomd 2730 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต = ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜))
279278fveq2d 6885 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜)))
280131rspceeqv 3625 . . . . . . . . . . . . 13 (((๐‘š โˆ’ ๐‘—) โˆˆ (0...(๐‘  โˆ’ 1)) โˆง (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))(๐บโ€˜๐‘˜))) โ†’ โˆƒ๐‘› โˆˆ (0...(๐‘  โˆ’ 1))(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)))
281272, 279, 280syl2anc 583 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ โˆƒ๐‘› โˆˆ (0...(๐‘  โˆ’ 1))(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)))
282 fvex 6894 . . . . . . . . . . . . 13 (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ V
283 eqeq1 2728 . . . . . . . . . . . . . 14 (๐‘ง = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ†’ (๐‘ง = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) โ†” (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜))))
284283rexbidv 3170 . . . . . . . . . . . . 13 (๐‘ง = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ†’ (โˆƒ๐‘› โˆˆ (0...(๐‘  โˆ’ 1))๐‘ง = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)) โ†” โˆƒ๐‘› โˆˆ (0...(๐‘  โˆ’ 1))(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜))))
285 mertens.10 . . . . . . . . . . . . 13 ๐‘‡ = {๐‘ง โˆฃ โˆƒ๐‘› โˆˆ (0...(๐‘  โˆ’ 1))๐‘ง = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜))}
286282, 284, 285elab2 3664 . . . . . . . . . . . 12 ((absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ ๐‘‡ โ†” โˆƒ๐‘› โˆˆ (0...(๐‘  โˆ’ 1))(absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) = (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))(๐บโ€˜๐‘˜)))
287281, 286sylibr 233 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ ๐‘‡)
288 suprub 12172 . . . . . . . . . . 11 (((๐‘‡ โІ โ„ โˆง ๐‘‡ โ‰  โˆ… โˆง โˆƒ๐‘ง โˆˆ โ„ โˆ€๐‘ค โˆˆ ๐‘‡ ๐‘ค โ‰ค ๐‘ง) โˆง (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ ๐‘‡) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ‰ค sup(๐‘‡, โ„, < ))
289251, 287, 288syl2anc 583 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ‰ค sup(๐‘‡, โ„, < ))
290224, 225, 125syl2anc 583 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((absโ€˜๐ด) โˆˆ โ„ โˆง 0 โ‰ค (absโ€˜๐ด)))
29190, 78syldan 590 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„)
29236absge0d 15388 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ 0 โ‰ค (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต))
29390, 292syldan 590 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ 0 โ‰ค (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต))
294291, 293jca 511 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„ โˆง 0 โ‰ค (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)))
295212ad2antrr 723 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ sup(๐‘‡, โ„, < ) โˆˆ โ„)
296 lemul12a 12069 . . . . . . . . . . 11 (((((absโ€˜๐ด) โˆˆ โ„ โˆง 0 โ‰ค (absโ€˜๐ด)) โˆง (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โˆˆ โ„) โˆง (((absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โˆˆ โ„ โˆง 0 โ‰ค (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆง sup(๐‘‡, โ„, < ) โˆˆ โ„)) โ†’ (((absโ€˜๐ด) โ‰ค (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โˆง (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ‰ค sup(๐‘‡, โ„, < )) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))))
297290, 227, 294, 295, 296syl22anc 836 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ (((absโ€˜๐ด) โ‰ค (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โˆง (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต) โ‰ค sup(๐‘‡, โ„, < )) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))))
298250, 289, 297mp2and 696 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )))
29982, 91, 223, 298fsumle 15742 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )))
300222recnd 11239 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) โˆˆ โ„‚)
301300adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) โˆˆ โ„‚)
302 fsumconst 15733 . . . . . . . . . 10 (((((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š) โˆˆ Fin โˆง ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) โˆˆ โ„‚) โ†’ ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) = ((โ™ฏโ€˜(((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) ยท ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))))
30382, 301, 302syl2anc 583 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) = ((โ™ฏโ€˜(((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) ยท ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))))
304 1zzd 12590 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ 1 โˆˆ โ„ค)
30556adantr 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐‘  โˆˆ โ„ค)
306 fzen 13515 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง (๐‘š โˆ’ ๐‘ ) โˆˆ โ„ค) โ†’ (1...๐‘ ) โ‰ˆ ((1 + (๐‘š โˆ’ ๐‘ ))...(๐‘  + (๐‘š โˆ’ ๐‘ ))))
307304, 305, 69, 306syl3anc 1368 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (1...๐‘ ) โ‰ˆ ((1 + (๐‘š โˆ’ ๐‘ ))...(๐‘  + (๐‘š โˆ’ ๐‘ ))))
308 ax-1cn 11164 . . . . . . . . . . . . . . 15 1 โˆˆ โ„‚
30969zcnd 12664 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ โ„‚)
310 addcom 11397 . . . . . . . . . . . . . . 15 ((1 โˆˆ โ„‚ โˆง (๐‘š โˆ’ ๐‘ ) โˆˆ โ„‚) โ†’ (1 + (๐‘š โˆ’ ๐‘ )) = ((๐‘š โˆ’ ๐‘ ) + 1))
311308, 309, 310sylancr 586 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (1 + (๐‘š โˆ’ ๐‘ )) = ((๐‘š โˆ’ ๐‘ ) + 1))
312259, 258pncan3d 11571 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘  + (๐‘š โˆ’ ๐‘ )) = ๐‘š)
313311, 312oveq12d 7419 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((1 + (๐‘š โˆ’ ๐‘ ))...(๐‘  + (๐‘š โˆ’ ๐‘ ))) = (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š))
314307, 313breqtrd 5164 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (1...๐‘ ) โ‰ˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š))
315 fzfid 13935 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (1...๐‘ ) โˆˆ Fin)
316 hashen 14304 . . . . . . . . . . . . 13 (((1...๐‘ ) โˆˆ Fin โˆง (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š) โˆˆ Fin) โ†’ ((โ™ฏโ€˜(1...๐‘ )) = (โ™ฏโ€˜(((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†” (1...๐‘ ) โ‰ˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)))
317315, 82, 316syl2anc 583 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((โ™ฏโ€˜(1...๐‘ )) = (โ™ฏโ€˜(((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) โ†” (1...๐‘ ) โ‰ˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)))
318314, 317mpbird 257 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (โ™ฏโ€˜(1...๐‘ )) = (โ™ฏโ€˜(((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)))
319 hashfz1 14303 . . . . . . . . . . . 12 (๐‘  โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...๐‘ )) = ๐‘ )
32047, 319syl 17 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (โ™ฏโ€˜(1...๐‘ )) = ๐‘ )
321318, 320eqtr3d 2766 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (โ™ฏโ€˜(((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) = ๐‘ )
322321oveq1d 7416 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((โ™ฏโ€˜(((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) ยท ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))) = (๐‘  ยท ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))))
323212recnd 11239 . . . . . . . . . . . 12 (๐œ‘ โ†’ sup(๐‘‡, โ„, < ) โˆˆ โ„‚)
324215rpcnne0d 13022 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((sup(๐‘‡, โ„, < ) + 1) โˆˆ โ„‚ โˆง (sup(๐‘‡, โ„, < ) + 1) โ‰  0))
325 div23 11888 . . . . . . . . . . . 12 (((๐ธ / 2) โˆˆ โ„‚ โˆง sup(๐‘‡, โ„, < ) โˆˆ โ„‚ โˆง ((sup(๐‘‡, โ„, < ) + 1) โˆˆ โ„‚ โˆง (sup(๐‘‡, โ„, < ) + 1) โ‰  0)) โ†’ (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)) = (((๐ธ / 2) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )))
326156, 323, 324, 325syl3anc 1368 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)) = (((๐ธ / 2) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )))
32756zcnd 12664 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘  โˆˆ โ„‚)
328219rpcnd 13015 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ธ / 2) / ๐‘ ) โˆˆ โ„‚)
329 divass 11887 . . . . . . . . . . . . . 14 ((๐‘  โˆˆ โ„‚ โˆง ((๐ธ / 2) / ๐‘ ) โˆˆ โ„‚ โˆง ((sup(๐‘‡, โ„, < ) + 1) โˆˆ โ„‚ โˆง (sup(๐‘‡, โ„, < ) + 1) โ‰  0)) โ†’ ((๐‘  ยท ((๐ธ / 2) / ๐‘ )) / (sup(๐‘‡, โ„, < ) + 1)) = (๐‘  ยท (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1))))
330327, 328, 324, 329syl3anc 1368 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘  ยท ((๐ธ / 2) / ๐‘ )) / (sup(๐‘‡, โ„, < ) + 1)) = (๐‘  ยท (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1))))
3315nnne0d 12259 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘  โ‰  0)
332156, 327, 331divcan2d 11989 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘  ยท ((๐ธ / 2) / ๐‘ )) = (๐ธ / 2))
333332oveq1d 7416 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘  ยท ((๐ธ / 2) / ๐‘ )) / (sup(๐‘‡, โ„, < ) + 1)) = ((๐ธ / 2) / (sup(๐‘‡, โ„, < ) + 1)))
334330, 333eqtr3d 2766 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘  ยท (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1))) = ((๐ธ / 2) / (sup(๐‘‡, โ„, < ) + 1)))
335334oveq1d 7416 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘  ยท (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1))) ยท sup(๐‘‡, โ„, < )) = (((๐ธ / 2) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )))
336220rpcnd 13015 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) โˆˆ โ„‚)
337327, 336, 323mulassd 11234 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘  ยท (((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1))) ยท sup(๐‘‡, โ„, < )) = (๐‘  ยท ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))))
338326, 335, 3373eqtr2rd 2771 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘  ยท ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))) = (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)))
339338adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘  ยท ((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < ))) = (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)))
340303, 322, 3393eqtrd 2768 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((((๐ธ / 2) / ๐‘ ) / (sup(๐‘‡, โ„, < ) + 1)) ยท sup(๐‘‡, โ„, < )) = (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)))
341299, 340breqtrd 5164 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โ‰ค (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)))
342 peano2re 11384 . . . . . . . . . . 11 (sup(๐‘‡, โ„, < ) โˆˆ โ„ โ†’ (sup(๐‘‡, โ„, < ) + 1) โˆˆ โ„)
343212, 342syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (sup(๐‘‡, โ„, < ) + 1) โˆˆ โ„)
344212ltp1d 12141 . . . . . . . . . 10 (๐œ‘ โ†’ sup(๐‘‡, โ„, < ) < (sup(๐‘‡, โ„, < ) + 1))
345212, 343, 93, 344ltmul2dd 13069 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) < ((๐ธ / 2) ยท (sup(๐‘‡, โ„, < ) + 1)))
346213, 94, 215ltdivmul2d 13065 . . . . . . . . 9 (๐œ‘ โ†’ ((((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)) < (๐ธ / 2) โ†” ((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) < ((๐ธ / 2) ยท (sup(๐‘‡, โ„, < ) + 1))))
347345, 346mpbird 257 . . . . . . . 8 (๐œ‘ โ†’ (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)) < (๐ธ / 2))
348347adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (((๐ธ / 2) ยท sup(๐‘‡, โ„, < )) / (sup(๐‘‡, โ„, < ) + 1)) < (๐ธ / 2))
34992, 217, 95, 341, 348lelttrd 11369 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < (๐ธ / 2))
35081, 92, 95, 95, 208, 349lt2addd 11834 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) + ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต))) < ((๐ธ / 2) + (๐ธ / 2)))
35114, 36absmuld 15398 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ (absโ€˜(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) = ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)))
352351sumeq2dv 15646 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘š)(absโ€˜(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) = ฮฃ๐‘— โˆˆ (0...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)))
35369zred 12663 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) โˆˆ โ„)
354353ltp1d 12141 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (๐‘š โˆ’ ๐‘ ) < ((๐‘š โˆ’ ๐‘ ) + 1))
355 fzdisj 13525 . . . . . . . 8 ((๐‘š โˆ’ ๐‘ ) < ((๐‘š โˆ’ ๐‘ ) + 1) โ†’ ((0...(๐‘š โˆ’ ๐‘ )) โˆฉ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) = โˆ…)
356354, 355syl 17 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((0...(๐‘š โˆ’ ๐‘ )) โˆฉ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)) = โˆ…)
357 fzsplit 13524 . . . . . . . 8 ((๐‘š โˆ’ ๐‘ ) โˆˆ (0...๐‘š) โ†’ (0...๐‘š) = ((0...(๐‘š โˆ’ ๐‘ )) โˆช (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)))
35867, 357syl 17 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (0...๐‘š) = ((0...(๐‘š โˆ’ ๐‘ )) โˆช (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)))
35979recnd 11239 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โˆง ๐‘— โˆˆ (0...๐‘š)) โ†’ ((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) โˆˆ โ„‚)
360356, 358, 10, 359fsumsplit 15684 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) = (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) + ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต))))
361352, 360eqtr2d 2765 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (ฮฃ๐‘— โˆˆ (0...(๐‘š โˆ’ ๐‘ ))((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) + ฮฃ๐‘— โˆˆ (((๐‘š โˆ’ ๐‘ ) + 1)...๐‘š)((absโ€˜๐ด) ยท (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต))) = ฮฃ๐‘— โˆˆ (0...๐‘š)(absโ€˜(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)))
36242rpcnd 13015 . . . . . . 7 (๐œ‘ โ†’ ๐ธ โˆˆ โ„‚)
363362adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ๐ธ โˆˆ โ„‚)
3643632halvesd 12455 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ((๐ธ / 2) + (๐ธ / 2)) = ๐ธ)
365350, 361, 3643brtr3d 5169 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘š)(absโ€˜(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ)
36639, 41, 44, 45, 365lelttrd 11369 . . 3 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))) โ†’ (absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ)
367366ralrimiva 3138 . 2 (๐œ‘ โ†’ โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))(absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ)
368 fveq2 6881 . . . 4 (๐‘ฆ = (๐‘  + ๐‘ก) โ†’ (โ„คโ‰ฅโ€˜๐‘ฆ) = (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก)))
369368raleqdv 3317 . . 3 (๐‘ฆ = (๐‘  + ๐‘ก) โ†’ (โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฆ)(absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ โ†” โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))(absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ))
370369rspcev 3604 . 2 (((๐‘  + ๐‘ก) โˆˆ โ„•0 โˆง โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜(๐‘  + ๐‘ก))(absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ) โ†’ โˆƒ๐‘ฆ โˆˆ โ„•0 โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฆ)(absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ)
3719, 367, 370syl2anc 583 1 (๐œ‘ โ†’ โˆƒ๐‘ฆ โˆˆ โ„•0 โˆ€๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘ฆ)(absโ€˜ฮฃ๐‘— โˆˆ (0...๐‘š)(๐ด ยท ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜((๐‘š โˆ’ ๐‘—) + 1))๐ต)) < ๐ธ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  {cab 2701   โ‰  wne 2932  โˆ€wral 3053  โˆƒwrex 3062   โˆช cun 3938   โˆฉ cin 3939   โІ wss 3940  โˆ…c0 4314   class class class wbr 5138  dom cdm 5666  โ€˜cfv 6533  (class class class)co 7401   โ‰ˆ cen 8932  Fincfn 8935  supcsup 9431  โ„‚cc 11104  โ„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   ยท cmul 11111   < clt 11245   โ‰ค cle 11246   โˆ’ cmin 11441   / cdiv 11868  โ„•cn 12209  2c2 12264  โ„•0cn0 12469  โ„คcz 12555  โ„คโ‰ฅcuz 12819  โ„+crp 12971  ...cfz 13481  seqcseq 13963  โ™ฏchash 14287  abscabs 15178   โ‡ cli 15425  ฮฃcsu 15629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-ico 13327  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-rlim 15430  df-sum 15630
This theorem is referenced by:  mertenslem2  15828
  Copyright terms: Public domain W3C validator