binomrisefac - Metamath Proof Explorer

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

Theorem binomrisefac 15949

Description: A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018.)

**Assertion**
Ref	Expression
binomrisefac	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 + 𝐵) RiseFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘 𝑘,𝑁

**Proof of Theorem binomrisefac**
Step	Hyp	Ref	Expression
1		negdi 11418	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
2	1	3adant3 1132	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
3	2	oveq1d 7361	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (-(𝐴 + 𝐵) FallFac 𝑁) = ((-𝐴 + -𝐵) FallFac 𝑁))
4		negcl 11360	. . . . . 6 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
5		negcl 11360	. . . . . 6 ⊢ (𝐵 ∈ ℂ → -𝐵 ∈ ℂ)
6		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀)
7		binomfallfac 15948	. . . . . 6 ⊢ ((-𝐴 ∈ ℂ ∧ -𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((-𝐴 + -𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))
8	4, 5, 6, 7	syl3an 1160	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((-𝐴 + -𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))
9	3, 8	eqtrd 2766	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (-(𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))
10	9	oveq2d 7362	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((-1↑𝑁) · (-(𝐴 + 𝐵) FallFac 𝑁)) = ((-1↑𝑁) · Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))))
11		fzfid 13880	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (0...𝑁) ∈ Fin)
12		neg1cn 12110	. . . . . 6 ⊢ -1 ∈ ℂ
13		expcl 13986	. . . . . 6 ⊢ ((-1 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (-1↑𝑁) ∈ ℂ)
14	12, 13	mpan 690	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (-1↑𝑁) ∈ ℂ)
15	14	3ad2ant3 1135	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (-1↑𝑁) ∈ ℂ)
16		simp3 1138	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℕ₀)
17		elfzelz 13424	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
18		bccl 14229	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → (𝑁C𝑘) ∈ ℕ₀)
19	16, 17, 18	syl2an 596	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℕ₀)
20	19	nn0cnd 12444	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ)
21		simpl1 1192	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ)
22	21	negcld 11459	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → -𝐴 ∈ ℂ)
23	16	nn0zd 12494	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℤ)
24		zsubcl 12514	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑁 − 𝑘) ∈ ℤ)
25	23, 17, 24	syl2an 596	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈ ℤ)
26		elfzle2 13428	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ≤ 𝑁)
27	26	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≤ 𝑁)
28		simpl3 1194	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℕ₀)
29	28	nn0red 12443	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
30		elfznn0 13520	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
31	30	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ₀)
32	31	nn0red 12443	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ)
33	29, 32	subge0d 11707	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (0 ≤ (𝑁 − 𝑘) ↔ 𝑘 ≤ 𝑁))
34	27, 33	mpbird 257	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 0 ≤ (𝑁 − 𝑘))
35		elnn0z 12481	. . . . . . . 8 ⊢ ((𝑁 − 𝑘) ∈ ℕ₀ ↔ ((𝑁 − 𝑘) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑘)))
36	25, 34, 35	sylanbrc 583	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈ ℕ₀)
37		fallfaccl 15923	. . . . . . 7 ⊢ ((-𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ₀) → (-𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ)
38	22, 36, 37	syl2anc 584	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (-𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ)
39		simp2 1137	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → 𝐵 ∈ ℂ)
40	39	negcld 11459	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → -𝐵 ∈ ℂ)
41		fallfaccl 15923	. . . . . . 7 ⊢ ((-𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (-𝐵 FallFac 𝑘) ∈ ℂ)
42	40, 30, 41	syl2an 596	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (-𝐵 FallFac 𝑘) ∈ ℂ)
43	38, 42	mulcld 11132	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)) ∈ ℂ)
44	20, 43	mulcld 11132	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))) ∈ ℂ)
45	11, 15, 44	fsummulc2 15691	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((-1↑𝑁) · Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))))
46	10, 45	eqtrd 2766	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((-1↑𝑁) · (-(𝐴 + 𝐵) FallFac 𝑁)) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))))
47		addcl 11088	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
48		risefallfac 15931	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 + 𝐵) RiseFac 𝑁) = ((-1↑𝑁) · (-(𝐴 + 𝐵) FallFac 𝑁)))
49	47, 48	stoic3 1777	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 + 𝐵) RiseFac 𝑁) = ((-1↑𝑁) · (-(𝐴 + 𝐵) FallFac 𝑁)))
50		risefallfac 15931	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ₀) → (𝐴 RiseFac (𝑁 − 𝑘)) = ((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘))))
51	21, 36, 50	syl2anc 584	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 RiseFac (𝑁 − 𝑘)) = ((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘))))
52		simpl2 1193	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ ℂ)
53		risefallfac 15931	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐵 RiseFac 𝑘) = ((-1↑𝑘) · (-𝐵 FallFac 𝑘)))
54	52, 31, 53	syl2anc 584	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 RiseFac 𝑘) = ((-1↑𝑘) · (-𝐵 FallFac 𝑘)))
55	51, 54	oveq12d 7364	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘)) = (((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘))) · ((-1↑𝑘) · (-𝐵 FallFac 𝑘))))
56		expcl 13986	. . . . . . . 8 ⊢ ((-1 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ₀) → (-1↑(𝑁 − 𝑘)) ∈ ℂ)
57	12, 36, 56	sylancr 587	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (-1↑(𝑁 − 𝑘)) ∈ ℂ)
58		expcl 13986	. . . . . . . . 9 ⊢ ((-1 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℂ)
59	12, 30, 58	sylancr 587	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝑁) → (-1↑𝑘) ∈ ℂ)
60	59	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
61	57, 38, 60, 42	mul4d 11325	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘))) · ((-1↑𝑘) · (-𝐵 FallFac 𝑘))) = (((-1↑(𝑁 − 𝑘)) · (-1↑𝑘)) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))
62	12	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → -1 ∈ ℂ)
63	62, 31, 36	expaddd 14055	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (-1↑((𝑁 − 𝑘) + 𝑘)) = ((-1↑(𝑁 − 𝑘)) · (-1↑𝑘)))
64	16	nn0cnd 12444	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℂ)
65	30	nn0cnd 12444	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ)
66		npcan 11369	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑁 − 𝑘) + 𝑘) = 𝑁)
67	64, 65, 66	syl2an 596	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 𝑘) + 𝑘) = 𝑁)
68	67	oveq2d 7362	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (-1↑((𝑁 − 𝑘) + 𝑘)) = (-1↑𝑁))
69	63, 68	eqtr3d 2768	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑(𝑁 − 𝑘)) · (-1↑𝑘)) = (-1↑𝑁))
70	69	oveq1d 7361	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (((-1↑(𝑁 − 𝑘)) · (-1↑𝑘)) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))) = ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))
71	55, 61, 70	3eqtrd 2770	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘)) = ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))
72	71	oveq2d 7362	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))) = ((𝑁C𝑘) · ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))))
73	15	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑁) ∈ ℂ)
74	20, 73, 43	mul12d 11322	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) = ((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))))
75	72, 74	eqtrd 2766	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))) = ((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))))
76	75	sumeq2dv 15609	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))))
77	46, 49, 76	3eqtr4d 2776	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 + 𝐵) RiseFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 class class class wbr 5089 (class class class)co 7346 ℂcc 11004 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 ≤ cle 11147 − cmin 11344 -cneg 11345 ℕ₀cn0 12381 ℤcz 12468 ...cfz 13407 ↑cexp 13968 Ccbc 14209 Σcsu 15593 FallFac cfallfac 15911 RiseFac crisefac 15912

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-oi 9396 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-fz 13408 df-fzo 13555 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594 df-prod 15811 df-risefac 15913 df-fallfac 15914

This theorem is referenced by: (None)

W3C validator