Metamath Proof Explorer

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 𝑘 ) ) ) )