Theorem binomfallfac

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

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

Proof

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