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

Theorem binomlem 11504
Description: Lemma for binom 11505 (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 5903 . . . 4 ((๐œ‘ โˆง ๐œ“) โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด))
4 0zd 9278 . . . . . . . 8 (๐œ‘ โ†’ 0 โˆˆ โ„ค)
5 binomlem.3 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
65nn0zd 9386 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
74, 6fzfigd 10444 . . . . . . 7 (๐œ‘ โ†’ (0...๐‘) โˆˆ Fin)
8 binomlem.1 . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
9 fzelp1 10087 . . . . . . . . 9 (๐‘˜ โˆˆ (0...๐‘) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
10 elfzelz 10038 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
11 bccl 10760 . . . . . . . . . . 11 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
125, 10, 11syl2an 289 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C๐‘˜) โˆˆ โ„•0)
1312nn0cnd 9244 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C๐‘˜) โˆˆ โ„‚)
149, 13sylan2 286 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐‘C๐‘˜) โˆˆ โ„‚)
15 fznn0sub 10070 . . . . . . . . . 10 (๐‘˜ โˆˆ (0...๐‘) โ†’ (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0)
16 expcl 10551 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
178, 15, 16syl2an 289 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) โˆˆ โ„‚)
18 binomlem.2 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
19 elfznn0 10127 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„•0)
20 expcl 10551 . . . . . . . . . . 11 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0) โ†’ (๐ตโ†‘๐‘˜) โˆˆ โ„‚)
2118, 19, 20syl2an 289 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐ตโ†‘๐‘˜) โˆˆ โ„‚)
229, 21sylan2 286 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ตโ†‘๐‘˜) โˆˆ โ„‚)
2317, 22mulcld 7991 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) โˆˆ โ„‚)
2414, 23mulcld 7991 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
257, 8, 24fsummulc1 11470 . . . . . 6 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด))
268adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐ด โˆˆ โ„‚)
2714, 23, 26mulassd 7994 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ((๐‘C๐‘˜) ยท (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด)))
285nn0cnd 9244 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
2928adantr 276 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘ โˆˆ โ„‚)
30 1cnd 7986 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ 1 โˆˆ โ„‚)
31 elfzelz 10038 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (0...๐‘) โ†’ ๐‘˜ โˆˆ โ„ค)
3231adantl 277 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘˜ โˆˆ โ„ค)
3332zcnd 9389 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐‘˜ โˆˆ โ„‚)
3429, 30, 33addsubd 8302 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) = ((๐‘ โˆ’ ๐‘˜) + 1))
3534oveq2d 5904 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) = (๐ดโ†‘((๐‘ โˆ’ ๐‘˜) + 1)))
36 expp1 10540 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (๐‘ โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ดโ†‘((๐‘ โˆ’ ๐‘˜) + 1)) = ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด))
378, 15, 36syl2an 289 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘((๐‘ โˆ’ ๐‘˜) + 1)) = ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด))
3835, 37eqtrd 2220 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) = ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด))
3938oveq1d 5903 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด) ยท (๐ตโ†‘๐‘˜)))
4017, 26, 22mul32d 8123 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท ๐ด) ยท (๐ตโ†‘๐‘˜)) = (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด))
4139, 40eqtrd 2220 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด))
4241oveq2d 5904 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ((๐‘C๐‘˜) ยท (((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) ยท ๐ด)))
4327, 42eqtr4d 2223 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
4443sumeq2dv 11389 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
45 fzssp1 10080 . . . . . . . 8 (0...๐‘) โІ (0...(๐‘ + 1))
4645a1i 9 . . . . . . 7 (๐œ‘ โ†’ (0...๐‘) โІ (0...(๐‘ + 1)))
47 fznn0sub 10070 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(๐‘ + 1)) โ†’ ((๐‘ + 1) โˆ’ ๐‘˜) โˆˆ โ„•0)
48 expcl 10551 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง ((๐‘ + 1) โˆ’ ๐‘˜) โˆˆ โ„•0) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
498, 47, 48syl2an 289 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) โˆˆ โ„‚)
5049, 21mulcld 7991 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) โˆˆ โ„‚)
5113, 50mulcld 7991 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
529, 51sylan2 286 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) โˆˆ โ„‚)
535adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ๐‘ โˆˆ โ„•0)
54 eldifi 3269 . . . . . . . . . . . 12 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘)) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
5554, 10syl 14 . . . . . . . . . . 11 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘)) โ†’ ๐‘˜ โˆˆ โ„ค)
5655adantl 277 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ๐‘˜ โˆˆ โ„ค)
57 eldifn 3270 . . . . . . . . . . 11 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘)) โ†’ ยฌ ๐‘˜ โˆˆ (0...๐‘))
5857adantl 277 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ยฌ ๐‘˜ โˆˆ (0...๐‘))
59 bcval3 10744 . . . . . . . . . 10 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค โˆง ยฌ ๐‘˜ โˆˆ (0...๐‘)) โ†’ (๐‘C๐‘˜) = 0)
6053, 56, 58, 59syl3anc 1248 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ (๐‘C๐‘˜) = 0)
6160oveq1d 5903 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
6250mul02d 8362 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
6354, 62sylan2 286 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ (0 ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
6461, 63eqtrd 2220 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– (0...๐‘))) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
65 eluzelz 9550 . . . . . . . . . 10 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜0) โ†’ ๐‘› โˆˆ โ„ค)
6665adantl 277 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ๐‘› โˆˆ โ„ค)
67 0zd 9278 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ 0 โˆˆ โ„ค)
686adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ ๐‘ โˆˆ โ„ค)
69 fzdcel 10053 . . . . . . . . 9 ((๐‘› โˆˆ โ„ค โˆง 0 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ DECID ๐‘› โˆˆ (0...๐‘))
7066, 67, 68, 69syl3anc 1248 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ DECID ๐‘› โˆˆ (0...๐‘))
7170ralrimiva 2560 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)DECID ๐‘› โˆˆ (0...๐‘))
72 fzssuz 10078 . . . . . . . 8 (0...(๐‘ + 1)) โІ (โ„คโ‰ฅโ€˜0)
7372a1i 9 . . . . . . 7 (๐œ‘ โ†’ (0...(๐‘ + 1)) โІ (โ„คโ‰ฅโ€˜0))
7468peano2zd 9391 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (๐‘ + 1) โˆˆ โ„ค)
75 fzdcel 10053 . . . . . . . . 9 ((๐‘› โˆˆ โ„ค โˆง 0 โˆˆ โ„ค โˆง (๐‘ + 1) โˆˆ โ„ค) โ†’ DECID ๐‘› โˆˆ (0...(๐‘ + 1)))
7666, 67, 74, 75syl3anc 1248 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ DECID ๐‘› โˆˆ (0...(๐‘ + 1)))
7776ralrimiva 2560 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)DECID ๐‘› โˆˆ (0...(๐‘ + 1)))
7846, 52, 64, 71, 4, 73, 77isumss 11412 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
7925, 44, 783eqtrd 2224 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
8079adantr 276 . . . 4 ((๐œ‘ โˆง ๐œ“) โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
813, 80eqtrd 2220 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
821oveq1d 5903 . . . 4 (๐œ“ โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต) = (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต))
837, 18, 24fsummulc1 11470 . . . . 5 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต))
84 1zzd 9293 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
8518adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ ๐ต โˆˆ โ„‚)
8624, 85mulcld 7991 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...๐‘)) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) โˆˆ โ„‚)
87 oveq2 5896 . . . . . . . . . 10 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐‘C๐‘˜) = (๐‘C(๐‘— โˆ’ 1)))
88 oveq2 5896 . . . . . . . . . . . 12 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐‘ โˆ’ ๐‘˜) = (๐‘ โˆ’ (๐‘— โˆ’ 1)))
8988oveq2d 5904 . . . . . . . . . . 11 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) = (๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))))
90 oveq2 5896 . . . . . . . . . . 11 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (๐ตโ†‘๐‘˜) = (๐ตโ†‘(๐‘— โˆ’ 1)))
9189, 90oveq12d 5906 . . . . . . . . . 10 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1))))
9287, 91oveq12d 5906 . . . . . . . . 9 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ ((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))))
9392oveq1d 5903 . . . . . . . 8 (๐‘˜ = (๐‘— โˆ’ 1) โ†’ (((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = (((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต))
9484, 4, 6, 86, 93fsumshft 11465 . . . . . . 7 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘— โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต))
95 oveq1 5895 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ (๐‘— โˆ’ 1) = (๐‘˜ โˆ’ 1))
9695oveq2d 5904 . . . . . . . . . 10 (๐‘— = ๐‘˜ โ†’ (๐‘C(๐‘— โˆ’ 1)) = (๐‘C(๐‘˜ โˆ’ 1)))
9795oveq2d 5904 . . . . . . . . . . . 12 (๐‘— = ๐‘˜ โ†’ (๐‘ โˆ’ (๐‘— โˆ’ 1)) = (๐‘ โˆ’ (๐‘˜ โˆ’ 1)))
9897oveq2d 5904 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ (๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) = (๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))))
9995oveq2d 5904 . . . . . . . . . . 11 (๐‘— = ๐‘˜ โ†’ (๐ตโ†‘(๐‘— โˆ’ 1)) = (๐ตโ†‘(๐‘˜ โˆ’ 1)))
10098, 99oveq12d 5906 . . . . . . . . . 10 (๐‘— = ๐‘˜ โ†’ ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1))) = ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))))
10196, 100oveq12d 5906 . . . . . . . . 9 (๐‘— = ๐‘˜ โ†’ ((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))))
102101oveq1d 5903 . . . . . . . 8 (๐‘— = ๐‘˜ โ†’ (((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต) = (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต))
103102cbvsumv 11382 . . . . . . 7 ฮฃ๐‘— โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘— โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘— โˆ’ 1))) ยท (๐ตโ†‘(๐‘— โˆ’ 1)))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต)
10494, 103eqtrdi 2236 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต))
10528adantr 276 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘ โˆˆ โ„‚)
106 elfzelz 10038 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
107106adantl 277 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„ค)
108107zcnd 9389 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„‚)
109 1cnd 7986 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ 1 โˆˆ โ„‚)
110105, 108, 109subsub3d 8311 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐‘ โˆ’ (๐‘˜ โˆ’ 1)) = ((๐‘ + 1) โˆ’ ๐‘˜))
111110oveq2d 5904 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) = (๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)))
112111oveq1d 5903 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))))
113112oveq2d 5904 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))))
114113oveq1d 5903 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต))
115 0z 9277 . . . . . . . . . . . 12 0 โˆˆ โ„ค
116 fzp1ss 10086 . . . . . . . . . . . 12 (0 โˆˆ โ„ค โ†’ ((0 + 1)...(๐‘ + 1)) โІ (0...(๐‘ + 1)))
117115, 116ax-mp 5 . . . . . . . . . . 11 ((0 + 1)...(๐‘ + 1)) โІ (0...(๐‘ + 1))
118117sseli 3163 . . . . . . . . . 10 (๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ (0...(๐‘ + 1)))
11910adantl 277 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„ค)
120 peano2zm 9304 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„ค โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„ค)
121119, 120syl 14 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„ค)
122 bccl 10760 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„•0 โˆง (๐‘˜ โˆ’ 1) โˆˆ โ„ค) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„•0)
1235, 121, 122syl2an2r 595 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) โˆˆ โ„•0)
124123nn0cnd 9244 . . . . . . . . . 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 10067 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (1...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„•)
129 0p1e1 9046 . . . . . . . . . . . . . . 15 (0 + 1) = 1
130129oveq1i 5898 . . . . . . . . . . . . . 14 ((0 + 1)...(๐‘ + 1)) = (1...(๐‘ + 1))
131128, 130eleq2s 2282 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)) โ†’ ๐‘˜ โˆˆ โ„•)
132131adantl 277 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ๐‘˜ โˆˆ โ„•)
133 nnm1nn0 9230 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„•0)
134132, 133syl 14 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐‘˜ โˆ’ 1) โˆˆ โ„•0)
135127, 134expcld 10667 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ตโ†‘(๐‘˜ โˆ’ 1)) โˆˆ โ„‚)
136126, 135mulcld 7991 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) โˆˆ โ„‚)
137125, 136, 127mulassd 7994 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต)))
138126, 135, 127mulassd 7994 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต)))
139 expm1t 10561 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ตโ†‘๐‘˜) = ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต))
14018, 131, 139syl2an 289 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (๐ตโ†‘๐‘˜) = ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต))
141140oveq2d 5904 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท ((๐ตโ†‘(๐‘˜ โˆ’ 1)) ยท ๐ต)))
142138, 141eqtr4d 2223 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต) = ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))
143142oveq2d 5904 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท (((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1))) ยท ๐ต)) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
144114, 137, 1433eqtrd 2224 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))) โ†’ (((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
145144sumeq2dv 11389 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))(((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘(๐‘ โˆ’ (๐‘˜ โˆ’ 1))) ยท (๐ตโ†‘(๐‘˜ โˆ’ 1)))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
146117a1i 9 . . . . . . 7 (๐œ‘ โ†’ ((0 + 1)...(๐‘ + 1)) โІ (0...(๐‘ + 1)))
147124, 50mulcld 7991 . . . . . . . 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 3269 . . . . . . . . . . . . 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 3270 . . . . . . . . . . . 12 (๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1))) โ†’ ยฌ ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)))
155154adantl 277 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ยฌ ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1)))
156 0zd 9278 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ 0 โˆˆ โ„ค)
157149nn0zd 9386 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ๐‘ โˆˆ โ„ค)
158 1zzd 9293 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ 1 โˆˆ โ„ค)
159 fzaddel 10072 . . . . . . . . . . . . 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 9389 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ๐‘˜ โˆˆ โ„‚)
162 ax-1cn 7917 . . . . . . . . . . . . . 14 1 โˆˆ โ„‚
163 npcan 8179 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘˜ โˆ’ 1) + 1) = ๐‘˜)
164161, 162, 163sylancl 413 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ((๐‘˜ โˆ’ 1) + 1) = ๐‘˜)
165164eleq1d 2256 . . . . . . . . . . . 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 10744 . . . . . . . . . 10 ((๐‘ โˆˆ โ„•0 โˆง (๐‘˜ โˆ’ 1) โˆˆ โ„ค โˆง ยฌ (๐‘˜ โˆ’ 1) โˆˆ (0...๐‘)) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) = 0)
169149, 153, 167, 168syl3anc 1248 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ (๐‘C(๐‘˜ โˆ’ 1)) = 0)
170169oveq1d 5903 . . . . . . . 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 2220 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ ((0...(๐‘ + 1)) โˆ– ((0 + 1)...(๐‘ + 1)))) โ†’ ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = 0)
17367peano2zd 9391 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ (0 + 1) โˆˆ โ„ค)
174 fzdcel 10053 . . . . . . . . 9 ((๐‘› โˆˆ โ„ค โˆง (0 + 1) โˆˆ โ„ค โˆง (๐‘ + 1) โˆˆ โ„ค) โ†’ DECID ๐‘› โˆˆ ((0 + 1)...(๐‘ + 1)))
17566, 173, 74, 174syl3anc 1248 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)) โ†’ DECID ๐‘› โˆˆ ((0 + 1)...(๐‘ + 1)))
176175ralrimiva 2560 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ (โ„คโ‰ฅโ€˜0)DECID ๐‘› โˆˆ ((0 + 1)...(๐‘ + 1)))
177146, 148, 172, 176, 4, 73, 77isumss 11412 . . . . . 6 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ ((0 + 1)...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
178104, 145, 1773eqtrd 2224 . . . . 5 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...๐‘)(((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
17983, 178eqtrd 2220 . . . 4 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ (0...๐‘)((๐‘C๐‘˜) ยท ((๐ดโ†‘(๐‘ โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
18082, 179sylan9eqr 2242 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
18181, 180oveq12d 5906 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)) = (ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
1828, 18addcld 7990 . . . . 5 (๐œ‘ โ†’ (๐ด + ๐ต) โˆˆ โ„‚)
183182, 5expp1d 10668 . . . 4 (๐œ‘ โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = (((๐ด + ๐ต)โ†‘๐‘) ยท (๐ด + ๐ต)))
184182, 5expcld 10667 . . . . 5 (๐œ‘ โ†’ ((๐ด + ๐ต)โ†‘๐‘) โˆˆ โ„‚)
185184, 8, 18adddid 7995 . . . 4 (๐œ‘ โ†’ (((๐ด + ๐ต)โ†‘๐‘) ยท (๐ด + ๐ต)) = ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)))
186183, 185eqtrd 2220 . . 3 (๐œ‘ โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)))
187186adantr 276 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ ((๐ด + ๐ต)โ†‘(๐‘ + 1)) = ((((๐ด + ๐ต)โ†‘๐‘) ยท ๐ด) + (((๐ด + ๐ต)โ†‘๐‘) ยท ๐ต)))
188 bcpasc 10759 . . . . . . . 8 ((๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) = ((๐‘ + 1)C๐‘˜))
1895, 10, 188syl2an 289 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ ((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) = ((๐‘ + 1)C๐‘˜))
190189oveq1d 5903 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))))
19113, 124, 50adddird 7996 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘C๐‘˜) + (๐‘C(๐‘˜ โˆ’ 1))) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
192190, 191eqtr3d 2222 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ (0...(๐‘ + 1))) โ†’ (((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = (((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
193192sumeq2dv 11389 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘ + 1)C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) = ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
1946peano2zd 9391 . . . . . 6 (๐œ‘ โ†’ (๐‘ + 1) โˆˆ โ„ค)
1954, 194fzfigd 10444 . . . . 5 (๐œ‘ โ†’ (0...(๐‘ + 1)) โˆˆ Fin)
196195, 51, 147fsumadd 11427 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))(((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))) = (ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C๐‘˜) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜))) + ฮฃ๐‘˜ โˆˆ (0...(๐‘ + 1))((๐‘C(๐‘˜ โˆ’ 1)) ยท ((๐ดโ†‘((๐‘ + 1) โˆ’ ๐‘˜)) ยท (๐ตโ†‘๐‘˜)))))
197193, 196eqtrd 2220 . . 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 2230 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 2158   โˆ– cdif 3138   โІ wss 3141  โ€˜cfv 5228  (class class class)co 5888  โ„‚cc 7822  0cc0 7824  1c1 7825   + caddc 7827   ยท cmul 7829   โˆ’ cmin 8141  โ„•cn 8932  โ„•0cn0 9189  โ„คcz 9266  โ„คโ‰ฅcuz 9541  ...cfz 10021  โ†‘cexp 10532  Ccbc 10740  ฮฃcsu 11374
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-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-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-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
This theorem is referenced by:  binom  11505
  Copyright terms: Public domain W3C validator