Theorem binomfallfaclem2

Description: Lemma for binomfallfac . Inductive step. (Contributed by Scott Fenton, 13-Mar-2018)

	Ref	Expression
Hypotheses	binomfallfaclem.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	binomfallfaclem.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	binomfallfaclem.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	binomfallfaclem.4	⊢ ( 𝜓 → ( ( 𝐴 + 𝐵 ) FallFac 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )
Assertion	binomfallfaclem2	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + 𝐵 ) FallFac ( 𝑁 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		binomfallfaclem.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		binomfallfaclem.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		binomfallfaclem.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		binomfallfaclem.4	⊢ ( 𝜓 → ( ( 𝐴 + 𝐵 ) FallFac 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )
5		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
6		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
7	3 5 6	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
8	7	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
9		fznn0sub	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
10		fallfaccl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ∈ ℂ )
11	1 9 10	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) ∈ ℂ )
12		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
13		fallfaccl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 FallFac 𝑘 ) ∈ ℂ )
14	2 12 13	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 FallFac 𝑘 ) ∈ ℂ )
15	11 14	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ∈ ℂ )
16	1 2	addcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
17	3	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
18	16 17	subcld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − 𝑁 ) ∈ ℂ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 + 𝐵 ) − 𝑁 ) ∈ ℂ )
20	8 15 19	mulassd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = ( ( 𝑁 C 𝑘 ) · ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) ) )
21	9	nn0cnd	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℂ )
22		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 𝑘 ) ∈ ℂ ) → ( 𝐴 − ( 𝑁 − 𝑘 ) ) ∈ ℂ )
23	1 21 22	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 − ( 𝑁 − 𝑘 ) ) ∈ ℂ )
24	12	nn0cnd	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℂ )
25		subcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐵 − 𝑘 ) ∈ ℂ )
26	2 24 25	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 − 𝑘 ) ∈ ℂ )
27	15 23 26	adddid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( ( 𝐴 − ( 𝑁 − 𝑘 ) ) + ( 𝐵 − 𝑘 ) ) ) = ( ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) + ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐵 − 𝑘 ) ) ) )
28	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
29	17	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℂ )
30	28 29	subcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 − 𝑁 ) ∈ ℂ )
31	24	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
32	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ ℂ )
33	30 31 32	ppncand	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 − 𝑁 ) + 𝑘 ) + ( 𝐵 − 𝑘 ) ) = ( ( 𝐴 − 𝑁 ) + 𝐵 ) )
34	28 29 31	subsubd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 − ( 𝑁 − 𝑘 ) ) = ( ( 𝐴 − 𝑁 ) + 𝑘 ) )
35	34	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 − ( 𝑁 − 𝑘 ) ) + ( 𝐵 − 𝑘 ) ) = ( ( ( 𝐴 − 𝑁 ) + 𝑘 ) + ( 𝐵 − 𝑘 ) ) )
36	28 32 29	addsubd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 + 𝐵 ) − 𝑁 ) = ( ( 𝐴 − 𝑁 ) + 𝐵 ) )
37	33 35 36	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 − ( 𝑁 − 𝑘 ) ) + ( 𝐵 − 𝑘 ) ) = ( ( 𝐴 + 𝐵 ) − 𝑁 ) )
38	37	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( ( 𝐴 − ( 𝑁 − 𝑘 ) ) + ( 𝐵 − 𝑘 ) ) ) = ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
39	11 14 23	mul32d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) = ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) · ( 𝐵 FallFac 𝑘 ) ) )
40		1cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 1 ∈ ℂ )
41	29 40 31	addsubd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 − 𝑘 ) + 1 ) )
42	41	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( 𝐴 FallFac ( ( 𝑁 − 𝑘 ) + 1 ) ) )
43		fallfacp1	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) )
44	1 9 43	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 FallFac ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) )
45	42 44	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) )
46	45	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) = ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) · ( 𝐵 FallFac 𝑘 ) ) )
47	39 46	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) = ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) )
48	11 14 26	mulassd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐵 − 𝑘 ) ) = ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( ( 𝐵 FallFac 𝑘 ) · ( 𝐵 − 𝑘 ) ) ) )
49		fallfacp1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 FallFac ( 𝑘 + 1 ) ) = ( ( 𝐵 FallFac 𝑘 ) · ( 𝐵 − 𝑘 ) ) )
50	2 12 49	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 FallFac ( 𝑘 + 1 ) ) = ( ( 𝐵 FallFac 𝑘 ) · ( 𝐵 − 𝑘 ) ) )
51	50	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) = ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( ( 𝐵 FallFac 𝑘 ) · ( 𝐵 − 𝑘 ) ) ) )
52	48 51	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐵 − 𝑘 ) ) = ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) )
53	47 52	oveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐴 − ( 𝑁 − 𝑘 ) ) ) + ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( 𝐵 − 𝑘 ) ) ) = ( ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) + ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) )
54	27 38 53	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = ( ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) + ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) )
55	54	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) + ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
56	3	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
57		uzid	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
58		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
59		fzss2	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( 𝑁 + 1 ) ) )
60	56 57 58 59	4syl	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( 𝑁 + 1 ) ) )
61	60	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
62		fznn0sub	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
63		fallfaccl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℂ )
64	1 62 63	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℂ )
65	61 64	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℂ )
66	65 14	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ∈ ℂ )
67		peano2nn0	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
68	12 67	syl	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑘 + 1 ) ∈ ℕ0 )
69		fallfaccl	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝐵 FallFac ( 𝑘 + 1 ) ) ∈ ℂ )
70	2 68 69	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 FallFac ( 𝑘 + 1 ) ) ∈ ℂ )
71	11 70	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ∈ ℂ )
72	8 66 71	adddid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) + ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
73	20 55 72	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
74	73	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
75	74	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
76	16 3	fallfacp1d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) FallFac ( 𝑁 + 1 ) ) = ( ( ( 𝐴 + 𝐵 ) FallFac 𝑁 ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
77	4	oveq1d	⊢ ( 𝜓 → ( ( ( 𝐴 + 𝐵 ) FallFac 𝑁 ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
78	76 77	sylan9eq	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + 𝐵 ) FallFac ( 𝑁 + 1 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
79		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
80	8 15	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ∈ ℂ )
81	79 18 80	fsummulc1	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
82	81	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
83	78 82	eqtrd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + 𝐵 ) FallFac ( 𝑁 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) · ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
84		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
85		bcpasc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
86	3 84 85	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
87	86	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )
88	3 84 6	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
89	88	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
90		peano2zm	⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
91	84 90	syl	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
92		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
93	3 91 92	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
94	93	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℂ )
95		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
96	2 95 13	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝐵 FallFac 𝑘 ) ∈ ℂ )
97	64 96	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ∈ ℂ )
98	89 94 97	adddird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) )
99	87 98	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) )
100	99	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) )
101		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
102	3 101	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
103	89 97	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ∈ ℂ )
104		oveq2	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑁 C 𝑘 ) = ( 𝑁 C ( 𝑁 + 1 ) ) )
105		oveq2	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) )
106	105	oveq2d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) )
107		oveq2	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝐵 FallFac 𝑘 ) = ( 𝐵 FallFac ( 𝑁 + 1 ) ) )
108	106 107	oveq12d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) = ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) )
109	104 108	oveq12d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ) )
110	102 103 109	fsump1	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ) ) )
111		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
112	3 111	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
113	112	nn0zd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
114	3	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
115	114	ltp1d	⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 1 ) )
116	115	olcd	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) < 0 ∨ 𝑁 < ( 𝑁 + 1 ) ) )
117		bcval4	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ ( ( 𝑁 + 1 ) < 0 ∨ 𝑁 < ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑁 + 1 ) ) = 0 )
118	3 113 116 117	syl3anc	⊢ ( 𝜑 → ( 𝑁 C ( 𝑁 + 1 ) ) = 0 )
119	118	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ) = ( 0 · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ) )
120	112	nn0cnd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
121	120	subidd	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) = 0 )
122	121	oveq2d	⊢ ( 𝜑 → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) = ( 𝐴 FallFac 0 ) )
123		0nn0	⊢ 0 ∈ ℕ0
124		fallfaccl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 FallFac 0 ) ∈ ℂ )
125	1 123 124	sylancl	⊢ ( 𝜑 → ( 𝐴 FallFac 0 ) ∈ ℂ )
126	122 125	eqeltrd	⊢ ( 𝜑 → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) ∈ ℂ )
127		fallfaccl	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 𝐵 FallFac ( 𝑁 + 1 ) ) ∈ ℂ )
128	2 112 127	syl2anc	⊢ ( 𝜑 → ( 𝐵 FallFac ( 𝑁 + 1 ) ) ∈ ℂ )
129	126 128	mulcld	⊢ ( 𝜑 → ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ∈ ℂ )
130	129	mul02d	⊢ ( 𝜑 → ( 0 · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ) = 0 )
131	119 130	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ) = 0 )
132	131	oveq2d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − ( 𝑁 + 1 ) ) ) · ( 𝐵 FallFac ( 𝑁 + 1 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + 0 ) )
133	61 103	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ∈ ℂ )
134	79 133	fsumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ∈ ℂ )
135	134	addid1d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + 0 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )
136	110 132 135	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )
137	112 101	eleqtrdi	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
138	94 97	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ∈ ℂ )
139		oveq1	⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = ( 0 − 1 ) )
140		df-neg	⊢ - 1 = ( 0 − 1 )
141	139 140	eqtr4di	⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = - 1 )
142	141	oveq2d	⊢ ( 𝑘 = 0 → ( 𝑁 C ( 𝑘 − 1 ) ) = ( 𝑁 C - 1 ) )
143		oveq2	⊢ ( 𝑘 = 0 → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 + 1 ) − 0 ) )
144	143	oveq2d	⊢ ( 𝑘 = 0 → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) )
145		oveq2	⊢ ( 𝑘 = 0 → ( 𝐵 FallFac 𝑘 ) = ( 𝐵 FallFac 0 ) )
146	144 145	oveq12d	⊢ ( 𝑘 = 0 → ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) = ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) )
147	142 146	oveq12d	⊢ ( 𝑘 = 0 → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = ( ( 𝑁 C - 1 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ) )
148	137 138 147	fsum1p	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = ( ( ( 𝑁 C - 1 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) )
149		neg1z	⊢ - 1 ∈ ℤ
150		neg1lt0	⊢ - 1 < 0
151	150	orci	⊢ ( - 1 < 0 ∨ 𝑁 < - 1 )
152		bcval4	⊢ ( ( 𝑁 ∈ ℕ0 ∧ - 1 ∈ ℤ ∧ ( - 1 < 0 ∨ 𝑁 < - 1 ) ) → ( 𝑁 C - 1 ) = 0 )
153	149 151 152	mp3an23	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C - 1 ) = 0 )
154	3 153	syl	⊢ ( 𝜑 → ( 𝑁 C - 1 ) = 0 )
155	154	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 C - 1 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ) = ( 0 · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ) )
156	120	subid1d	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 0 ) = ( 𝑁 + 1 ) )
157	156	oveq2d	⊢ ( 𝜑 → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) = ( 𝐴 FallFac ( 𝑁 + 1 ) ) )
158		fallfaccl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 + 1 ) ) ∈ ℂ )
159	1 112 158	syl2anc	⊢ ( 𝜑 → ( 𝐴 FallFac ( 𝑁 + 1 ) ) ∈ ℂ )
160	157 159	eqeltrd	⊢ ( 𝜑 → ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) ∈ ℂ )
161		fallfaccl	⊢ ( ( 𝐵 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐵 FallFac 0 ) ∈ ℂ )
162	2 123 161	sylancl	⊢ ( 𝜑 → ( 𝐵 FallFac 0 ) ∈ ℂ )
163	160 162	mulcld	⊢ ( 𝜑 → ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ∈ ℂ )
164	163	mul02d	⊢ ( 𝜑 → ( 0 · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ) = 0 )
165	155 164	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 C - 1 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ) = 0 )
166		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
167		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
168	1 2 3	binomfallfaclem1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑗 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
169		oveq2	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝑁 C 𝑗 ) = ( 𝑁 C ( 𝑘 − 1 ) ) )
170		oveq2	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝑁 − 𝑗 ) = ( 𝑁 − ( 𝑘 − 1 ) ) )
171	170	oveq2d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) = ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) )
172		oveq1	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝑗 + 1 ) = ( ( 𝑘 − 1 ) + 1 ) )
173	172	oveq2d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝐵 FallFac ( 𝑗 + 1 ) ) = ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) )
174	171 173	oveq12d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) = ( ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) ) )
175	169 174	oveq12d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝑁 C 𝑗 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) ) ) )
176	166 167 56 168 175	fsumshft	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑗 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) ) ) )
177	17	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℂ )
178		elfzelz	⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
179	178	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℤ )
180	179	zcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℂ )
181		1cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
182	177 180 181	subsub3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑁 − ( 𝑘 − 1 ) ) = ( ( 𝑁 + 1 ) − 𝑘 ) )
183	182	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) = ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) )
184	180 181	npcand	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
185	184	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) = ( 𝐵 FallFac 𝑘 ) )
186	183 185	oveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) ) = ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) )
187	186	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )
188	187	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐵 FallFac ( ( 𝑘 − 1 ) + 1 ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )
189	176 188	eqtr2d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑗 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) ) )
190		oveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑁 C 𝑘 ) = ( 𝑁 C 𝑗 ) )
191		oveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑁 − 𝑘 ) = ( 𝑁 − 𝑗 ) )
192	191	oveq2d	⊢ ( 𝑘 = 𝑗 → ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) = ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) )
193		oveq1	⊢ ( 𝑘 = 𝑗 → ( 𝑘 + 1 ) = ( 𝑗 + 1 ) )
194	193	oveq2d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 FallFac ( 𝑘 + 1 ) ) = ( 𝐵 FallFac ( 𝑗 + 1 ) ) )
195	192 194	oveq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) = ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) )
196	190 195	oveq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) = ( ( 𝑁 C 𝑗 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) ) )
197	196	cbvsumv	⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) = Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑗 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑗 ) ) · ( 𝐵 FallFac ( 𝑗 + 1 ) ) ) )
198	189 197	eqtr4di	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) )
199	165 198	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑁 C - 1 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 0 ) ) · ( 𝐵 FallFac 0 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) = ( 0 + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
200	1 2 3	binomfallfaclem1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ∈ ℂ )
201	79 200	fsumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ∈ ℂ )
202	201	addid2d	⊢ ( 𝜑 → ( 0 + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) )
203	148 199 202	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) )
204	136 203	oveq12d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
205		fzfid	⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
206	205 103 138	fsumadd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) )
207	79 133 200	fsumadd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
208	204 206 207	3eqtr4d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
209	100 208	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
210	209	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝑘 ) ) · ( 𝐵 FallFac ( 𝑘 + 1 ) ) ) ) ) )
211	75 83 210	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + 𝐵 ) FallFac ( 𝑁 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( 𝐴 FallFac ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐵 FallFac 𝑘 ) ) ) )