This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcxmas

Description: Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion bcxmas ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑀 ) C 𝑀 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )

Proof

Step Hyp Ref Expression
1 bcxmaslem1 ⊢ ( 𝑚 = 0 → ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = ( ( ( 𝑁 + 1 ) + 0 ) C 0 ) )
2 oveq2 ⊢ ( 𝑚 = 0 → ( 0 ... 𝑚 ) = ( 0 ... 0 ) )
3 2 sumeq1d ⊢ ( 𝑚 = 0 → Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = Σ 𝑗 ∈ ( 0 ... 0 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )
4 1 3 eqeq12d ⊢ ( 𝑚 = 0 → ( ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ↔ ( ( ( 𝑁 + 1 ) + 0 ) C 0 ) = Σ 𝑗 ∈ ( 0 ... 0 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) )
5 bcxmaslem1 ⊢ ( 𝑚 = 𝑘 → ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) )
6 oveq2 ⊢ ( 𝑚 = 𝑘 → ( 0 ... 𝑚 ) = ( 0 ... 𝑘 ) )
7 6 sumeq1d ⊢ ( 𝑚 = 𝑘 → Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )
8 5 7 eqeq12d ⊢ ( 𝑚 = 𝑘 → ( ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ↔ ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) )
9 bcxmaslem1 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = ( ( ( 𝑁 + 1 ) + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) )
10 oveq2 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 0 ... 𝑚 ) = ( 0 ... ( 𝑘 + 1 ) ) )
11 10 sumeq1d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = Σ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )
12 9 11 eqeq12d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ↔ ( ( ( 𝑁 + 1 ) + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) )
13 bcxmaslem1 ⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = ( ( ( 𝑁 + 1 ) + 𝑀 ) C 𝑀 ) )
14 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 0 ... 𝑚 ) = ( 0 ... 𝑀 ) )
15 14 sumeq1d ⊢ ( 𝑚 = 𝑀 → Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )
16 13 15 eqeq12d ⊢ ( 𝑚 = 𝑀 → ( ( ( ( 𝑁 + 1 ) + 𝑚 ) C 𝑚 ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ↔ ( ( ( 𝑁 + 1 ) + 𝑀 ) C 𝑀 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) )
17 0nn0 ⊢ 0 ∈ ℕ0
18 nn0addcl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( 𝑁 + 0 ) ∈ ℕ0 )
19 bcn0 ⊢ ( ( 𝑁 + 0 ) ∈ ℕ0 → ( ( 𝑁 + 0 ) C 0 ) = 1 )
20 18 19 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( 𝑁 + 0 ) C 0 ) = 1 )
21 17 20 mpan2 ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 0 ) C 0 ) = 1 )
22 0z ⊢ 0 ∈ ℤ
23 1nn0 ⊢ 1 ∈ ℕ0
24 21 23 eqeltrdi ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 0 ) C 0 ) ∈ ℕ0 )
25 24 nn0cnd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 0 ) C 0 ) ∈ ℂ )
26 bcxmaslem1 ⊢ ( 𝑗 = 0 → ( ( 𝑁 + 𝑗 ) C 𝑗 ) = ( ( 𝑁 + 0 ) C 0 ) )
27 26 fsum1 ⊢ ( ( 0 ∈ ℤ ∧ ( ( 𝑁 + 0 ) C 0 ) ∈ ℂ ) → Σ 𝑗 ∈ ( 0 ... 0 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = ( ( 𝑁 + 0 ) C 0 ) )
28 22 25 27 sylancr ⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑗 ∈ ( 0 ... 0 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = ( ( 𝑁 + 0 ) C 0 ) )
29 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
30 nn0addcl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) + 0 ) ∈ ℕ0 )
31 29 17 30 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 0 ) ∈ ℕ0 )
32 bcn0 ⊢ ( ( ( 𝑁 + 1 ) + 0 ) ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 0 ) C 0 ) = 1 )
33 31 32 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 0 ) C 0 ) = 1 )
34 21 28 33 3eqtr4rd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 0 ) C 0 ) = Σ 𝑗 ∈ ( 0 ... 0 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )
35 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
36 elnn0uz ⊢ ( 𝑘 ∈ ℕ0 ↔ 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
37 35 36 sylib ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
38 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
39 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) → 𝑗 ∈ ℕ0 )
40 nn0addcl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑁 + 𝑗 ) ∈ ℕ0 )
41 38 39 40 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ) → ( 𝑁 + 𝑗 ) ∈ ℕ0 )
42 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) → 𝑗 ∈ ℤ )
43 42 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ) → 𝑗 ∈ ℤ )
44 bccl ⊢ ( ( ( 𝑁 + 𝑗 ) ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( ( 𝑁 + 𝑗 ) C 𝑗 ) ∈ ℕ0 )
45 41 43 44 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ) → ( ( 𝑁 + 𝑗 ) C 𝑗 ) ∈ ℕ0 )
46 45 nn0cnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ) → ( ( 𝑁 + 𝑗 ) C 𝑗 ) ∈ ℂ )
47 bcxmaslem1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑁 + 𝑗 ) C 𝑗 ) = ( ( 𝑁 + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) )
48 37 46 47 fsump1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) + ( ( 𝑁 + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) ) )
49 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
50 49 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
51 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
52 51 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
53 1cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℂ )
54 add32r ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 + ( 𝑘 + 1 ) ) = ( ( 𝑁 + 1 ) + 𝑘 ) )
55 50 52 53 54 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + ( 𝑘 + 1 ) ) = ( ( 𝑁 + 1 ) + 𝑘 ) )
56 55 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) = ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) )
57 56 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) + ( ( 𝑁 + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) )
58 48 57 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) )
59 58 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) → Σ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) = ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) )
60 oveq1 ⊢ ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) )
61 60 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) )
62 ax-1cn ⊢ 1 ∈ ℂ
63 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
64 52 62 63 sylancl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
65 64 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( ( 𝑘 + 1 ) − 1 ) ) = ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) )
66 65 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( ( 𝑘 + 1 ) − 1 ) ) ) = ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) ) )
67 nn0addcl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ0 )
68 29 67 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ0 )
69 nn0p1nn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
70 69 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℕ )
71 70 nnzd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℤ )
72 bcpasc ⊢ ( ( ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ0 ∧ ( 𝑘 + 1 ) ∈ ℤ ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( ( 𝑘 + 1 ) − 1 ) ) ) = ( ( ( ( 𝑁 + 1 ) + 𝑘 ) + 1 ) C ( 𝑘 + 1 ) ) )
73 68 71 72 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( ( 𝑘 + 1 ) − 1 ) ) ) = ( ( ( ( 𝑁 + 1 ) + 𝑘 ) + 1 ) C ( 𝑘 + 1 ) ) )
74 66 73 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) ) = ( ( ( ( 𝑁 + 1 ) + 𝑘 ) + 1 ) C ( 𝑘 + 1 ) ) )
75 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
76 nnnn0addcl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ )
77 75 76 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ )
78 77 nnnn0d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ0 )
79 bccl ⊢ ( ( ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ0 ∧ ( 𝑘 + 1 ) ∈ ℤ ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ∈ ℕ0 )
80 78 71 79 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ∈ ℕ0 )
81 80 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ∈ ℂ )
82 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
83 82 adantl ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
84 bccl ⊢ ( ( ( ( 𝑁 + 1 ) + 𝑘 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) ∈ ℕ0 )
85 67 83 84 syl2anc ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) ∈ ℕ0 )
86 29 85 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) ∈ ℕ0 )
87 86 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) ∈ ℂ )
88 81 87 addcomd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) ) = ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) )
89 peano2cn ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
90 49 89 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
91 90 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℂ )
92 91 52 53 addassd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑘 ) + 1 ) = ( ( 𝑁 + 1 ) + ( 𝑘 + 1 ) ) )
93 92 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) + 1 ) C ( 𝑘 + 1 ) ) = ( ( ( 𝑁 + 1 ) + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) )
94 74 88 93 3eqtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) )
95 94 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) → ( ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) + ( ( ( 𝑁 + 1 ) + 𝑘 ) C ( 𝑘 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) )
96 59 61 95 3eqtr2rd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( ( 𝑁 + 1 ) + 𝑘 ) C 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) ) → ( ( ( 𝑁 + 1 ) + ( 𝑘 + 1 ) ) C ( 𝑘 + 1 ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑘 + 1 ) ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )
97 4 8 12 16 34 96 nn0indd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) + 𝑀 ) C 𝑀 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑁 + 𝑗 ) C 𝑗 ) )