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 
|- ( ph -> C e. CC )
binomcxplem.k 
|- ( ph -> K e. NN )
Assertion binomcxplemwb 
|- ( ph -> ( ( ( C - K ) x. ( C _Cc K ) ) + ( ( C - ( K - 1 ) ) x. ( C _Cc ( K - 1 ) ) ) ) = ( C x. ( C _Cc K ) ) )

Proof

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