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

Theorem binomlem 11508
Description: Lemma for binom 11509 (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
Hypotheses
Ref Expression
binomlem.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
binomlem.2 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
binomlem.3 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
binomlem.4 (๐œ“ โ†’ ((๐ด + ๐ต)โ†‘๐‘) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
Assertion
Ref Expression
binomlem ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
Distinct variable groups:   ๐ด,๐‘˜   ๐ต,๐‘˜   ๐‘˜,๐‘   ๐œ‘,๐‘˜
Allowed substitution hint:   ๐œ“(๐‘˜)

Proof of Theorem binomlem
Dummy variables ๐‘— ๐‘› are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 binomlem.4 . . . . . 6 (๐œ“ โ†’ ((๐ด + ๐ต)โ†‘๐‘) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
21adantl 277 . . . . 5 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต)โ†‘๐‘) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
32oveq1d 5905 . . . 4 ((๐œ‘ โˆง ๐œ“) โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด))
4 0zd 9282 . . . . . . . 8 (๐œ‘ โ†’ 0 โˆˆ โ„ค)
5 binomlem.3 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
65nn0zd 9390 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
74, 6fzfigd 10448 . . . . . . 7 (๐œ‘ โ†’ (0...๐‘) โˆˆ Fin)
8 binomlem.1 . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
9 fzelp1 10091 . . . . . . . . 9 (๐‘˜ โˆˆ (0...๐‘) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
10 elfzelz 10042 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
11 bccl 10764 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
125, 10, 11syl2an 289 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
1312nn0cnd 9248 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C๐‘˜) โˆˆ โ„‚)
149, 13sylan2 286 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐‘C๐‘˜) โˆˆ โ„‚)
15 fznn0sub 10074 . . . . . . . . . 10 (๐‘˜ โˆˆ (0...๐‘) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0)
16 expcl 10555 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
178, 15, 16syl2an 289 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
18 binomlem.2 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
19 elfznn0 10131 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„•0)
20 expcl 10555 . . . . . . . . . . 11 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ตโ†‘๐‘˜) โˆˆ โ„‚)
2118, 19, 20syl2an 289 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐ตโ†‘๐‘˜) โˆˆ โ„‚)
229, 21sylan2 286 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ตโ†‘๐‘˜) โˆˆ โ„‚)
2317, 22mulcld 7995 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) โˆˆ โ„‚)
2414, 23mulcld 7995 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
257, 8, 24fsummulc1 11474 . . . . . 6 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด))
268adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐ด โˆˆ โ„‚)
2714, 23, 26mulassd 7998 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ((๐‘C๐‘˜) ยท (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด)))
285nn0cnd 9248 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
2928adantr 276 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘ โˆˆ โ„‚)
30 1cnd 7990 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ 1 โˆˆ โ„‚)
31 elfzelz 10042 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (0...๐‘) โ†’ ๐‘˜ โˆˆ โ„ค)
3231adantl 277 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘˜ โˆˆ โ„ค)
3332zcnd 9393 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘˜ โˆˆ โ„‚)
3429, 30, 33addsubd 8306 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) = ((๐‘ โˆ’ ๐‘˜) + 1))
3534oveq2d 5906 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) = (๐ดโ†‘((๐‘ โˆ’ ๐‘˜) + 1)))
36 expp1 10544 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ดโ†‘((๐‘ โˆ’ ๐‘˜) + 1)) = ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด))
378, 15, 36syl2an 289 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘((๐‘ โˆ’ ๐‘˜) + 1)) = ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด))
3835, 37eqtrd 2221 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) = ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด))
3938oveq1d 5905 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด) ยท (๐ตโ†‘๐‘˜)))
4017, 26, 22mul32d 8127 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด) ยท (๐ตโ†‘๐‘˜)) = (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด))
4139, 40eqtrd 2221 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด))
4241oveq2d 5906 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ((๐‘C๐‘˜) ยท (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด)))
4327, 42eqtr4d 2224 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
4443sumeq2dv 11393 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
45 fzssp1 10084 . . . . . . . 8 (0...๐‘) โІ (0...(๐‘ + 1))
4645a1i 9 . . . . . . 7 (๐œ‘ โ†’ (0...๐‘) โІ (0...(๐‘ + 1)))
47 fznn0sub 10074 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) โˆˆ โ„•0)
48 expcl 10555 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง ((๐‘ + 1) โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
498, 47, 48syl2an 289 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
5049, 21mulcld 7995 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) โˆˆ โ„‚)
5113, 50mulcld 7995 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
529, 51sylan2 286 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
535adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ๐‘ โˆˆ โ„•0)
54 eldifi 3271 . . . . . . . . . . . 12 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘)) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
5554, 10syl 14 . . . . . . . . . . 11 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘)) โ†’ ๐‘˜ โˆˆ โ„ค)
5655adantl 277 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ๐‘˜ โˆˆ โ„ค)
57 eldifn 3272 . . . . . . . . . . 11 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘)) โ†’ ยฌ ๐‘˜ โˆˆ (0...๐‘))
5857adantl 277 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ยฌ ๐‘˜ โˆˆ (0...๐‘))
59 bcval3 10748 . . . . . . . . . 10 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค โˆง ยฌ ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐‘C๐‘˜) = 0)
6053, 56, 58, 59syl3anc 1248 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ (๐‘C๐‘˜) = 0)
6160oveq1d 5905 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
6250mul02d 8366 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
6354, 62sylan2 286 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
6461, 63eqtrd 2221 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
65 eluzelz 9554 . . . . . . . . . 10 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜0) โ†’ ๐‘› โˆˆ โ„ค)
6665adantl 277 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ๐‘› โˆˆ โ„ค)
67 0zd 9282 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ 0 โˆˆ โ„ค)
686adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ๐‘ โˆˆ โ„ค)
69 fzdcel 10057 . . . . . . . . 9 ((๐‘› โˆˆ โ„ค โˆง 0 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ DECID ๐‘› โˆˆ (0...๐‘))
7066, 67, 68, 69syl3anc 1248 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ DECID ๐‘› โˆˆ (0...๐‘))
7170ralrimiva 2562 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)DECID ๐‘› โˆˆ (0...๐‘))
72 fzssuz 10082 . . . . . . . 8 (0...(๐‘ + 1)) โІ (โ„คโ‰ฅโ€˜0)
7372a1i 9 . . . . . . 7 (๐œ‘ โ†’ (0...(๐‘ + 1)) โІ (โ„คโ‰ฅโ€˜0))
7468peano2zd 9395 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (๐‘ + 1) โˆˆ โ„ค)
75 fzdcel 10057 . . . . . . . . 9 ((๐‘› โˆˆ โ„ค โˆง 0 โˆˆ โ„ค โˆง (๐‘ + 1) โˆˆ โ„ค) โ†’ DECID ๐‘› โˆˆ (0...(๐‘ + 1)))
7666, 67, 74, 75syl3anc 1248 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ DECID ๐‘› โˆˆ (0...(๐‘ + 1)))
7776ralrimiva 2562 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)DECID ๐‘› โˆˆ (0...(๐‘ + 1)))
7846, 52, 64, 71, 4, 73, 77isumss 11416 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
7925, 44, 783eqtrd 2225 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
8079adantr 276 . . . 4 ((๐œ‘ โˆง ๐œ“) โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
813, 80eqtrd 2221 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
821oveq1d 5905 . . . 4 (๐œ“ โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต))
837, 18, 24fsummulc1 11474 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต))
84 1zzd 9297 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
8518adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐ต โˆˆ โ„‚)
8624, 85mulcld 7995 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) โˆˆ โ„‚)
87 oveq2 5898 . . . . . . . . . 10 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐‘C๐‘˜) = (๐‘C(๐‘— โˆ’ 1)))
88 oveq2 5898 . . . . . . . . . . . 12 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐‘ โˆ’ ๐‘˜) = (๐‘ โˆ’ (๐‘— โˆ’ 1)))
8988oveq2d 5906 . . . . . . . . . . 11 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) = (๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))))
90 oveq2 5898 . . . . . . . . . . 11 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐ตโ†‘๐‘˜) = (๐ตโ†‘(๐‘— โˆ’ 1)))
9189, 90oveq12d 5908 . . . . . . . . . 10 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1))))
9287, 91oveq12d 5908 . . . . . . . . 9 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))))
9392oveq1d 5905 . . . . . . . 8 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = (((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต))
9484, 4, 6, 86, 93fsumshft 11469 . . . . . . 7 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘— โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต))
95 oveq1 5897 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ (๐‘— โˆ’ 1) = (๐‘˜ โˆ’ 1))
9695oveq2d 5906 . . . . . . . . . 10 (๐‘— = ๐‘˜ โ†’ (๐‘C(๐‘— โˆ’ 1)) = (๐‘C(๐‘˜ โˆ’ 1)))
9795oveq2d 5906 . . . . . . . . . . . 12 (๐‘— = ๐‘˜ โ†’ (๐‘ โˆ’ (๐‘— โˆ’ 1)) = (๐‘ โˆ’ (๐‘˜ โˆ’ 1)))
9897oveq2d 5906 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ (๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) = (๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))))
9995oveq2d 5906 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ (๐ตโ†‘(๐‘— โˆ’ 1)) = (๐ตโ†‘(๐‘˜ โˆ’ 1)))
10098, 99oveq12d 5908 . . . . . . . . . 10 (๐‘— = ๐‘˜ โ†’ ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1))) = ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))))
10196, 100oveq12d 5908 . . . . . . . . 9 (๐‘— = ๐‘˜ โ†’ ((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))))
102101oveq1d 5905 . . . . . . . 8 (๐‘— = ๐‘˜ โ†’ (((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต) = (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต))
103102cbvsumv 11386 . . . . . . 7 ฮฃ๐‘— โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต)
10494, 103eqtrdi 2237 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต))
10528adantr 276 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘ โˆˆ โ„‚)
106 elfzelz 10042 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
107106adantl 277 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„ค)
108107zcnd 9393 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„‚)
109 1cnd 7990 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ 1 โˆˆ โ„‚)
110105, 108, 109subsub3d 8315 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐‘ โˆ’ (๐‘˜ โˆ’ 1)) = ((๐‘ + 1) โˆ’ ๐‘˜))
111110oveq2d 5906 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) = (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)))
112111oveq1d 5905 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))))
113112oveq2d 5906 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))))
114113oveq1d 5905 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต))
115 0z 9281 . . . . . . . . . . . 12 0 โˆˆ โ„ค
116 fzp1ss 10090 . . . . . . . . . . . 12 (0 โˆˆ โ„ค โ†’ ((0 + 1)...(๐‘ + 1)) โІ (0...(๐‘ + 1)))
117115, 116ax-mp 5 . . . . . . . . . . 11 ((0 + 1)...(๐‘ + 1)) โІ (0...(๐‘ + 1))
118117sseli 3165 . . . . . . . . . 10 (๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
11910adantl 277 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„ค)
120 peano2zm 9308 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„ค)
121119, 120syl 14 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„ค)
122 bccl 10764 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„•0 โˆง (๐‘˜ โˆ’ 1) โˆˆ โ„ค) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„•0)
1235, 121, 122syl2an2r 595 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„•0)
124123nn0cnd 9248 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„‚)
125118, 124sylan2 286 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„‚)
126118, 49sylan2 286 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
12718adantr 276 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐ต โˆˆ โ„‚)
128 elfznn 10071 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (1...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„•)
129 0p1e1 9050 . . . . . . . . . . . . . . 15 (0 + 1) = 1
130129oveq1i 5900 . . . . . . . . . . . . . 14 ((0 + 1)...(๐‘ + 1)) = (1...(๐‘ + 1))
131128, 130eleq2s 2283 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„•)
132131adantl 277 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„•)
133 nnm1nn0 9234 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„•0)
134132, 133syl 14 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„•0)
135127, 134expcld 10671 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ตโ†‘(๐‘˜ โˆ’ 1)) โˆˆ โ„‚)
136126, 135mulcld 7995 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) โˆˆ โ„‚)
137125, 136, 127mulassd 7998 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต)))
138126, 135, 127mulassd 7998 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต)))
139 expm1t 10565 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ตโ†‘๐‘˜) = ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต))
14018, 131, 139syl2an 289 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ตโ†‘๐‘˜) = ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต))
141140oveq2d 5906 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต)))
142138, 141eqtr4d 2224 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))
143142oveq2d 5906 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต)) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
144114, 137, 1433eqtrd 2225 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
145144sumeq2dv 11393 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
146117a1i 9 . . . . . . 7 (๐œ‘ โ†’ ((0 + 1)...(๐‘ + 1)) โІ (0...(๐‘ + 1)))
147124, 50mulcld 7995 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
148118, 147sylan2 286 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
1495adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ๐‘ โˆˆ โ„•0)
150 eldifi 3271 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
151150adantl 277 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
152151, 10syl 14 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ๐‘˜ โˆˆ โ„ค)
153152, 120syl 14 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„ค)
154 eldifn 3272 . . . . . . . . . . . 12 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1))) โ†’ ยฌ ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)))
155154adantl 277 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ยฌ ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)))
156 0zd 9282 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ 0 โˆˆ โ„ค)
157149nn0zd 9390 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ๐‘ โˆˆ โ„ค)
158 1zzd 9297 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ 1 โˆˆ โ„ค)
159 fzaddel 10076 . . . . . . . . . . . . 13 (((0 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โˆง ((๐‘˜ โˆ’ 1) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค)) โ†’ ((๐‘˜ โˆ’ 1) โˆˆ (0...๐‘) โ†” ((๐‘˜ โˆ’ 1) + 1) โˆˆ ((0 + 1)...(๐‘ + 1))))
160156, 157, 153, 158, 159syl22anc 1249 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ((๐‘˜ โˆ’ 1) โˆˆ (0...๐‘) โ†” ((๐‘˜ โˆ’ 1) + 1) โˆˆ ((0 + 1)...(๐‘ + 1))))
161152zcnd 9393 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ๐‘˜ โˆˆ โ„‚)
162 ax-1cn 7921 . . . . . . . . . . . . . 14 1 โˆˆ โ„‚
163 npcan 8183 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘˜ โˆ’ 1) + 1) = ๐‘˜)
164161, 162, 163sylancl 413 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ((๐‘˜ โˆ’ 1) + 1) = ๐‘˜)
165164eleq1d 2257 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ (((๐‘˜ โˆ’ 1) + 1) โˆˆ ((0 + 1)...(๐‘ + 1)) โ†” ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))))
166160, 165bitrd 188 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ((๐‘˜ โˆ’ 1) โˆˆ (0...๐‘) โ†” ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))))
167155, 166mtbird 674 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ยฌ (๐‘˜ โˆ’ 1) โˆˆ (0...๐‘))
168 bcval3 10748 . . . . . . . . . 10 ((๐‘ โˆˆ โ„•0 โˆง (๐‘˜ โˆ’ 1) โˆˆ โ„ค โˆง ยฌ (๐‘˜ โˆ’ 1) โˆˆ (0...๐‘)) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) = 0)
169149, 153, 167, 168syl3anc 1248 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) = 0)
170169oveq1d 5905 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
171150, 62sylan2 286 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
172170, 171eqtrd 2221 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
17367peano2zd 9395 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (0 + 1) โˆˆ โ„ค)
174 fzdcel 10057 . . . . . . . . 9 ((๐‘› โˆˆ โ„ค โˆง (0 + 1) โˆˆ โ„ค โˆง (๐‘ + 1) โˆˆ โ„ค) โ†’ DECID ๐‘› โˆˆ ((0 + 1)...(๐‘ + 1)))
17566, 173, 74, 174syl3anc 1248 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ DECID ๐‘› โˆˆ ((0 + 1)...(๐‘ + 1)))
176175ralrimiva 2562 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)DECID ๐‘› โˆˆ ((0 + 1)...(๐‘ + 1)))
177146, 148, 172, 176, 4, 73, 77isumss 11416 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
178104, 145, 1773eqtrd 2225 . . . . 5 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
17983, 178eqtrd 2221 . . . 4 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
18082, 179sylan9eqr 2243 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
18181, 180oveq12d 5908 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)) = (ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
1828, 18addcld 7994 . . . . 5 (๐œ‘ โ†’ (๐ด + ๐ต) โˆˆ โ„‚)
183182, 5expp1d 10672 . . . 4 (๐œ‘ โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = (((๐ด + ๐ต)โ†‘๐‘) ยท (๐ด + ๐ต)))
184182, 5expcld 10671 . . . . 5 (๐œ‘ โ†’ ((๐ด + ๐ต)โ†‘๐‘) โˆˆ โ„‚)
185184, 8, 18adddid 7999 . . . 4 (๐œ‘ โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท (๐ด + ๐ต)) = ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)))
186183, 185eqtrd 2221 . . 3 (๐œ‘ โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)))
187186adantr 276 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)))
188 bcpasc 10763 . . . . . . . 8 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) = ((๐‘ + 1)C๐‘˜))
1895, 10, 188syl2an 289 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) = ((๐‘ + 1)C๐‘˜))
190189oveq1d 5905 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
19113, 124, 50adddird 8000 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
192190, 191eqtr3d 2223 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
193192sumeq2dv 11393 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
1946peano2zd 9395 . . . . . 6 (๐œ‘ โ†’ (๐‘ + 1) โˆˆ โ„ค)
1954, 194fzfigd 10448 . . . . 5 (๐œ‘ โ†’ (0...(๐‘ + 1)) โˆˆ Fin)
196195, 51, 147fsumadd 11431 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))) = (ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
197193, 196eqtrd 2221 . . 3 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
198197adantr 276 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
199181, 187, 1983eqtr4d 2231 1 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105  DECID wdc 835   = wceq 1363   โˆˆ wcel 2159   โˆ– cdif 3140   โІ wss 3143  โ€˜cfv 5230  (class class class)co 5890  โ„‚cc 7826  0cc0 7828  1c1 7829   + caddc 7831   ยท cmul 7833   โˆ’ cmin 8145  โ„•cn 8936  โ„•0cn0 9193  โ„คcz 9270  โ„คโ‰ฅcuz 9545  ...cfz 10025  โ†‘cexp 10536  Ccbc 10744  ฮฃcsu 11378
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 2161  ax-14 2162  ax-ext 2170  ax-coll 4132  ax-sep 4135  ax-nul 4143  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-setind 4550  ax-iinf 4601  ax-cnex 7919  ax-resscn 7920  ax-1cn 7921  ax-1re 7922  ax-icn 7923  ax-addcl 7924  ax-addrcl 7925  ax-mulcl 7926  ax-mulrcl 7927  ax-addcom 7928  ax-mulcom 7929  ax-addass 7930  ax-mulass 7931  ax-distr 7932  ax-i2m1 7933  ax-0lt1 7934  ax-1rid 7935  ax-0id 7936  ax-rnegex 7937  ax-precex 7938  ax-cnre 7939  ax-pre-ltirr 7940  ax-pre-ltwlin 7941  ax-pre-lttrn 7942  ax-pre-apti 7943  ax-pre-ltadd 7944  ax-pre-mulgt0 7945  ax-pre-mulext 7946  ax-arch 7947  ax-caucvg 7948
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 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-nel 2455  df-ral 2472  df-rex 2473  df-reu 2474  df-rmo 2475  df-rab 2476  df-v 2753  df-sbc 2977  df-csb 3072  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-nul 3437  df-if 3549  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-int 3859  df-iun 3902  df-br 4018  df-opab 4079  df-mpt 4080  df-tr 4116  df-id 4307  df-po 4310  df-iso 4311  df-iord 4380  df-on 4382  df-ilim 4383  df-suc 4385  df-iom 4604  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-isom 5239  df-riota 5846  df-ov 5893  df-oprab 5894  df-mpo 5895  df-1st 6158  df-2nd 6159  df-recs 6323  df-irdg 6388  df-frec 6409  df-1o 6434  df-oadd 6438  df-er 6552  df-en 6758  df-dom 6759  df-fin 6760  df-pnf 8011  df-mnf 8012  df-xr 8013  df-ltxr 8014  df-le 8015  df-sub 8147  df-neg 8148  df-reap 8549  df-ap 8556  df-div 8647  df-inn 8937  df-2 8995  df-3 8996  df-4 8997  df-n0 9194  df-z 9271  df-uz 9546  df-q 9637  df-rp 9671  df-fz 10026  df-fzo 10160  df-seqfrec 10463  df-exp 10537  df-fac 10723  df-bc 10745  df-ihash 10773  df-cj 10868  df-re 10869  df-im 10870  df-rsqrt 11024  df-abs 11025  df-clim 11304  df-sumdc 11379
This theorem is referenced by:  binom  11509
  Copyright terms: Public domain W3C validator