ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  efaddlem GIF version

Theorem efaddlem 11695
Description: Lemma for efadd 11696 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
efadd.1 ๐น = (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ดโ†‘๐‘›) / (!โ€˜๐‘›)))
efadd.2 ๐บ = (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ตโ†‘๐‘›) / (!โ€˜๐‘›)))
efadd.3 ๐ป = (๐‘› โˆˆ โ„•0 โ†ฆ (((๐ด + ๐ต)โ†‘๐‘›) / (!โ€˜๐‘›)))
efadd.4 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
efadd.5 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
Assertion
Ref Expression
efaddlem (๐œ‘ โ†’ (expโ€˜(๐ด + ๐ต)) = ((expโ€˜๐ด) ยท (expโ€˜๐ต)))
Distinct variable groups:   ๐ด,๐‘›   ๐ต,๐‘›
Allowed substitution hints:   ๐œ‘(๐‘›)   ๐น(๐‘›)   ๐บ(๐‘›)   ๐ป(๐‘›)

Proof of Theorem efaddlem
Dummy variables ๐‘— ๐‘˜ ๐‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efadd.4 . . . 4 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
2 efadd.5 . . . 4 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
31, 2addcld 7990 . . 3 (๐œ‘ โ†’ (๐ด + ๐ต) โˆˆ โ„‚)
4 efadd.3 . . . 4 ๐ป = (๐‘› โˆˆ โ„•0 โ†ฆ (((๐ด + ๐ต)โ†‘๐‘›) / (!โ€˜๐‘›)))
54efcvg 11687 . . 3 ((๐ด + ๐ต) โˆˆ โ„‚ โ†’ seq0( + , ๐ป) โ‡ (expโ€˜(๐ด + ๐ต)))
63, 5syl 14 . 2 (๐œ‘ โ†’ seq0( + , ๐ป) โ‡ (expโ€˜(๐ด + ๐ต)))
7 efadd.1 . . . . . 6 ๐น = (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ดโ†‘๐‘›) / (!โ€˜๐‘›)))
87eftvalcn 11678 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘—) = ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)))
91, 8sylan 283 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐นโ€˜๐‘—) = ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)))
10 absexp 11101 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜(๐ดโ†‘๐‘—)) = ((absโ€˜๐ด)โ†‘๐‘—))
111, 10sylan 283 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜(๐ดโ†‘๐‘—)) = ((absโ€˜๐ด)โ†‘๐‘—))
12 faccl 10728 . . . . . . . 8 (๐‘— โˆˆ โ„•0 โ†’ (!โ€˜๐‘—) โˆˆ โ„•)
1312adantl 277 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜๐‘—) โˆˆ โ„•)
14 nnre 8939 . . . . . . . 8 ((!โ€˜๐‘—) โˆˆ โ„• โ†’ (!โ€˜๐‘—) โˆˆ โ„)
15 nnnn0 9196 . . . . . . . . 9 ((!โ€˜๐‘—) โˆˆ โ„• โ†’ (!โ€˜๐‘—) โˆˆ โ„•0)
1615nn0ge0d 9245 . . . . . . . 8 ((!โ€˜๐‘—) โˆˆ โ„• โ†’ 0 โ‰ค (!โ€˜๐‘—))
1714, 16absidd 11189 . . . . . . 7 ((!โ€˜๐‘—) โˆˆ โ„• โ†’ (absโ€˜(!โ€˜๐‘—)) = (!โ€˜๐‘—))
1813, 17syl 14 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜(!โ€˜๐‘—)) = (!โ€˜๐‘—))
1911, 18oveq12d 5906 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((absโ€˜(๐ดโ†‘๐‘—)) / (absโ€˜(!โ€˜๐‘—))) = (((absโ€˜๐ด)โ†‘๐‘—) / (!โ€˜๐‘—)))
20 expcl 10551 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐ดโ†‘๐‘—) โˆˆ โ„‚)
211, 20sylan 283 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐ดโ†‘๐‘—) โˆˆ โ„‚)
2213nncnd 8946 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜๐‘—) โˆˆ โ„‚)
2313nnap0d 8978 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (!โ€˜๐‘—) # 0)
2421, 22, 23absdivapd 11217 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ (absโ€˜((๐ดโ†‘๐‘—) / (!โ€˜๐‘—))) = ((absโ€˜(๐ดโ†‘๐‘—)) / (absโ€˜(!โ€˜๐‘—))))
251abscld 11203 . . . . . . 7 (๐œ‘ โ†’ (absโ€˜๐ด) โˆˆ โ„)
2625recnd 7999 . . . . . 6 (๐œ‘ โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
27 eqid 2187 . . . . . . 7 (๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›))) = (๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))
2827eftvalcn 11678 . . . . . 6 (((absโ€˜๐ด) โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘—) = (((absโ€˜๐ด)โ†‘๐‘—) / (!โ€˜๐‘—)))
2926, 28sylan 283 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘—) = (((absโ€˜๐ด)โ†‘๐‘—) / (!โ€˜๐‘—)))
3019, 24, 293eqtr4rd 2231 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘—) = (absโ€˜((๐ดโ†‘๐‘—) / (!โ€˜๐‘—))))
31 eftcl 11675 . . . . 5 ((๐ด โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) โˆˆ โ„‚)
321, 31sylan 283 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ โ„•0) โ†’ ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) โˆˆ โ„‚)
33 efadd.2 . . . . . 6 ๐บ = (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ตโ†‘๐‘›) / (!โ€˜๐‘›)))
3433eftvalcn 11678 . . . . 5 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) = ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜)))
352, 34sylan 283 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘˜) = ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜)))
36 eftcl 11675 . . . . 5 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜)) โˆˆ โ„‚)
372, 36sylan 283 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜)) โˆˆ โ„‚)
384eftvalcn 11678 . . . . . 6 (((๐ด + ๐ต) โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ปโ€˜๐‘˜) = (((๐ด + ๐ต)โ†‘๐‘˜) / (!โ€˜๐‘˜)))
393, 38sylan 283 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ปโ€˜๐‘˜) = (((๐ด + ๐ต)โ†‘๐‘˜) / (!โ€˜๐‘˜)))
401adantr 276 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐ด โˆˆ โ„‚)
412adantr 276 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐ต โˆˆ โ„‚)
42 simpr 110 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„•0)
43 binom 11505 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((๐ด + ๐ต)โ†‘๐‘˜) = ฮฃ๐‘— โˆˆ (0...๐‘˜)((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))))
4440, 41, 42, 43syl3anc 1248 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ((๐ด + ๐ต)โ†‘๐‘˜) = ฮฃ๐‘— โˆˆ (0...๐‘˜)((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))))
4544oveq1d 5903 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (((๐ด + ๐ต)โ†‘๐‘˜) / (!โ€˜๐‘˜)) = (ฮฃ๐‘— โˆˆ (0...๐‘˜)((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)))
46 0zd 9278 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ 0 โˆˆ โ„ค)
4742nn0zd 9386 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ๐‘˜ โˆˆ โ„ค)
4846, 47fzfigd 10444 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (0...๐‘˜) โˆˆ Fin)
49 faccl 10728 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„•0 โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
5049adantl 277 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (!โ€˜๐‘˜) โˆˆ โ„•)
5150nncnd 8946 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (!โ€˜๐‘˜) โˆˆ โ„‚)
52 bccl2 10761 . . . . . . . . . . 11 (๐‘— โˆˆ (0...๐‘˜) โ†’ (๐‘˜C๐‘—) โˆˆ โ„•)
5352adantl 277 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐‘˜C๐‘—) โˆˆ โ„•)
5453nncnd 8946 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐‘˜C๐‘—) โˆˆ โ„‚)
551ad2antrr 488 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ๐ด โˆˆ โ„‚)
56 fznn0sub 10070 . . . . . . . . . . . 12 (๐‘— โˆˆ (0...๐‘˜) โ†’ (๐‘˜ โˆ’ ๐‘—) โˆˆ โ„•0)
5756adantl 277 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐‘˜ โˆ’ ๐‘—) โˆˆ โ„•0)
5855, 57expcld 10667 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) โˆˆ โ„‚)
592ad2antrr 488 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ๐ต โˆˆ โ„‚)
60 elfznn0 10127 . . . . . . . . . . . 12 (๐‘— โˆˆ (0...๐‘˜) โ†’ ๐‘— โˆˆ โ„•0)
6160adantl 277 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ๐‘— โˆˆ โ„•0)
6259, 61expcld 10667 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐ตโ†‘๐‘—) โˆˆ โ„‚)
6358, 62mulcld 7991 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—)) โˆˆ โ„‚)
6454, 63mulcld 7991 . . . . . . . 8 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) โˆˆ โ„‚)
6550nnap0d 8978 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (!โ€˜๐‘˜) # 0)
6648, 51, 64, 65fsumdivapc 11471 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (ฮฃ๐‘— โˆˆ (0...๐‘˜)((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)) = ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)))
6755, 61expcld 10667 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐ดโ†‘๐‘—) โˆˆ โ„‚)
6861, 12syl 14 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜๐‘—) โˆˆ โ„•)
6968nncnd 8946 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜๐‘—) โˆˆ โ„‚)
7068nnap0d 8978 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜๐‘—) # 0)
7167, 69, 70divclapd 8760 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) โˆˆ โ„‚)
7233eftvalcn 11678 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„‚ โˆง (๐‘˜ โˆ’ ๐‘—) โˆˆ โ„•0) โ†’ (๐บโ€˜(๐‘˜ โˆ’ ๐‘—)) = ((๐ตโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))))
7359, 57, 72syl2anc 411 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐บโ€˜(๐‘˜ โˆ’ ๐‘—)) = ((๐ตโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))))
7459, 57expcld 10667 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐ตโ†‘(๐‘˜ โˆ’ ๐‘—)) โˆˆ โ„‚)
75 faccl 10728 . . . . . . . . . . . . . 14 ((๐‘˜ โˆ’ ๐‘—) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘˜ โˆ’ ๐‘—)) โˆˆ โ„•)
7657, 75syl 14 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜(๐‘˜ โˆ’ ๐‘—)) โˆˆ โ„•)
7776nncnd 8946 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜(๐‘˜ โˆ’ ๐‘—)) โˆˆ โ„‚)
7876nnap0d 8978 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜(๐‘˜ โˆ’ ๐‘—)) # 0)
7974, 77, 78divclapd 8760 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((๐ตโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))) โˆˆ โ„‚)
8073, 79eqeltrd 2264 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐บโ€˜(๐‘˜ โˆ’ ๐‘—)) โˆˆ โ„‚)
8171, 80mulcld 7991 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))) โˆˆ โ„‚)
82 oveq2 5896 . . . . . . . . . . 11 (๐‘— = ((0 + ๐‘˜) โˆ’ ๐‘š) โ†’ (๐ดโ†‘๐‘—) = (๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)))
83 fveq2 5527 . . . . . . . . . . 11 (๐‘— = ((0 + ๐‘˜) โˆ’ ๐‘š) โ†’ (!โ€˜๐‘—) = (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š)))
8482, 83oveq12d 5906 . . . . . . . . . 10 (๐‘— = ((0 + ๐‘˜) โˆ’ ๐‘š) โ†’ ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) = ((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š))))
85 oveq2 5896 . . . . . . . . . . 11 (๐‘— = ((0 + ๐‘˜) โˆ’ ๐‘š) โ†’ (๐‘˜ โˆ’ ๐‘—) = (๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š)))
8685fveq2d 5531 . . . . . . . . . 10 (๐‘— = ((0 + ๐‘˜) โˆ’ ๐‘š) โ†’ (๐บโ€˜(๐‘˜ โˆ’ ๐‘—)) = (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š))))
8784, 86oveq12d 5906 . . . . . . . . 9 (๐‘— = ((0 + ๐‘˜) โˆ’ ๐‘š) โ†’ (((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))) = (((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š)))))
8846, 47, 81, 87fisumrev2 11467 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))) = ฮฃ๐‘š โˆˆ (0...๐‘˜)(((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š)))))
8933eftvalcn 11678 . . . . . . . . . . . . . 14 ((๐ต โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„•0) โ†’ (๐บโ€˜๐‘—) = ((๐ตโ†‘๐‘—) / (!โ€˜๐‘—)))
9059, 61, 89syl2anc 411 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐บโ€˜๐‘—) = ((๐ตโ†‘๐‘—) / (!โ€˜๐‘—)))
9190oveq2d 5904 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))) ยท (๐บโ€˜๐‘—)) = (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))) ยท ((๐ตโ†‘๐‘—) / (!โ€˜๐‘—))))
9276, 68nnmulcld 8981 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—)) โˆˆ โ„•)
9392nncnd 8946 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—)) โˆˆ โ„‚)
9477, 69, 78, 70mulap0d 8628 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—)) # 0)
9563, 93, 94divrecap2d 8764 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—)) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))) = ((1 / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))))
9658, 77, 62, 69, 78, 70divmuldivapd 8802 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))) ยท ((๐ตโ†‘๐‘—) / (!โ€˜๐‘—))) = (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—)) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))))
97 bcval2 10743 . . . . . . . . . . . . . . . . 17 (๐‘— โˆˆ (0...๐‘˜) โ†’ (๐‘˜C๐‘—) = ((!โ€˜๐‘˜) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))))
9897adantl 277 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐‘˜C๐‘—) = ((!โ€˜๐‘˜) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))))
9998oveq1d 5903 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((๐‘˜C๐‘—) / (!โ€˜๐‘˜)) = (((!โ€˜๐‘˜) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))) / (!โ€˜๐‘˜)))
10051adantr 276 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜๐‘˜) โˆˆ โ„‚)
10165adantr 276 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜๐‘˜) # 0)
102100, 93, 100, 94, 101divdiv32apd 8786 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((!โ€˜๐‘˜) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))) / (!โ€˜๐‘˜)) = (((!โ€˜๐‘˜) / (!โ€˜๐‘˜)) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))))
103100, 101dividapd 8756 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((!โ€˜๐‘˜) / (!โ€˜๐‘˜)) = 1)
104103oveq1d 5903 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((!โ€˜๐‘˜) / (!โ€˜๐‘˜)) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))) = (1 / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))))
105102, 104eqtrd 2220 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((!โ€˜๐‘˜) / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))) / (!โ€˜๐‘˜)) = (1 / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))))
10699, 105eqtrd 2220 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((๐‘˜C๐‘—) / (!โ€˜๐‘˜)) = (1 / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))))
107106oveq1d 5903 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐‘˜C๐‘—) / (!โ€˜๐‘˜)) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) = ((1 / ((!โ€˜(๐‘˜ โˆ’ ๐‘—)) ยท (!โ€˜๐‘—))) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))))
10895, 96, 1073eqtr4rd 2231 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐‘˜C๐‘—) / (!โ€˜๐‘˜)) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) = (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))) ยท ((๐ตโ†‘๐‘—) / (!โ€˜๐‘—))))
10991, 108eqtr4d 2223 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))) ยท (๐บโ€˜๐‘—)) = (((๐‘˜C๐‘—) / (!โ€˜๐‘˜)) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))))
110 nn0cn 9199 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚)
111110ad2antlr 489 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ๐‘˜ โˆˆ โ„‚)
112111addid2d 8120 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (0 + ๐‘˜) = ๐‘˜)
113112oveq1d 5903 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((0 + ๐‘˜) โˆ’ ๐‘—) = (๐‘˜ โˆ’ ๐‘—))
114113oveq2d 5904 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) = (๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)))
115113fveq2d 5531 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—)) = (!โ€˜(๐‘˜ โˆ’ ๐‘—)))
116114, 115oveq12d 5906 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—))) = ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))))
117113oveq2d 5904 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)) = (๐‘˜ โˆ’ (๐‘˜ โˆ’ ๐‘—)))
118 nn0cn 9199 . . . . . . . . . . . . . . . 16 (๐‘— โˆˆ โ„•0 โ†’ ๐‘— โˆˆ โ„‚)
11961, 118syl 14 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ ๐‘— โˆˆ โ„‚)
120111, 119nncand 8286 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐‘˜ โˆ’ (๐‘˜ โˆ’ ๐‘—)) = ๐‘—)
121117, 120eqtrd 2220 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)) = ๐‘—)
122121fveq2d 5531 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—))) = (๐บโ€˜๐‘—))
123116, 122oveq12d 5906 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)))) = (((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) / (!โ€˜(๐‘˜ โˆ’ ๐‘—))) ยท (๐บโ€˜๐‘—)))
12454, 63, 100, 101div23apd 8798 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)) = (((๐‘˜C๐‘—) / (!โ€˜๐‘˜)) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))))
125109, 123, 1243eqtr4rd 2231 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โˆง ๐‘— โˆˆ (0...๐‘˜)) โ†’ (((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)) = (((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)))))
126125sumeq2dv 11389 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)) = ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)))))
127 oveq2 5896 . . . . . . . . . . . . 13 (๐‘— = ๐‘š โ†’ ((0 + ๐‘˜) โˆ’ ๐‘—) = ((0 + ๐‘˜) โˆ’ ๐‘š))
128127oveq2d 5904 . . . . . . . . . . . 12 (๐‘— = ๐‘š โ†’ (๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) = (๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)))
129127fveq2d 5531 . . . . . . . . . . . 12 (๐‘— = ๐‘š โ†’ (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—)) = (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š)))
130128, 129oveq12d 5906 . . . . . . . . . . 11 (๐‘— = ๐‘š โ†’ ((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—))) = ((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š))))
131127oveq2d 5904 . . . . . . . . . . . 12 (๐‘— = ๐‘š โ†’ (๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)) = (๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š)))
132131fveq2d 5531 . . . . . . . . . . 11 (๐‘— = ๐‘š โ†’ (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—))) = (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š))))
133130, 132oveq12d 5906 . . . . . . . . . 10 (๐‘— = ๐‘š โ†’ (((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)))) = (((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š)))))
134133cbvsumv 11382 . . . . . . . . 9 ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘—)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘—))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘—)))) = ฮฃ๐‘š โˆˆ (0...๐‘˜)(((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š))))
135126, 134eqtrdi 2236 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)) = ฮฃ๐‘š โˆˆ (0...๐‘˜)(((๐ดโ†‘((0 + ๐‘˜) โˆ’ ๐‘š)) / (!โ€˜((0 + ๐‘˜) โˆ’ ๐‘š))) ยท (๐บโ€˜(๐‘˜ โˆ’ ((0 + ๐‘˜) โˆ’ ๐‘š)))))
13688, 135eqtr4d 2223 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))) = ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)))
13766, 136eqtr4d 2223 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (ฮฃ๐‘— โˆˆ (0...๐‘˜)((๐‘˜C๐‘—) ยท ((๐ดโ†‘(๐‘˜ โˆ’ ๐‘—)) ยท (๐ตโ†‘๐‘—))) / (!โ€˜๐‘˜)) = ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))))
13845, 137eqtrd 2220 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (((๐ด + ๐ต)โ†‘๐‘˜) / (!โ€˜๐‘˜)) = ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))))
13939, 138eqtrd 2220 . . . 4 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ปโ€˜๐‘˜) = ฮฃ๐‘— โˆˆ (0...๐‘˜)(((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท (๐บโ€˜(๐‘˜ โˆ’ ๐‘—))))
14027efcllem 11680 . . . . 5 ((absโ€˜๐ด) โˆˆ โ„‚ โ†’ seq0( + , (๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))) โˆˆ dom โ‡ )
14126, 140syl 14 . . . 4 (๐œ‘ โ†’ seq0( + , (๐‘› โˆˆ โ„•0 โ†ฆ (((absโ€˜๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))) โˆˆ dom โ‡ )
14233efcllem 11680 . . . . 5 (๐ต โˆˆ โ„‚ โ†’ seq0( + , ๐บ) โˆˆ dom โ‡ )
1432, 142syl 14 . . . 4 (๐œ‘ โ†’ seq0( + , ๐บ) โˆˆ dom โ‡ )
1447efcllem 11680 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
1451, 144syl 14 . . . 4 (๐œ‘ โ†’ seq0( + , ๐น) โˆˆ dom โ‡ )
1469, 30, 32, 35, 37, 139, 141, 143, 145mertensabs 11558 . . 3 (๐œ‘ โ†’ seq0( + , ๐ป) โ‡ (ฮฃ๐‘— โˆˆ โ„•0 ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท ฮฃ๐‘˜ โˆˆ โ„•0 ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜))))
147 efval 11682 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (expโ€˜๐ด) = ฮฃ๐‘— โˆˆ โ„•0 ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)))
1481, 147syl 14 . . . 4 (๐œ‘ โ†’ (expโ€˜๐ด) = ฮฃ๐‘— โˆˆ โ„•0 ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)))
149 efval 11682 . . . . 5 (๐ต โˆˆ โ„‚ โ†’ (expโ€˜๐ต) = ฮฃ๐‘˜ โˆˆ โ„•0 ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜)))
1502, 149syl 14 . . . 4 (๐œ‘ โ†’ (expโ€˜๐ต) = ฮฃ๐‘˜ โˆˆ โ„•0 ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜)))
151148, 150oveq12d 5906 . . 3 (๐œ‘ โ†’ ((expโ€˜๐ด) ยท (expโ€˜๐ต)) = (ฮฃ๐‘— โˆˆ โ„•0 ((๐ดโ†‘๐‘—) / (!โ€˜๐‘—)) ยท ฮฃ๐‘˜ โˆˆ โ„•0 ((๐ตโ†‘๐‘˜) / (!โ€˜๐‘˜))))
152146, 151breqtrrd 4043 . 2 (๐œ‘ โ†’ seq0( + , ๐ป) โ‡ ((expโ€˜๐ด) ยท (expโ€˜๐ต)))
153 climuni 11314 . 2 ((seq0( + , ๐ป) โ‡ (expโ€˜(๐ด + ๐ต)) โˆง seq0( + , ๐ป) โ‡ ((expโ€˜๐ด) ยท (expโ€˜๐ต))) โ†’ (expโ€˜(๐ด + ๐ต)) = ((expโ€˜๐ด) ยท (expโ€˜๐ต)))
1546, 152, 153syl2anc 411 1 (๐œ‘ โ†’ (expโ€˜(๐ด + ๐ต)) = ((expโ€˜๐ด) ยท (expโ€˜๐ต)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   = wceq 1363   โˆˆ wcel 2158   class class class wbr 4015   โ†ฆ cmpt 4076  dom cdm 4638  โ€˜cfv 5228  (class class class)co 5888  โ„‚cc 7822  0cc0 7824  1c1 7825   + caddc 7827   ยท cmul 7829   โˆ’ cmin 8141   # cap 8551   / cdiv 8642  โ„•cn 8932  โ„•0cn0 9189  ...cfz 10021  seqcseq 10458  โ†‘cexp 10532  !cfa 10718  Ccbc 10740  abscabs 11019   โ‡ cli 11299  ฮฃcsu 11374  expce 11663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-disj 3993  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-frec 6405  df-1o 6430  df-oadd 6434  df-er 6548  df-en 6754  df-dom 6755  df-fin 6756  df-sup 6996  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-ico 9907  df-fz 10022  df-fzo 10156  df-seqfrec 10459  df-exp 10533  df-fac 10719  df-bc 10741  df-ihash 10769  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-clim 11300  df-sumdc 11375  df-ef 11669
This theorem is referenced by:  efadd  11696
  Copyright terms: Public domain W3C validator