binomfallfac - Metamath Proof Explorer

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

Theorem binomfallfac 16096

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

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

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

Proof of Theorem binomfallfac Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7420	. . . . . 6 ⊢ (𝑚 = 0 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 0))
2		oveq2 7420	. . . . . . . 8 ⊢ (𝑚 = 0 → (0...𝑚) = (0...0))
3		fz0sn 13657	. . . . . . . 8 ⊢ (0...0) = {0}
4	2, 3	eqtrdi 2814	. . . . . . 7 ⊢ (𝑚 = 0 → (0...𝑚) = {0})
5		oveq1 7419	. . . . . . . . 9 ⊢ (𝑚 = 0 → (𝑚C𝑘) = (0C𝑘))
6		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑚 = 0 → (𝑚 − 𝑘) = (0 − 𝑘))
7	6	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (0 − 𝑘)))
8	7	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑚 = 0 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))
9	5, 8	oveq12d 7430	. . . . . . . 8 ⊢ (𝑚 = 0 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))))
10	9	adantr 485	. . . . . . 7 ⊢ ((𝑚 = 0 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))))
11	4, 10	sumeq12dv 15759	. . . . . 6 ⊢ (𝑚 = 0 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))))
12	1, 11	eqeq12d 2779	. . . . 5 ⊢ (𝑚 = 0 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))))
13	12	imbi2d 343	. . . 4 ⊢ (𝑚 = 0 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))))))
14		oveq2 7420	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 𝑛))
15		oveq2 7420	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (0...𝑚) = (0...𝑛))
16		oveq1 7419	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑚C𝑘) = (𝑛C𝑘))
17		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑚 − 𝑘) = (𝑛 − 𝑘))
18	17	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (𝑛 − 𝑘)))
19	18	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))
20	16, 19	oveq12d 7430	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))))
21	20	adantr 485	. . . . . . 7 ⊢ ((𝑚 = 𝑛 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))))
22	15, 21	sumeq12dv 15759	. . . . . 6 ⊢ (𝑚 = 𝑛 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))))
23	14, 22	eqeq12d 2779	. . . . 5 ⊢ (𝑚 = 𝑛 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))))
24	23	imbi2d 343	. . . 4 ⊢ (𝑚 = 𝑛 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))))))
25		oveq2 7420	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac (𝑛 + 1)))
26		oveq2 7420	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (0...𝑚) = (0...(𝑛 + 1)))
27		oveq1 7419	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → (𝑚C𝑘) = ((𝑛 + 1)C𝑘))
28		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 𝑘) = ((𝑛 + 1) − 𝑘))
29	28	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac ((𝑛 + 1) − 𝑘)))
30	29	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))
31	27, 30	oveq12d 7430	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))
32	31	adantr 485	. . . . . . 7 ⊢ ((𝑚 = (𝑛 + 1) ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))
33	26, 32	sumeq12dv 15759	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))
34	25, 33	eqeq12d 2779	. . . . 5 ⊢ (𝑚 = (𝑛 + 1) → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))))
35	34	imbi2d 343	. . . 4 ⊢ (𝑚 = (𝑛 + 1) → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))))
36		oveq2 7420	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 𝑁))
37		oveq2 7420	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (0...𝑚) = (0...𝑁))
38		oveq1 7419	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (𝑚C𝑘) = (𝑁C𝑘))
39		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → (𝑚 − 𝑘) = (𝑁 − 𝑘))
40	39	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (𝑁 − 𝑘)))
41	40	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))
42	38, 41	oveq12d 7430	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))
43	42	adantr 485	. . . . . . 7 ⊢ ((𝑚 = 𝑁 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))
44	37, 43	sumeq12dv 15759	. . . . . 6 ⊢ (𝑚 = 𝑁 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))
45	36, 44	eqeq12d 2779	. . . . 5 ⊢ (𝑚 = 𝑁 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))))
46	45	imbi2d 343	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))))
47		fallfac0 16083	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 0) = 1)
48		fallfac0 16083	. . . . . . . . 9 ⊢ (𝐵 ∈ ℂ → (𝐵 FallFac 0) = 1)
49	47, 48	oveqan12d 7431	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 FallFac 0) · (𝐵 FallFac 0)) = (1 · 1))
50		1t1e1 12403	. . . . . . . 8 ⊢ (1 · 1) = 1
51	49, 50	eqtrdi 2814	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 FallFac 0) · (𝐵 FallFac 0)) = 1)
52	51	oveq2d 7428	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))) = (1 · 1))
53	52, 50	eqtrdi 2814	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))) = 1)
54		0cn 11199	. . . . . 6 ⊢ 0 ∈ ℂ
55		ax-1cn 11159	. . . . . . 7 ⊢ 1 ∈ ℂ
56	53, 55	eqeltrdi 2871	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))) ∈ ℂ)
57		oveq2 7420	. . . . . . . . 9 ⊢ (𝑘 = 0 → (0C𝑘) = (0C0))
58		0nn0 12520	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
59		bcnn 14350	. . . . . . . . . 10 ⊢ (0 ∈ ℕ₀ → (0C0) = 1)
60	58, 59	ax-mp 5	. . . . . . . . 9 ⊢ (0C0) = 1
61	57, 60	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑘 = 0 → (0C𝑘) = 1)
62		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (0 − 𝑘) = (0 − 0))
63		0m0e0 12360	. . . . . . . . . . 11 ⊢ (0 − 0) = 0
64	62, 63	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (0 − 𝑘) = 0)
65	64	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝐴 FallFac (0 − 𝑘)) = (𝐴 FallFac 0))
66		oveq2 7420	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝐵 FallFac 𝑘) = (𝐵 FallFac 0))
67	65, 66	oveq12d 7430	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac 0) · (𝐵 FallFac 0)))
68	61, 67	oveq12d 7430	. . . . . . 7 ⊢ (𝑘 = 0 → ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))))
69	68	sumsn 15799	. . . . . 6 ⊢ ((0 ∈ ℂ ∧ (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))) ∈ ℂ) → Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))))
70	54, 56, 69	sylancr 598	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))))
71		addcl 11183	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
72		fallfac0 16083	. . . . . 6 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((𝐴 + 𝐵) FallFac 0) = 1)
73	71, 72	syl 18	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = 1)
74	53, 70, 73	3eqtr4rd 2809	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))))
75		simprl 782	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ₀ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → 𝐴 ∈ ℂ)
76		simprr 784	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ₀ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → 𝐵 ∈ ℂ)
77		simpl 487	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ₀ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) → 𝑛 ∈ ℕ₀)
78		id 23	. . . . . . 7 ⊢ (((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) → ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))))
79	75, 76, 77, 78	binomfallfaclem2 16095	. . . . . 6 ⊢ (((𝑛 ∈ ℕ₀ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))
80	79	exp31 424	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))))
81	80	a2d 30	. . . 4 ⊢ (𝑛 ∈ ℕ₀ → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))))
82	13, 24, 35, 46, 74, 81	nn0ind 12692	. . 3 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))))
83	82	com12 33	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 ∈ ℕ₀ → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))))
84	83	3impia 1135	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 {csn 4590 (class class class)co 7412 ℂcc 11099 0cc0 11101 1c1 11102 + caddc 11104 · cmul 11106 − cmin 11442 ℕ₀cn0 12505 ...cfz 13536 Ccbc 14340 Σcsu 15739 FallFac cfallfac 16060

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-inf2 9611 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-pre-sup 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-sup 9403 df-oi 9473 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-n0 12506 df-z 12593 df-uz 12864 df-rp 13018 df-fz 13537 df-fzo 13685 df-seq 14040 df-exp 14100 df-fac 14312 df-bc 14341 df-hash 14369 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-clim 15541 df-sum 15740 df-prod 15960 df-risefac 16062 df-fallfac 16063

This theorem is referenced by: binomrisefac 16097

W3C validator