Metamath Proof Explorer

Theorem binomcxplemwb

Description: Lemma for binomcxp . The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxplem.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
binomcxplem.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
Assertion binomcxplemwb ( 𝜑 → ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 C𝑐 𝐾 ) ) + ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) ) ) = ( 𝐶 · ( 𝐶 C𝑐 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 binomcxplem.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 binomcxplem.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 2 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
4 1 3 npcand ⊢ ( 𝜑 → ( ( 𝐶 − 𝐾 ) + 𝐾 ) = 𝐶 )
5 4 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐾 ) + 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) = ( 𝐶 · ( 𝐶 FallFac 𝐾 ) ) )
6 1 3 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐾 ) ∈ ℂ )
7 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
8 fallfaccl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
9 1 7 8 syl2anc ⊢ ( 𝜑 → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
10 6 3 9 adddird ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐾 ) + 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) = ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) + ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) ) )
11 5 10 eqtr3d ⊢ ( 𝜑 → ( 𝐶 · ( 𝐶 FallFac 𝐾 ) ) = ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) + ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) ) )
12 11 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) = ( ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) + ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) ) / ( ! ‘ 𝐾 ) ) )
13 1 7 bccval ⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
14 13 oveq2d ⊢ ( 𝜑 → ( 𝐶 · ( 𝐶 C𝑐 𝐾 ) ) = ( 𝐶 · ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ) )
15 faccl ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
16 15 nncnd ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℂ )
17 7 16 syl ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℂ )
18 facne0 ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ≠ 0 )
19 7 18 syl ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ≠ 0 )
20 1 9 17 19 divassd ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) = ( 𝐶 · ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ) )
21 14 20 eqtr4d ⊢ ( 𝜑 → ( 𝐶 · ( 𝐶 C𝑐 𝐾 ) ) = ( ( 𝐶 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) )
22 6 9 17 19 divassd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) = ( ( 𝐶 − 𝐾 ) · ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) + ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) ) = ( ( ( 𝐶 − 𝐾 ) · ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ) + ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) ) )
24 6 9 mulcld ⊢ ( 𝜑 → ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) ∈ ℂ )
25 3 9 mulcld ⊢ ( 𝜑 → ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) ∈ ℂ )
26 24 25 17 19 divdird ⊢ ( 𝜑 → ( ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) + ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) ) / ( ! ‘ 𝐾 ) ) = ( ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) + ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) ) )
27 13 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 − 𝐾 ) · ( 𝐶 C𝑐 𝐾 ) ) = ( ( 𝐶 − 𝐾 ) · ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ) )
28 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
29 2 28 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
30 faccl ⊢ ( ( 𝐾 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℕ )
31 30 nncnd ⊢ ( ( 𝐾 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℂ )
32 29 31 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℂ )
33 facne0 ⊢ ( ( 𝐾 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝐾 − 1 ) ) ≠ 0 )
34 29 33 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝐾 − 1 ) ) ≠ 0 )
35 2 nnne0d ⊢ ( 𝜑 → 𝐾 ≠ 0 )
36 9 32 3 34 35 divcan5d ⊢ ( 𝜑 → ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( 𝐾 · ( ! ‘ ( 𝐾 − 1 ) ) ) ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ ( 𝐾 − 1 ) ) ) )
37 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
38 3 37 npcand ⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
39 38 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ! ‘ 𝐾 ) )
40 38 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝐾 − 1 ) ) · ( ( 𝐾 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
41 facp1 ⊢ ( ( 𝐾 − 1 ) ∈ ℕ0 → ( ! ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · ( ( 𝐾 − 1 ) + 1 ) ) )
42 29 41 syl ⊢ ( 𝜑 → ( ! ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · ( ( 𝐾 − 1 ) + 1 ) ) )
43 3 32 mulcomd ⊢ ( 𝜑 → ( 𝐾 · ( ! ‘ ( 𝐾 − 1 ) ) ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
44 40 42 43 3eqtr4d ⊢ ( 𝜑 → ( ! ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( 𝐾 · ( ! ‘ ( 𝐾 − 1 ) ) ) )
45 39 44 eqtr3d ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) = ( 𝐾 · ( ! ‘ ( 𝐾 − 1 ) ) ) )
46 45 oveq2d ⊢ ( 𝜑 → ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) = ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( 𝐾 · ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
47 3 37 subcld ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℂ )
48 1 47 subcld ⊢ ( 𝜑 → ( 𝐶 − ( 𝐾 − 1 ) ) ∈ ℂ )
49 fallfaccl ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐾 − 1 ) ∈ ℕ0 ) → ( 𝐶 FallFac ( 𝐾 − 1 ) ) ∈ ℂ )
50 1 29 49 syl2anc ⊢ ( 𝜑 → ( 𝐶 FallFac ( 𝐾 − 1 ) ) ∈ ℂ )
51 48 50 32 34 divassd ⊢ ( 𝜑 → ( ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 FallFac ( 𝐾 − 1 ) ) ) / ( ! ‘ ( 𝐾 − 1 ) ) ) = ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( ( 𝐶 FallFac ( 𝐾 − 1 ) ) / ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
52 38 oveq2d ⊢ ( 𝜑 → ( 𝐶 FallFac ( ( 𝐾 − 1 ) + 1 ) ) = ( 𝐶 FallFac 𝐾 ) )
53 fallfacp1 ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐾 − 1 ) ∈ ℕ0 ) → ( 𝐶 FallFac ( ( 𝐾 − 1 ) + 1 ) ) = ( ( 𝐶 FallFac ( 𝐾 − 1 ) ) · ( 𝐶 − ( 𝐾 − 1 ) ) ) )
54 1 29 53 syl2anc ⊢ ( 𝜑 → ( 𝐶 FallFac ( ( 𝐾 − 1 ) + 1 ) ) = ( ( 𝐶 FallFac ( 𝐾 − 1 ) ) · ( 𝐶 − ( 𝐾 − 1 ) ) ) )
55 52 54 eqtr3d ⊢ ( 𝜑 → ( 𝐶 FallFac 𝐾 ) = ( ( 𝐶 FallFac ( 𝐾 − 1 ) ) · ( 𝐶 − ( 𝐾 − 1 ) ) ) )
56 48 50 mulcomd ⊢ ( 𝜑 → ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 FallFac ( 𝐾 − 1 ) ) ) = ( ( 𝐶 FallFac ( 𝐾 − 1 ) ) · ( 𝐶 − ( 𝐾 − 1 ) ) ) )
57 55 56 eqtr4d ⊢ ( 𝜑 → ( 𝐶 FallFac 𝐾 ) = ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 FallFac ( 𝐾 − 1 ) ) ) )
58 57 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ ( 𝐾 − 1 ) ) ) = ( ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 FallFac ( 𝐾 − 1 ) ) ) / ( ! ‘ ( 𝐾 − 1 ) ) ) )
59 1 29 bccval ⊢ ( 𝜑 → ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) = ( ( 𝐶 FallFac ( 𝐾 − 1 ) ) / ( ! ‘ ( 𝐾 − 1 ) ) ) )
60 59 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) ) = ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( ( 𝐶 FallFac ( 𝐾 − 1 ) ) / ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
61 51 58 60 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ ( 𝐾 − 1 ) ) ) )
62 36 46 61 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) ) = ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) )
63 27 62 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 C𝑐 𝐾 ) ) + ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) ) ) = ( ( ( 𝐶 − 𝐾 ) · ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ) + ( ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) / ( ! ‘ 𝐾 ) ) ) )
64 23 26 63 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 C𝑐 𝐾 ) ) + ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) ) ) = ( ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 FallFac 𝐾 ) ) + ( 𝐾 · ( 𝐶 FallFac 𝐾 ) ) ) / ( ! ‘ 𝐾 ) ) )
65 12 21 64 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐾 ) · ( 𝐶 C𝑐 𝐾 ) ) + ( ( 𝐶 − ( 𝐾 − 1 ) ) · ( 𝐶 C𝑐 ( 𝐾 − 1 ) ) ) ) = ( 𝐶 · ( 𝐶 C𝑐 𝐾 ) ) )