Metamath Proof Explorer

Theorem sticksstones16

Description: Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024)

Ref Expression
Hypotheses sticksstones16.1 
|- ( ph -> N e. NN0 )
sticksstones16.2 
|- ( ph -> K e. NN )
sticksstones16.3 
|- A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
Assertion sticksstones16 
|- ( ph -> ( # ` A ) = ( ( N + ( K - 1 ) ) _C ( K - 1 ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones16.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones16.2 
 |-  ( ph -> K e. NN )
3 sticksstones16.3 
 |-  A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
4 fveq2 
 |-  ( i = j -> ( g ` i ) = ( g ` j ) )
5 4 cbvsumv 
 |-  sum_ i e. ( 1 ... K ) ( g ` i ) = sum_ j e. ( 1 ... K ) ( g ` j )
6 5 eqeq1i 
 |-  ( sum_ i e. ( 1 ... K ) ( g ` i ) = N <-> sum_ j e. ( 1 ... K ) ( g ` j ) = N )
7 6 anbi2i 
 |-  ( ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) <-> ( g : ( 1 ... K ) --> NN0 /\ sum_ j e. ( 1 ... K ) ( g ` j ) = N ) )
8 7 abbii 
 |-  { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ j e. ( 1 ... K ) ( g ` j ) = N ) }
9 3 8 eqtri 
 |-  A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ j e. ( 1 ... K ) ( g ` j ) = N ) }
10 9 a1i 
 |-  ( ph -> A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ j e. ( 1 ... K ) ( g ` j ) = N ) } )
11 nfv 
 |-  F/ g ph
12 2 nncnd 
 |-  ( ph -> K e. CC )
13 1cnd 
 |-  ( ph -> 1 e. CC )
14 12 13 npcand 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
15 14 eqcomd 
 |-  ( ph -> K = ( ( K - 1 ) + 1 ) )
16 15 oveq2d 
 |-  ( ph -> ( 1 ... K ) = ( 1 ... ( ( K - 1 ) + 1 ) ) )
17 16 feq2d 
 |-  ( ph -> ( g : ( 1 ... K ) --> NN0 <-> g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 ) )
18 16 sumeq1d 
 |-  ( ph -> sum_ j e. ( 1 ... K ) ( g ` j ) = sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) )
19 18 eqeq1d 
 |-  ( ph -> ( sum_ j e. ( 1 ... K ) ( g ` j ) = N <-> sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) )
20 17 19 anbi12d 
 |-  ( ph -> ( ( g : ( 1 ... K ) --> NN0 /\ sum_ j e. ( 1 ... K ) ( g ` j ) = N ) <-> ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) ) )
21 11 20 abbid 
 |-  ( ph -> { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ j e. ( 1 ... K ) ( g ` j ) = N ) } = { g | ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) } )
22 10 21 eqtrd 
 |-  ( ph -> A = { g | ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) } )
23 22 fveq2d 
 |-  ( ph -> ( # ` A ) = ( # ` { g | ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) } ) )
24 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
25 2 24 syl 
 |-  ( ph -> ( K - 1 ) e. NN0 )
26 fveq2 
 |-  ( j = i -> ( g ` j ) = ( g ` i ) )
27 26 cbvsumv 
 |-  sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = sum_ i e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` i )
28 27 eqeq1i 
 |-  ( sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N <-> sum_ i e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` i ) = N )
29 28 anbi2i 
 |-  ( ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) <-> ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` i ) = N ) )
30 29 abbii 
 |-  { g | ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) } = { g | ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` i ) = N ) }
31 1 25 30 sticksstones15 
 |-  ( ph -> ( # ` { g | ( g : ( 1 ... ( ( K - 1 ) + 1 ) ) --> NN0 /\ sum_ j e. ( 1 ... ( ( K - 1 ) + 1 ) ) ( g ` j ) = N ) } ) = ( ( N + ( K - 1 ) ) _C ( K - 1 ) ) )
32 23 31 eqtrd 
 |-  ( ph -> ( # ` A ) = ( ( N + ( K - 1 ) ) _C ( K - 1 ) ) )