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

Theorem eftlub 15998
Description: An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
eftl.1 ๐น = (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ดโ†‘๐‘›) / (!โ€˜๐‘›)))
eftl.2 ๐บ = (๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))
eftl.3 ๐ป = (๐‘› โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘›)))
eftl.4 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
eftl.5 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
eftl.6 (๐œ‘ โ†’ (absโ€˜๐ด) โ‰ค 1)
Assertion
Ref Expression
eftlub (๐œ‘ โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜)) โ‰ค (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))))
Distinct variable groups:   ๐‘˜,๐‘›,๐ด   ๐‘˜,๐น   ๐‘˜,๐บ   ๐‘˜,๐‘€,๐‘›   ๐œ‘,๐‘˜
Allowed substitution hints:   ๐œ‘(๐‘›)   ๐น(๐‘›)   ๐บ(๐‘›)   ๐ป(๐‘˜,๐‘›)

Proof of Theorem eftlub
Dummy variable ๐‘— is distinct from all other variables.
StepHypRef Expression
1 eftl.5 . . . 4 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
2 eftl.4 . . . . 5 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
32nnnn0d 12480 . . . 4 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0)
4 eftl.1 . . . . 5 ๐น = (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ดโ†‘๐‘›) / (!โ€˜๐‘›)))
54eftlcl 15996 . . . 4 ((๐ด โˆˆ โ„‚ โˆง ๐‘€ โˆˆ โ„•0) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜) โˆˆ โ„‚)
61, 3, 5syl2anc 585 . . 3 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜) โˆˆ โ„‚)
76abscld 15328 . 2 (๐œ‘ โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜)) โˆˆ โ„)
81abscld 15328 . . 3 (๐œ‘ โ†’ (absโ€˜๐ด) โˆˆ โ„)
9 eftl.2 . . . 4 ๐บ = (๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))
109reeftlcl 15997 . . 3 (((absโ€˜๐ด) โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„•0) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜) โˆˆ โ„)
118, 3, 10syl2anc 585 . 2 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜) โˆˆ โ„)
128, 3reexpcld 14075 . . 3 (๐œ‘ โ†’ ((absโ€˜๐ด)โ†‘๐‘€) โˆˆ โ„)
13 peano2nn0 12460 . . . . . 6 (๐‘€ โˆˆ โ„•0 โ†’ (๐‘€ + 1) โˆˆ โ„•0)
143, 13syl 17 . . . . 5 (๐œ‘ โ†’ (๐‘€ + 1) โˆˆ โ„•0)
1514nn0red 12481 . . . 4 (๐œ‘ โ†’ (๐‘€ + 1) โˆˆ โ„)
163faccld 14191 . . . . 5 (๐œ‘ โ†’ (!โ€˜๐‘€) โˆˆ โ„•)
1716, 2nnmulcld 12213 . . . 4 (๐œ‘ โ†’ ((!โ€˜๐‘€) ยท ๐‘€) โˆˆ โ„•)
1815, 17nndivred 12214 . . 3 (๐œ‘ โ†’ ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€)) โˆˆ โ„)
1912, 18remulcld 11192 . 2 (๐œ‘ โ†’ (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))) โˆˆ โ„)
20 eqid 2737 . . 3 (โ„คโ‰ฅโ€˜๐‘€) = (โ„คโ‰ฅโ€˜๐‘€)
212nnzd 12533 . . . 4 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
22 eqidd 2738 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘˜) = (๐นโ€˜๐‘˜))
23 eluznn0 12849 . . . . . 6 ((๐‘€ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„•0)
243, 23sylan 581 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘˜ โˆˆ โ„•0)
254eftval 15966 . . . . . . 7 (๐‘˜ โˆˆ โ„•0 โ†’ (๐นโ€˜๐‘˜) = ((๐ดโ†‘๐‘˜) / (!โ€˜๐‘˜)))
2625adantl 483 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘˜) = ((๐ดโ†‘๐‘˜) / (!โ€˜๐‘˜)))
27 eftcl 15963 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((๐ดโ†‘๐‘˜) / (!โ€˜๐‘˜)) โˆˆ โ„‚)
281, 27sylan 581 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((๐ดโ†‘๐‘˜) / (!โ€˜๐‘˜)) โˆˆ โ„‚)
2926, 28eqeltrd 2838 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
3024, 29syldan 592 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘˜) โˆˆ โ„‚)
314eftlcvg 15995 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐‘€ โˆˆ โ„•0) โ†’ seq๐‘€( + , ๐น) โˆˆ dom โ‡ )
321, 3, 31syl2anc 585 . . . 4 (๐œ‘ โ†’ seq๐‘€( + , ๐น) โˆˆ dom โ‡ )
3320, 21, 22, 30, 32isumclim2 15650 . . 3 (๐œ‘ โ†’ seq๐‘€( + , ๐น) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜))
34 eqidd 2738 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐บโ€˜๐‘˜) = (๐บโ€˜๐‘˜))
359eftval 15966 . . . . . . . 8 (๐‘˜ โˆˆ โ„•0 โ†’ (๐บโ€˜๐‘˜) = (((absโ€˜๐ด)โ†‘๐‘˜) / (!โ€˜๐‘˜)))
3635adantl 483 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) = (((absโ€˜๐ด)โ†‘๐‘˜) / (!โ€˜๐‘˜)))
37 reeftcl 15964 . . . . . . . 8 (((absโ€˜๐ด) โˆˆ โ„ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘๐‘˜) / (!โ€˜๐‘˜)) โˆˆ โ„)
388, 37sylan 581 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘๐‘˜) / (!โ€˜๐‘˜)) โˆˆ โ„)
3936, 38eqeltrd 2838 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) โˆˆ โ„)
4024, 39syldan 592 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐บโ€˜๐‘˜) โˆˆ โ„)
4140recnd 11190 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐บโ€˜๐‘˜) โˆˆ โ„‚)
428recnd 11190 . . . . 5 (๐œ‘ โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
439eftlcvg 15995 . . . . 5 (((absโ€˜๐ด) โˆˆ โ„‚ โˆง ๐‘€ โˆˆ โ„•0) โ†’ seq๐‘€( + , ๐บ) โˆˆ dom โ‡ )
4442, 3, 43syl2anc 585 . . . 4 (๐œ‘ โ†’ seq๐‘€( + , ๐บ) โˆˆ dom โ‡ )
4520, 21, 34, 41, 44isumclim2 15650 . . 3 (๐œ‘ โ†’ seq๐‘€( + , ๐บ) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜))
46 eftabs 15965 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜((๐ดโ†‘๐‘˜) / (!โ€˜๐‘˜))) = (((absโ€˜๐ด)โ†‘๐‘˜) / (!โ€˜๐‘˜)))
471, 46sylan 581 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜((๐ดโ†‘๐‘˜) / (!โ€˜๐‘˜))) = (((absโ€˜๐ด)โ†‘๐‘˜) / (!โ€˜๐‘˜)))
4826fveq2d 6851 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (absโ€˜(๐นโ€˜๐‘˜)) = (absโ€˜((๐ดโ†‘๐‘˜) / (!โ€˜๐‘˜))))
4947, 48, 363eqtr4rd 2788 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) = (absโ€˜(๐นโ€˜๐‘˜)))
5024, 49syldan 592 . . 3 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐บโ€˜๐‘˜) = (absโ€˜(๐นโ€˜๐‘˜)))
5120, 33, 45, 21, 30, 50iserabs 15707 . 2 (๐œ‘ โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜)) โ‰ค ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜))
52 nn0uz 12812 . . . 4 โ„•0 = (โ„คโ‰ฅโ€˜0)
53 0zd 12518 . . . 4 (๐œ‘ โ†’ 0 โˆˆ โ„ค)
542nncnd 12176 . . . . 5 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
55 nn0cn 12430 . . . . 5 (๐‘— โˆˆ โ„•0 โ†’ ๐‘— โˆˆ โ„‚)
56 nn0ex 12426 . . . . . . . 8 โ„•0 โˆˆ V
5756mptex 7178 . . . . . . 7 (๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›))) โˆˆ V
589, 57eqeltri 2834 . . . . . 6 ๐บ โˆˆ V
5958shftval4 14969 . . . . 5 ((๐‘€ โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„‚) โ†’ ((๐บ shift -๐‘€)โ€˜๐‘—) = (๐บโ€˜(๐‘€ + ๐‘—)))
6054, 55, 59syl2an 597 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐บ shift -๐‘€)โ€˜๐‘—) = (๐บโ€˜(๐‘€ + ๐‘—)))
61 nn0addcl 12455 . . . . . . 7 ((๐‘€ โˆˆ โ„•0 โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐‘€ + ๐‘—) โˆˆ โ„•0)
623, 61sylan 581 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐‘€ + ๐‘—) โˆˆ โ„•0)
639eftval 15966 . . . . . 6 ((๐‘€ + ๐‘—) โˆˆ โ„•0 โ†’ (๐บโ€˜(๐‘€ + ๐‘—)) = (((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) / (!โ€˜(๐‘€ + ๐‘—))))
6462, 63syl 17 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐บโ€˜(๐‘€ + ๐‘—)) = (((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) / (!โ€˜(๐‘€ + ๐‘—))))
658adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โˆˆ โ„)
66 reeftcl 15964 . . . . . 6 (((absโ€˜๐ด) โˆˆ โ„ โˆง (๐‘€ + ๐‘—) โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) / (!โ€˜(๐‘€ + ๐‘—))) โˆˆ โ„)
6765, 62, 66syl2anc 585 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) / (!โ€˜(๐‘€ + ๐‘—))) โˆˆ โ„)
6864, 67eqeltrd 2838 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐บโ€˜(๐‘€ + ๐‘—)) โˆˆ โ„)
69 oveq2 7370 . . . . . . 7 (๐‘› = ๐‘— โ†’ ((1 / (๐‘€ + 1))โ†‘๐‘›) = ((1 / (๐‘€ + 1))โ†‘๐‘—))
7069oveq2d 7378 . . . . . 6 (๐‘› = ๐‘— โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘›)) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
71 eftl.3 . . . . . 6 ๐ป = (๐‘› โˆˆ โ„•0 โ†ฆ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘›)))
72 ovex 7395 . . . . . 6 ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) โˆˆ V
7370, 71, 72fvmpt 6953 . . . . 5 (๐‘— โˆˆ โ„•0 โ†’ (๐ปโ€˜๐‘—) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
7473adantl 483 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐ปโ€˜๐‘—) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
7512, 16nndivred 12214 . . . . . 6 (๐œ‘ โ†’ (((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) โˆˆ โ„)
7675adantr 482 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) โˆˆ โ„)
772peano2nnd 12177 . . . . . . 7 (๐œ‘ โ†’ (๐‘€ + 1) โˆˆ โ„•)
7877nnrecred 12211 . . . . . 6 (๐œ‘ โ†’ (1 / (๐‘€ + 1)) โˆˆ โ„)
79 reexpcl 13991 . . . . . 6 (((1 / (๐‘€ + 1)) โˆˆ โ„ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((1 / (๐‘€ + 1))โ†‘๐‘—) โˆˆ โ„)
8078, 79sylan 581 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((1 / (๐‘€ + 1))โ†‘๐‘—) โˆˆ โ„)
8176, 80remulcld 11192 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) โˆˆ โ„)
8265, 62reexpcld 14075 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) โˆˆ โ„)
8312adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘€) โˆˆ โ„)
8462faccld 14191 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜(๐‘€ + ๐‘—)) โˆˆ โ„•)
8584nnred 12175 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜(๐‘€ + ๐‘—)) โˆˆ โ„)
8685, 81remulcld 11192 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜(๐‘€ + ๐‘—)) ยท ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—))) โˆˆ โ„)
873adantr 482 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ๐‘€ โˆˆ โ„•0)
88 uzid 12785 . . . . . . . . . 10 (๐‘€ โˆˆ โ„ค โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
8921, 88syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
90 uzaddcl 12836 . . . . . . . . 9 ((๐‘€ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐‘€ + ๐‘—) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
9189, 90sylan 581 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐‘€ + ๐‘—) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
921absge0d 15336 . . . . . . . . 9 (๐œ‘ โ†’ 0 โ‰ค (absโ€˜๐ด))
9392adantr 482 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ 0 โ‰ค (absโ€˜๐ด))
94 eftl.6 . . . . . . . . 9 (๐œ‘ โ†’ (absโ€˜๐ด) โ‰ค 1)
9594adantr 482 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜๐ด) โ‰ค 1)
9665, 87, 91, 93, 95leexp2rd 14165 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) โ‰ค ((absโ€˜๐ด)โ†‘๐‘€))
9716adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜๐‘€) โˆˆ โ„•)
98 nnexpcl 13987 . . . . . . . . . . . . 13 (((๐‘€ + 1) โˆˆ โ„• โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘€ + 1)โ†‘๐‘—) โˆˆ โ„•)
9977, 98sylan 581 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘€ + 1)โ†‘๐‘—) โˆˆ โ„•)
10097, 99nnmulcld 12213 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โˆˆ โ„•)
101100nnred 12175 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โˆˆ โ„)
1028, 3, 92expge0d 14076 . . . . . . . . . . . 12 (๐œ‘ โ†’ 0 โ‰ค ((absโ€˜๐ด)โ†‘๐‘€))
10312, 102jca 513 . . . . . . . . . . 11 (๐œ‘ โ†’ (((absโ€˜๐ด)โ†‘๐‘€) โˆˆ โ„ โˆง 0 โ‰ค ((absโ€˜๐ด)โ†‘๐‘€)))
104103adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘๐‘€) โˆˆ โ„ โˆง 0 โ‰ค ((absโ€˜๐ด)โ†‘๐‘€)))
105 faclbnd6 14206 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„•0 โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โ‰ค (!โ€˜(๐‘€ + ๐‘—)))
1063, 105sylan 581 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โ‰ค (!โ€˜(๐‘€ + ๐‘—)))
107 lemul1a 12016 . . . . . . . . . 10 (((((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โˆˆ โ„ โˆง (!โ€˜(๐‘€ + ๐‘—)) โˆˆ โ„ โˆง (((absโ€˜๐ด)โ†‘๐‘€) โˆˆ โ„ โˆง 0 โ‰ค ((absโ€˜๐ด)โ†‘๐‘€))) โˆง ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โ‰ค (!โ€˜(๐‘€ + ๐‘—))) โ†’ (((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) โ‰ค ((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)))
108101, 85, 104, 106, 107syl31anc 1374 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) โ‰ค ((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)))
10985, 83remulcld 11192 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) โˆˆ โ„)
110100nnrpd 12962 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โˆˆ โ„+)
11183, 109, 110lemuldiv2d 13014 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) โ‰ค ((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) โ†” ((absโ€˜๐ด)โ†‘๐‘€) โ‰ค (((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)))))
112108, 111mpbid 231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘€) โ‰ค (((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—))))
11384nncnd 12176 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜(๐‘€ + ๐‘—)) โˆˆ โ„‚)
11412recnd 11190 . . . . . . . . . . 11 (๐œ‘ โ†’ ((absโ€˜๐ด)โ†‘๐‘€) โˆˆ โ„‚)
115114adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘€) โˆˆ โ„‚)
116100nncnd 12176 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โˆˆ โ„‚)
117100nnne0d 12210 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)) โ‰  0)
118113, 115, 116, 117divassd 11973 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—))) = ((!โ€˜(๐‘€ + ๐‘—)) ยท (((absโ€˜๐ด)โ†‘๐‘€) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)))))
11977nncnd 12176 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘€ + 1) โˆˆ โ„‚)
120119adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐‘€ + 1) โˆˆ โ„‚)
12177adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐‘€ + 1) โˆˆ โ„•)
122121nnne0d 12210 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐‘€ + 1) โ‰  0)
123 nn0z 12531 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„•0 โ†’ ๐‘— โˆˆ โ„ค)
124123adantl 483 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ๐‘— โˆˆ โ„ค)
125120, 122, 124exprecd 14066 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((1 / (๐‘€ + 1))โ†‘๐‘—) = (1 / ((๐‘€ + 1)โ†‘๐‘—)))
126125oveq2d 7378 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท (1 / ((๐‘€ + 1)โ†‘๐‘—))))
12775recnd 11190 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) โˆˆ โ„‚)
128127adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) โˆˆ โ„‚)
12999nncnd 12176 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘€ + 1)โ†‘๐‘—) โˆˆ โ„‚)
13099nnne0d 12210 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘€ + 1)โ†‘๐‘—) โ‰  0)
131128, 129, 130divrecd 11941 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) / ((๐‘€ + 1)โ†‘๐‘—)) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท (1 / ((๐‘€ + 1)โ†‘๐‘—))))
13216nncnd 12176 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (!โ€˜๐‘€) โˆˆ โ„‚)
133132adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜๐‘€) โˆˆ โ„‚)
134 facne0 14193 . . . . . . . . . . . . . 14 (๐‘€ โˆˆ โ„•0 โ†’ (!โ€˜๐‘€) โ‰  0)
1353, 134syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (!โ€˜๐‘€) โ‰  0)
136135adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜๐‘€) โ‰  0)
137115, 133, 129, 136, 130divdiv1d 11969 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) / ((๐‘€ + 1)โ†‘๐‘—)) = (((absโ€˜๐ด)โ†‘๐‘€) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—))))
138126, 131, 1373eqtr2rd 2784 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘๐‘€) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—))) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
139138oveq2d 7378 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((!โ€˜(๐‘€ + ๐‘—)) ยท (((absโ€˜๐ด)โ†‘๐‘€) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—)))) = ((!โ€˜(๐‘€ + ๐‘—)) ยท ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—))))
140118, 139eqtrd 2777 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((!โ€˜(๐‘€ + ๐‘—)) ยท ((absโ€˜๐ด)โ†‘๐‘€)) / ((!โ€˜๐‘€) ยท ((๐‘€ + 1)โ†‘๐‘—))) = ((!โ€˜(๐‘€ + ๐‘—)) ยท ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—))))
141112, 140breqtrd 5136 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘๐‘€) โ‰ค ((!โ€˜(๐‘€ + ๐‘—)) ยท ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—))))
14282, 83, 86, 96, 141letrd 11319 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) โ‰ค ((!โ€˜(๐‘€ + ๐‘—)) ยท ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—))))
14384nngt0d 12209 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ 0 < (!โ€˜(๐‘€ + ๐‘—)))
144 ledivmul 12038 . . . . . . 7 ((((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) โˆˆ โ„ โˆง ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) โˆˆ โ„ โˆง ((!โ€˜(๐‘€ + ๐‘—)) โˆˆ โ„ โˆง 0 < (!โ€˜(๐‘€ + ๐‘—)))) โ†’ ((((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) / (!โ€˜(๐‘€ + ๐‘—))) โ‰ค ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) โ†” ((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) โ‰ค ((!โ€˜(๐‘€ + ๐‘—)) ยท ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))))
14582, 81, 85, 143, 144syl112anc 1375 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) / (!โ€˜(๐‘€ + ๐‘—))) โ‰ค ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) โ†” ((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) โ‰ค ((!โ€˜(๐‘€ + ๐‘—)) ยท ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))))
146142, 145mpbird 257 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (((absโ€˜๐ด)โ†‘(๐‘€ + ๐‘—)) / (!โ€˜(๐‘€ + ๐‘—))) โ‰ค ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
14764, 146eqbrtrd 5132 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐บโ€˜(๐‘€ + ๐‘—)) โ‰ค ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
148 0z 12517 . . . . . 6 0 โˆˆ โ„ค
14921znegcld 12616 . . . . . 6 (๐œ‘ โ†’ -๐‘€ โˆˆ โ„ค)
15058seqshft 14977 . . . . . 6 ((0 โˆˆ โ„ค โˆง -๐‘€ โˆˆ โ„ค) โ†’ seq0( + , (๐บ shift -๐‘€)) = (seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€))
151148, 149, 150sylancr 588 . . . . 5 (๐œ‘ โ†’ seq0( + , (๐บ shift -๐‘€)) = (seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€))
152 0cn 11154 . . . . . . . . . . . 12 0 โˆˆ โ„‚
153 subneg 11457 . . . . . . . . . . . 12 ((0 โˆˆ โ„‚ โˆง ๐‘€ โˆˆ โ„‚) โ†’ (0 โˆ’ -๐‘€) = (0 + ๐‘€))
154152, 153mpan 689 . . . . . . . . . . 11 (๐‘€ โˆˆ โ„‚ โ†’ (0 โˆ’ -๐‘€) = (0 + ๐‘€))
155 addid2 11345 . . . . . . . . . . 11 (๐‘€ โˆˆ โ„‚ โ†’ (0 + ๐‘€) = ๐‘€)
156154, 155eqtrd 2777 . . . . . . . . . 10 (๐‘€ โˆˆ โ„‚ โ†’ (0 โˆ’ -๐‘€) = ๐‘€)
15754, 156syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (0 โˆ’ -๐‘€) = ๐‘€)
158157seqeq1d 13919 . . . . . . . 8 (๐œ‘ โ†’ seq(0 โˆ’ -๐‘€)( + , ๐บ) = seq๐‘€( + , ๐บ))
159158, 45eqbrtrd 5132 . . . . . . 7 (๐œ‘ โ†’ seq(0 โˆ’ -๐‘€)( + , ๐บ) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜))
160 seqex 13915 . . . . . . . 8 seq(0 โˆ’ -๐‘€)( + , ๐บ) โˆˆ V
161 climshft 15465 . . . . . . . 8 ((-๐‘€ โˆˆ โ„ค โˆง seq(0 โˆ’ -๐‘€)( + , ๐บ) โˆˆ V) โ†’ ((seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜) โ†” seq(0 โˆ’ -๐‘€)( + , ๐บ) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜)))
162149, 160, 161sylancl 587 . . . . . . 7 (๐œ‘ โ†’ ((seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜) โ†” seq(0 โˆ’ -๐‘€)( + , ๐บ) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜)))
163159, 162mpbird 257 . . . . . 6 (๐œ‘ โ†’ (seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜))
164 ovex 7395 . . . . . . 7 (seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€) โˆˆ V
165 sumex 15579 . . . . . . 7 ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜) โˆˆ V
166164, 165breldm 5869 . . . . . 6 ((seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€) โ‡ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜) โ†’ (seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€) โˆˆ dom โ‡ )
167163, 166syl 17 . . . . 5 (๐œ‘ โ†’ (seq(0 โˆ’ -๐‘€)( + , ๐บ) shift -๐‘€) โˆˆ dom โ‡ )
168151, 167eqeltrd 2838 . . . 4 (๐œ‘ โ†’ seq0( + , (๐บ shift -๐‘€)) โˆˆ dom โ‡ )
1692nnge1d 12208 . . . . . . . . . 10 (๐œ‘ โ†’ 1 โ‰ค ๐‘€)
170 1nn 12171 . . . . . . . . . . 11 1 โˆˆ โ„•
171 nnleltp1 12565 . . . . . . . . . . 11 ((1 โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•) โ†’ (1 โ‰ค ๐‘€ โ†” 1 < (๐‘€ + 1)))
172170, 2, 171sylancr 588 . . . . . . . . . 10 (๐œ‘ โ†’ (1 โ‰ค ๐‘€ โ†” 1 < (๐‘€ + 1)))
173169, 172mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ 1 < (๐‘€ + 1))
17414nn0ge0d 12483 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โ‰ค (๐‘€ + 1))
17515, 174absidd 15314 . . . . . . . . 9 (๐œ‘ โ†’ (absโ€˜(๐‘€ + 1)) = (๐‘€ + 1))
176173, 175breqtrrd 5138 . . . . . . . 8 (๐œ‘ โ†’ 1 < (absโ€˜(๐‘€ + 1)))
177 eqid 2737 . . . . . . . . . 10 (๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›)) = (๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›))
178 ovex 7395 . . . . . . . . . 10 ((1 / (๐‘€ + 1))โ†‘๐‘—) โˆˆ V
17969, 177, 178fvmpt 6953 . . . . . . . . 9 (๐‘— โˆˆ โ„•0 โ†’ ((๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›))โ€˜๐‘—) = ((1 / (๐‘€ + 1))โ†‘๐‘—))
180179adantl 483 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›))โ€˜๐‘—) = ((1 / (๐‘€ + 1))โ†‘๐‘—))
181119, 176, 180georeclim 15764 . . . . . . 7 (๐œ‘ โ†’ seq0( + , (๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›))) โ‡ ((๐‘€ + 1) / ((๐‘€ + 1) โˆ’ 1)))
18280recnd 11190 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((1 / (๐‘€ + 1))โ†‘๐‘—) โˆˆ โ„‚)
183180, 182eqeltrd 2838 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›))โ€˜๐‘—) โˆˆ โ„‚)
184180oveq2d 7378 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›))โ€˜๐‘—)) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
18574, 184eqtr4d 2780 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐ปโ€˜๐‘—) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘› โˆˆ โ„•0 โ†ฆ ((1 / (๐‘€ + 1))โ†‘๐‘›))โ€˜๐‘—)))
18652, 53, 127, 181, 183, 185isermulc2 15549 . . . . . 6 (๐œ‘ โ†’ seq0( + , ๐ป) โ‡ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘€ + 1) / ((๐‘€ + 1) โˆ’ 1))))
187 ax-1cn 11116 . . . . . . . . . . 11 1 โˆˆ โ„‚
188 pncan 11414 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘€ + 1) โˆ’ 1) = ๐‘€)
18954, 187, 188sylancl 587 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘€ + 1) โˆ’ 1) = ๐‘€)
190189oveq2d 7378 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘€ + 1) / ((๐‘€ + 1) โˆ’ 1)) = ((๐‘€ + 1) / ๐‘€))
191190oveq2d 7378 . . . . . . . 8 (๐œ‘ โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘€ + 1) / ((๐‘€ + 1) โˆ’ 1))) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘€ + 1) / ๐‘€)))
19215, 2nndivred 12214 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘€ + 1) / ๐‘€) โˆˆ โ„)
193192recnd 11190 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘€ + 1) / ๐‘€) โˆˆ โ„‚)
194114, 193, 132, 135div23d 11975 . . . . . . . 8 (๐œ‘ โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ๐‘€)) / (!โ€˜๐‘€)) = ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘€ + 1) / ๐‘€)))
195191, 194eqtr4d 2780 . . . . . . 7 (๐œ‘ โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘€ + 1) / ((๐‘€ + 1) โˆ’ 1))) = ((((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ๐‘€)) / (!โ€˜๐‘€)))
196114, 193, 132, 135divassd 11973 . . . . . . 7 (๐œ‘ โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ๐‘€)) / (!โ€˜๐‘€)) = (((absโ€˜๐ด)โ†‘๐‘€) ยท (((๐‘€ + 1) / ๐‘€) / (!โ€˜๐‘€))))
1972nnne0d 12210 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โ‰  0)
198119, 54, 132, 197, 135divdiv1d 11969 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘€ + 1) / ๐‘€) / (!โ€˜๐‘€)) = ((๐‘€ + 1) / (๐‘€ ยท (!โ€˜๐‘€))))
19954, 132mulcomd 11183 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘€ ยท (!โ€˜๐‘€)) = ((!โ€˜๐‘€) ยท ๐‘€))
200199oveq2d 7378 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘€ + 1) / (๐‘€ ยท (!โ€˜๐‘€))) = ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€)))
201198, 200eqtrd 2777 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘€ + 1) / ๐‘€) / (!โ€˜๐‘€)) = ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€)))
202201oveq2d 7378 . . . . . . 7 (๐œ‘ โ†’ (((absโ€˜๐ด)โ†‘๐‘€) ยท (((๐‘€ + 1) / ๐‘€) / (!โ€˜๐‘€))) = (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))))
203195, 196, 2023eqtrd 2781 . . . . . 6 (๐œ‘ โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((๐‘€ + 1) / ((๐‘€ + 1) โˆ’ 1))) = (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))))
204186, 203breqtrd 5136 . . . . 5 (๐œ‘ โ†’ seq0( + , ๐ป) โ‡ (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))))
205 seqex 13915 . . . . . 6 seq0( + , ๐ป) โˆˆ V
206 ovex 7395 . . . . . 6 (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))) โˆˆ V
207205, 206breldm 5869 . . . . 5 (seq0( + , ๐ป) โ‡ (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))) โ†’ seq0( + , ๐ป) โˆˆ dom โ‡ )
208204, 207syl 17 . . . 4 (๐œ‘ โ†’ seq0( + , ๐ป) โˆˆ dom โ‡ )
20952, 53, 60, 68, 74, 81, 147, 168, 208isumle 15736 . . 3 (๐œ‘ โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐บโ€˜(๐‘€ + ๐‘—)) โ‰ค ฮฃ๐‘— โˆˆ โ„•0 ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)))
210 eqid 2737 . . . . 5 (โ„คโ‰ฅโ€˜(0 + ๐‘€)) = (โ„คโ‰ฅโ€˜(0 + ๐‘€))
211 fveq2 6847 . . . . 5 (๐‘˜ = (๐‘€ + ๐‘—) โ†’ (๐บโ€˜๐‘˜) = (๐บโ€˜(๐‘€ + ๐‘—)))
21254addid2d 11363 . . . . . . . . 9 (๐œ‘ โ†’ (0 + ๐‘€) = ๐‘€)
213212fveq2d 6851 . . . . . . . 8 (๐œ‘ โ†’ (โ„คโ‰ฅโ€˜(0 + ๐‘€)) = (โ„คโ‰ฅโ€˜๐‘€))
214213eleq2d 2824 . . . . . . 7 (๐œ‘ โ†’ (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(0 + ๐‘€)) โ†” ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)))
215214biimpa 478 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(0 + ๐‘€))) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
216215, 41syldan 592 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(0 + ๐‘€))) โ†’ (๐บโ€˜๐‘˜) โˆˆ โ„‚)
21752, 210, 211, 21, 53, 216isumshft 15731 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(0 + ๐‘€))(๐บโ€˜๐‘˜) = ฮฃ๐‘— โˆˆ โ„•0 (๐บโ€˜(๐‘€ + ๐‘—)))
218213sumeq1d 15593 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜(0 + ๐‘€))(๐บโ€˜๐‘˜) = ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜))
219217, 218eqtr3d 2779 . . 3 (๐œ‘ โ†’ ฮฃ๐‘— โˆˆ โ„•0 (๐บโ€˜(๐‘€ + ๐‘—)) = ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜))
22081recnd 11190 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) โˆˆ โ„‚)
22152, 53, 74, 220, 204isumclim 15649 . . 3 (๐œ‘ โ†’ ฮฃ๐‘— โˆˆ โ„•0 ((((absโ€˜๐ด)โ†‘๐‘€) / (!โ€˜๐‘€)) ยท ((1 / (๐‘€ + 1))โ†‘๐‘—)) = (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))))
222209, 219, 2213brtr3d 5141 . 2 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐บโ€˜๐‘˜) โ‰ค (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))))
2237, 11, 19, 51, 222letrd 11319 1 (๐œ‘ โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜)) โ‰ค (((absโ€˜๐ด)โ†‘๐‘€) ยท ((๐‘€ + 1) / ((!โ€˜๐‘€) ยท ๐‘€))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  Vcvv 3448   class class class wbr 5110   โ†ฆ cmpt 5193  dom cdm 5638  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392  -cneg 11393   / cdiv 11819  โ„•cn 12160  โ„•0cn0 12420  โ„คcz 12506  โ„คโ‰ฅcuz 12770  seqcseq 13913  โ†‘cexp 13974  !cfa 14180   shift cshi 14958  abscabs 15126   โ‡ cli 15373  ฮฃcsu 15577
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-fac 14181  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578
This theorem is referenced by:  ef01bndlem  16073  eirrlem  16093  dveflem  25359  subfaclim  33822
  Copyright terms: Public domain W3C validator